Theory Util_Set

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

section ‹Convenience results for set quantifiers›

theory Util_Set
imports Main
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  ‹Let››

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


subsubsection ‹Some auxiliary ‹if›-rules›

lemma if_P': "⟦ P; x = z ⟧ ⟹ (if P then x else y) = z" by simp
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 ∘ f2 = (λx. f1 (f2 x))" by (simp add: comp_def)
lemma comp3_conv: "f1 ∘ f2 ∘ 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 fastforce
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 ‹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
lemma all_imp_ball: "∀x. P x ⟹ ∀x∈A. P x" by blast

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