Theory Lib

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
   Miscellaneous library definitions and lemmas.
*)

chapter "Library"

theory Lib
imports Main
begin

(* FIXME: eliminate *)
lemma hd_map_simp:
  "b ≠ [] ⟹ hd (map a b) = a (hd b)"
  by (rule hd_map)

lemma tl_map_simp:
  "tl (map a b) = map a (tl b)"
  by (induct b,auto)

(* FIXME: could be added to Set.thy *)
lemma Collect_eq:
  "{x. P x} = {x. Q x} ⟷ (∀x. P x = Q x)"
  by (rule iffI) auto

(* FIXME: move next to HOL.iff_allI *)
lemma iff_impI: "⟦P ⟹ Q = R⟧ ⟹ (P ⟶ Q) = (P ⟶ R)" by blast

definition
  fun_app :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixr "$" 10) where
  "f $ x ≡ f x"

declare fun_app_def [iff]

lemma fun_app_cong[fundef_cong]:
  "⟦ f x = f' x' ⟧ ⟹ (f $ x) = (f' $ x')"
  by simp

lemma fun_app_apply_cong[fundef_cong]:
  "f x y = f' x' y' ⟹ (f $ x) y = (f' $ x') y'"
  by simp

lemma if_apply_cong[fundef_cong]:
  "⟦ P = P'; x = x'; P' ⟹ f x' = f' x'; ¬ P' ⟹ g x' = g' x' ⟧
     ⟹ (if P then f else g) x = (if P' then f' else g') x'"
  by simp

lemma case_prod_apply_cong[fundef_cong]:
  "⟦ f (fst p) (snd p) s = f' (fst p') (snd p') s' ⟧ ⟹ case_prod f p s = case_prod f' p' s'"
  by (simp add: split_def)

definition
  pred_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl "and" 35)
where
  "pred_conj P Q ≡ λx. P x ∧ Q x"

definition
  pred_disj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl "or" 30)
where
  "pred_disj P Q ≡ λx. P x ∨ Q x"

definition
  pred_neg :: "('a ⇒ bool) ⇒ ('a ⇒ bool)" ("not _" [40] 40)
where
  "pred_neg P ≡ λx. ¬ P x"

definition "K ≡ λx y. x"

definition
  zipWith :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a list ⇒ 'b list ⇒ 'c list" where
  "zipWith f xs ys ≡ map (case_prod f) (zip xs ys)"

primrec
  delete :: "'a ⇒ 'a list ⇒ 'a list"
where
  "delete y [] = []"
| "delete y (x#xs) = (if y=x then xs else x # delete y xs)"

primrec
  find :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a option"
where
  "find f [] = None"
| "find f (x # xs) = (if f x then Some x else find f xs)"

definition
 "swp f ≡ λx y. f y x"

primrec (nonexhaustive)
  theRight :: "'a + 'b ⇒ 'b" where
  "theRight (Inr x) = x"

primrec (nonexhaustive)
  theLeft :: "'a + 'b ⇒ 'a" where
  "theLeft (Inl x) = x"

definition
 "isLeft x ≡ (∃y. x = Inl y)"

definition
 "isRight x ≡ (∃y. x = Inr y)"

definition
 "const x ≡ λy. x"

lemma tranclD2:
  "(x, y) ∈ R⇧+ ⟹ ∃z. (x, z) ∈ R⇧* ∧ (z, y) ∈ R"
  by (erule tranclE) auto

lemma linorder_min_same1 [simp]:
  "(min y x = y) = (y ≤ (x::'a::linorder))"
  by (auto simp: min_def linorder_not_less)

lemma linorder_min_same2 [simp]:
  "(min x y = y) = (y ≤ (x::'a::linorder))"
  by (auto simp: min_def linorder_not_le)

text ‹A combinator for pairing up well-formed relations.
        The divisor function splits the population in halves,
        with the True half greater than the False half, and
        the supplied relations control the order within the halves.›

definition
  wf_sum :: "('a ⇒ bool) ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where
  "wf_sum divisor r r' ≡
     ({(x, y). ¬ divisor x ∧ ¬ divisor y} ∩ r')
   ∪  {(x, y). ¬ divisor x ∧ divisor y}
   ∪ ({(x, y). divisor x ∧ divisor y} ∩ r)"

lemma wf_sum_wf:
  "⟦ wf r; wf r' ⟧ ⟹ wf (wf_sum divisor r r')"
  apply (simp add: wf_sum_def)
  apply (rule wf_Un)+
      apply (erule wf_Int2)
     apply (rule wf_subset
             [where r="measure (λx. If (divisor x) 1 0)"])
      apply simp
     apply clarsimp
    apply blast
   apply (erule wf_Int2)
  apply blast
  done

abbreviation(input)
 "option_map == map_option"

lemmas option_map_def = map_option_case

lemma False_implies_equals [simp]:
  "((False ⟹ P) ⟹ PROP Q) ≡ PROP Q"
  apply (rule equal_intr_rule)
   apply (erule meta_mp)
   apply simp
  apply simp
  done

lemma split_paired_Ball:
  "(∀x ∈ A. P x) = (∀x y. (x,y) ∈ A ⟶ P (x,y))"
  by auto

lemma split_paired_Bex:
  "(∃x ∈ A. P x) = (∃x y. (x,y) ∈ A ∧ P (x,y))"
  by auto

end