Theory Util_Set

(*  Title:      Util_Set.thy
    Date:       Feb 2008
    Author:     David Trachtenherz
*)

header {* Convenience results for set quantifiers *}

theory Util_Set
imports Fun Set
begin


subsection {* Some auxiliary results for HOL rules *}

lemma conj_disj_absorb: "(P ∧ Q ∨ Q) = Q" by blast
lemma disj_eq_distribL: "((a ∨ b) = (a ∨ c)) = (a ∨ (b = c))" by blast
lemma disj_eq_distribR: "((a ∨ c) = (b ∨ c)) = ((a = b) ∨ c)" by blast

subsubsection {* Some auxiliary results for  @{text Let} *}

lemma Let_swap: "f (let x=a in g x) = (let x=a in f (g x))" by simp

subsubsection {* Some auxiliary @{text "if"}-rules *}

thm if_P
lemma if_P': "[| P; x = z |] ==> (if P then x else y) = z" by simp
thm if_not_P
lemma if_not_P': "[| ¬ P; y = z |] ==> (if P then x else y) = z" by simp

lemma if_P_both: "[| Q x; Q y |] ==> Q (if P then x else y)" by simp
lemma if_P_both_in_set: "[| x ∈ s; y ∈ s |] ==> (if P then x else y) ∈ s" by simp

subsubsection {* Some auxiliary rules for function composition *}

lemma comp2_conv: "f1 o f2 = (λx. f1 (f2 x))" by (simp add: comp_def)
lemma comp3_conv: "f1 o f2 o f3 = (λx. f1 (f2 (f3 x)))" by (simp add: comp_def)



subsection {* Some auxiliary lemmata for quantifiers *}

subsubsection {* Auxiliary results for universal and existential quantifiers *}

lemma ball_cong2: "
  [| I ⊆ A; ∀x∈A. f x = g x |] ==> (∀x∈I. P (f x)) = (∀x∈I. P (g x))" by fastsimp
lemma bex_cong2: "
  [| I ⊆ A; ∀x∈I. f x = g x |] ==> (∃x∈I. P (f x)) = (∃x∈I. P (g x))" by simp
lemma ball_all_cong: "
  ∀x. f x = g x ==> (∀x∈I. P (f x)) = (∀x∈I. P (g x))" by simp
lemma bex_all_cong: "
  ∀x. f x = g x ==> (∃x∈I. P (f x)) = (∃x∈I. P (g x))" by simp
lemma all_cong: "
  ∀x. f x = g x ==> (∀x. P (f x)) = (∀x. P (g x))" by simp
lemma ex_cong: "
  ∀x. f x = g x ==> (∃x. P (f x)) = (∃x. P (g x))" by simp

(*lemma all_eqI: "(!!x. P x = Q x) ==> (∀x. P x) = (∀x. Q x)"*)
lemmas all_eqI = iff_allI
(*lemma ex_eqI: "(!!x. P x = Q x) ==> (∃x. P x) = (∃x. Q x)"*)
lemmas ex_eqI = iff_exI

lemma all_imp_eqI: "
  [| P = P'; !!x. P x ==> Q x = Q' x |] ==>
  (∀x. P x --> Q x) = (∀x. P' x --> Q' x)"
by blast
lemma ex_imp_eqI: "
  [| P = P'; !!x. P x ==> Q x = Q' x |] ==>
  (∃x. P x ∧ Q x) = (∃x. P' x ∧ Q' x)"
by blast




subsubsection {* Auxiliary results for @{text empty} sets *}

lemma empty_imp_not_in: "x ∉ {}" by blast
lemma ex_imp_not_empty: "∃x. x ∈ A ==> A ≠ {}" by blast
lemma in_imp_not_empty: "x ∈ A ==> A ≠ {}" by blast
lemma not_empty_imp_ex: "A ≠ {} ==> ∃x. x ∈ A" by blast
lemma not_ex_in_conv: "(¬ (∃x. x ∈ A)) = (A = {})" by blast




subsubsection {* Some auxiliary results for subset and membership relation *}

lemma bex_subset_imp_bex: "[| ∃x∈A. P x; A ⊆ B |] ==> ∃x∈B. P x" by blast
lemma bex_imp_ex: "∃x∈A. P x ==> ∃x. P x" by blast
lemma ball_subset_imp_ball: "[| ∀x∈B. P x; A ⊆ B |] ==> ∀x∈A. P x" by blast
thm 
  ball_subset_imp_ball
  ball_subset_imp_ball[rule_format]
lemma all_imp_ball: "∀x. P x ==> ∀x∈A. P x" by blast

thm mem_Collect_eq
lemma mem_Collect_eq_not: "(a ∉ {x. P x}) = (¬ P a)" by blast
lemma Collect_not_in_imp_not: "a ∉ {x. P x} ==> ¬ P a" by blast
lemma Collect_not_imp_not_in: "¬ P a ==> a ∉ {x. P x}" by blast
lemma Collect_is_subset: "{x ∈ A. P x} ⊆ A" by blast



end