Theory List-Infinite.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; xA. f x = g x   (xI. P (f x)) = (xI. P (g x))" by fastforce
lemma bex_cong2: "
   I  A; xI. f x = g x   (xI. P (f x)) = (xI. P (g x))" by simp
lemma ball_all_cong: "
  x. f x = g x  (xI. P (f x)) = (xI. P (g x))" by simp
lemma bex_all_cong: "
  x. f x = g x  (xI. P (f x)) = (xI. 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: " xA. P x; A  B   xB. P x" by blast
lemma bex_imp_ex: "xA. P x  x. P x" by blast
lemma ball_subset_imp_ball: " xB. P x; A  B   xA. P x" by blast
lemma all_imp_ball: "x. P x  xA. 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