(* Title: HOL/Set.thy ID: $Id: Set.thy,v 1.101 2005/09/29 10:43:40 paulson Exp $ Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel *) header {* Set theory for higher-order logic *} theory Set imports LOrder begin text {* A set in HOL is simply a predicate. *} subsection {* Basic syntax *} global typedecl 'a set arities set :: (type) type consts "{}" :: "'a set" ("{}") UNIV :: "'a set" insert :: "'a => 'a set => 'a set" Collect :: "('a => bool) => 'a set" -- "comprehension" Int :: "'a set => 'a set => 'a set" (infixl 70) Un :: "'a set => 'a set => 'a set" (infixl 65) UNION :: "'a set => ('a => 'b set) => 'b set" -- "general union" INTER :: "'a set => ('a => 'b set) => 'b set" -- "general intersection" Union :: "'a set set => 'a set" -- "union of a set" Inter :: "'a set set => 'a set" -- "intersection of a set" Pow :: "'a set => 'a set set" -- "powerset" Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers" Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers" image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) syntax "op :" :: "'a => 'a set => bool" ("op :") consts "op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership" local instance set :: (type) "{ord, minus}" .. subsection {* Additional concrete syntax *} syntax range :: "('a => 'b) => 'b set" -- "of function" "op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership" "op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) "@Finset" :: "args => 'a set" ("{(_)}") "@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") "@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})") "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})") "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10) "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10) "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10) "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) "_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10) syntax (HOL) "_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10) "_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10) translations "range f" == "f`UNIV" "x ~: y" == "~ (x : y)" "{x, xs}" == "insert x {xs}" "{x}" == "insert x {}" "{x. P}" == "Collect (%x. P)" "{x:A. P}" => "{x. x:A & P}" "UN x y. B" == "UN x. UN y. B" "UN x. B" == "UNION UNIV (%x. B)" "UN x. B" == "UN x:UNIV. B" "INT x y. B" == "INT x. INT y. B" "INT x. B" == "INTER UNIV (%x. B)" "INT x. B" == "INT x:UNIV. B" "UN x:A. B" == "UNION A (%x. B)" "INT x:A. B" == "INTER A (%x. B)" "ALL x:A. P" == "Ball A (%x. P)" "EX x:A. P" == "Bex A (%x. P)" syntax (output) "_setle" :: "'a set => 'a set => bool" ("op <=") "_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) "_setless" :: "'a set => 'a set => bool" ("op <") "_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50) syntax (xsymbols) "_setle" :: "'a set => 'a set => bool" ("op ⊆") "_setle" :: "'a set => 'a set => bool" ("(_/ ⊆ _)" [50, 51] 50) "_setless" :: "'a set => 'a set => bool" ("op ⊂") "_setless" :: "'a set => 'a set => bool" ("(_/ ⊂ _)" [50, 51] 50) "op Int" :: "'a set => 'a set => 'a set" (infixl "∩" 70) "op Un" :: "'a set => 'a set => 'a set" (infixl "∪" 65) "op :" :: "'a => 'a set => bool" ("op ∈") "op :" :: "'a => 'a set => bool" ("(_/ ∈ _)" [50, 51] 50) "op ~:" :: "'a => 'a set => bool" ("op ∉") "op ~:" :: "'a => 'a set => bool" ("(_/ ∉ _)" [50, 51] 50) Union :: "'a set set => 'a set" ("\<Union>_" [90] 90) Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90) "_Ball" :: "pttrn => 'a set => bool => bool" ("(3∀_∈_./ _)" [0, 0, 10] 10) "_Bex" :: "pttrn => 'a set => bool => bool" ("(3∃_∈_./ _)" [0, 0, 10] 10) syntax (HTML output) "_setle" :: "'a set => 'a set => bool" ("op ⊆") "_setle" :: "'a set => 'a set => bool" ("(_/ ⊆ _)" [50, 51] 50) "_setless" :: "'a set => 'a set => bool" ("op ⊂") "_setless" :: "'a set => 'a set => bool" ("(_/ ⊂ _)" [50, 51] 50) "op Int" :: "'a set => 'a set => 'a set" (infixl "∩" 70) "op Un" :: "'a set => 'a set => 'a set" (infixl "∪" 65) "op :" :: "'a => 'a set => bool" ("op ∈") "op :" :: "'a => 'a set => bool" ("(_/ ∈ _)" [50, 51] 50) "op ~:" :: "'a => 'a set => bool" ("op ∉") "op ~:" :: "'a => 'a set => bool" ("(_/ ∉ _)" [50, 51] 50) "_Ball" :: "pttrn => 'a set => bool => bool" ("(3∀_∈_./ _)" [0, 0, 10] 10) "_Bex" :: "pttrn => 'a set => bool => bool" ("(3∃_∈_./ _)" [0, 0, 10] 10) syntax (xsymbols) "@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ ∈/ _./ _})") "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10) "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_∈_./ _)" 10) "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_∈_./ _)" 10) (* syntax (xsymbols) "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00_)/ _)" 10) "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00_)/ _)" 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00_∈_)/ _)" 10) "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00_∈_)/ _)" 10) *) syntax (latex output) "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00_)/ _)" 10) "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00_)/ _)" 10) "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00_∈_)/ _)" 10) "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00_∈_)/ _)" 10) text{* Note the difference between ordinary xsymbol syntax of indexed unions and intersections (e.g.\ @{text"\<Union>a1∈A1. B"}) and their \LaTeX\ rendition: @{term"\<Union>a1∈A1. B"}. The former does not make the index expression a subscript of the union/intersection symbol because this leads to problems with nested subscripts in Proof General. *} translations "op ⊆" => "op <= :: _ set => _ set => bool" "op ⊂" => "op < :: _ set => _ set => bool" typed_print_translation {* let fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = list_comb (Syntax.const "_setle", ts) | le_tr' _ _ _ = raise Match; fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = list_comb (Syntax.const "_setless", ts) | less_tr' _ _ _ = raise Match; in [("op <=", le_tr'), ("op <", less_tr')] end *} subsubsection "Bounded quantifiers" syntax "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) "_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) "_setleEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) syntax (xsymbols) "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3∀_⊂_./ _)" [0, 0, 10] 10) "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3∃_⊂_./ _)" [0, 0, 10] 10) "_setleAll" :: "[idt, 'a, bool] => bool" ("(3∀_⊆_./ _)" [0, 0, 10] 10) "_setleEx" :: "[idt, 'a, bool] => bool" ("(3∃_⊆_./ _)" [0, 0, 10] 10) syntax (HOL) "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) "_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) "_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) syntax (HTML output) "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3∀_⊂_./ _)" [0, 0, 10] 10) "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3∃_⊂_./ _)" [0, 0, 10] 10) "_setleAll" :: "[idt, 'a, bool] => bool" ("(3∀_⊆_./ _)" [0, 0, 10] 10) "_setleEx" :: "[idt, 'a, bool] => bool" ("(3∃_⊆_./ _)" [0, 0, 10] 10) translations "∀A⊂B. P" => "ALL A. A ⊂ B --> P" "∃A⊂B. P" => "EX A. A ⊂ B & P" "∀A⊆B. P" => "ALL A. A ⊆ B --> P" "∃A⊆B. P" => "EX A. A ⊆ B & P" print_translation {* let fun all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = (if v=v' andalso T="set" then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P else raise Match) | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = (if v=v' andalso T="set" then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P else raise Match); fun ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = (if v=v' andalso T="set" then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P else raise Match) | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = (if v=v' andalso T="set" then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P else raise Match) in [("ALL ", all_tr'), ("EX ", ex_tr')] end *} text {* \medskip Translate between @{text "{e | x1...xn. P}"} and @{text "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is only translated if @{text "[0..n] subset bvs(e)"}. *} parse_translation {* let val ex_tr = snd (mk_binder_tr ("EX ", "Ex")); fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1 | nvars _ = 1; fun setcompr_tr [e, idts, b] = let val eq = Syntax.const "op =" $ Bound (nvars idts) $ e; val P = Syntax.const "op &" $ eq $ b; val exP = ex_tr [idts, P]; in Syntax.const "Collect" $ Abs ("", dummyT, exP) end; in [("@SetCompr", setcompr_tr)] end; *} (* To avoid eta-contraction of body: *) print_translation {* let fun btr' syn [A,Abs abs] = let val (x,t) = atomic_abs_tr' abs in Syntax.const syn $ x $ A $ t end in [("Ball", btr' "_Ball"),("Bex", btr' "_Bex"), ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")] end *} print_translation {* let val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY")); fun setcompr_tr' [Abs (abs as (_, _, P))] = let fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) | check _ = false fun tr' (_ $ abs) = let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] in Syntax.const "@SetCompr" $ e $ idts $ Q end; in if check (P, 0) then tr' P else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs val M = Syntax.const "@Coll" $ x $ t in case t of Const("op &",_) $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A) $ P => if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M | _ => M end end; in [("Collect", setcompr_tr')] end; *} subsection {* Rules and definitions *} text {* Isomorphisms between predicates and sets. *} axioms mem_Collect_eq: "(a : {x. P(x)}) = P(a)" Collect_mem_eq: "{x. x:A} = A" finalconsts Collect "op :" defs Ball_def: "Ball A P == ALL x. x:A --> P(x)" Bex_def: "Bex A P == EX x. x:A & P(x)" defs (overloaded) subset_def: "A <= B == ALL x:A. x:B" psubset_def: "A < B == (A::'a set) <= B & ~ A=B" Compl_def: "- A == {x. ~x:A}" set_diff_def: "A - B == {x. x:A & ~x:B}" defs Un_def: "A Un B == {x. x:A | x:B}" Int_def: "A Int B == {x. x:A & x:B}" INTER_def: "INTER A B == {y. ALL x:A. y: B(x)}" UNION_def: "UNION A B == {y. EX x:A. y: B(x)}" Inter_def: "Inter S == (INT x:S. x)" Union_def: "Union S == (UN x:S. x)" Pow_def: "Pow A == {B. B <= A}" empty_def: "{} == {x. False}" UNIV_def: "UNIV == {x. True}" insert_def: "insert a B == {x. x=a} Un B" image_def: "f`A == {y. EX x:A. y = f(x)}" subsection {* Lemmas and proof tool setup *} subsubsection {* Relating predicates and sets *} declare mem_Collect_eq [iff] Collect_mem_eq [simp] lemma CollectI: "P(a) ==> a : {x. P(x)}" by simp lemma CollectD: "a : {x. P(x)} ==> P(a)" by simp lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" by simp lemmas CollectE = CollectD [elim_format] subsubsection {* Bounded quantifiers *} lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" by (simp add: Ball_def) lemmas strip = impI allI ballI lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x" by (simp add: Ball_def) lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" by (unfold Ball_def) blast ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *} text {* \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and @{prop "a:A"}; creates assumption @{prop "P a"}. *} ML {* local val ballE = thm "ballE" in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end; *} text {* Gives better instantiation for bound: *} ML_setup {* claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1); *} lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" -- {* Normally the best argument order: @{prop "P x"} constrains the choice of @{prop "x:A"}. *} by (unfold Bex_def) blast lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x" -- {* The best argument order when there is only one @{prop "x:A"}. *} by (unfold Bex_def) blast lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" by (unfold Bex_def) blast lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q" by (unfold Bex_def) blast lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)" -- {* Trival rewrite rule. *} by (simp add: Ball_def) lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)" -- {* Dual form for existentials. *} by (simp add: Bex_def) lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)" by blast lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)" by blast lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)" by blast lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)" by blast lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)" by blast lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)" by blast ML_setup {* local val Ball_def = thm "Ball_def"; val Bex_def = thm "Bex_def"; val simpset = Simplifier.clear_ss HOL_basic_ss; fun unfold_tac ss th = ALLGOALS (full_simp_tac (Simplifier.inherit_bounds ss simpset addsimps [th])); fun prove_bex_tac ss = unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac; val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; fun prove_ball_tac ss = unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac; val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; in val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ())) "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ())) "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; end; Addsimprocs [defBALL_regroup, defBEX_regroup]; *} subsubsection {* Congruence rules *} lemma ball_cong: "A = B ==> (!!x. x:B ==> P x = Q x) ==> (ALL x:A. P x) = (ALL x:B. Q x)" by (simp add: Ball_def) lemma strong_ball_cong [cong]: "A = B ==> (!!x. x:B =simp=> P x = Q x) ==> (ALL x:A. P x) = (ALL x:B. Q x)" by (simp add: simp_implies_def Ball_def) lemma bex_cong: "A = B ==> (!!x. x:B ==> P x = Q x) ==> (EX x:A. P x) = (EX x:B. Q x)" by (simp add: Bex_def cong: conj_cong) lemma strong_bex_cong [cong]: "A = B ==> (!!x. x:B =simp=> P x = Q x) ==> (EX x:A. P x) = (EX x:B. Q x)" by (simp add: simp_implies_def Bex_def cong: conj_cong) subsubsection {* Subsets *} lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A ⊆ B" by (simp add: subset_def) text {* \medskip Map the type @{text "'a set => anything"} to just @{typ 'a}; for overloading constants whose first argument has type @{typ "'a set"}. *} lemma subsetD [elim]: "A ⊆ B ==> c ∈ A ==> c ∈ B" -- {* Rule in Modus Ponens style. *} by (unfold subset_def) blast declare subsetD [intro?] -- FIXME lemma rev_subsetD: "c ∈ A ==> A ⊆ B ==> c ∈ B" -- {* The same, with reversed premises for use with @{text erule} -- cf @{text rev_mp}. *} by (rule subsetD) declare rev_subsetD [intro?] -- FIXME text {* \medskip Converts @{prop "A ⊆ B"} to @{prop "x ∈ A ==> x ∈ B"}. *} ML {* local val rev_subsetD = thm "rev_subsetD" in fun impOfSubs th = th RSN (2, rev_subsetD) end; *} lemma subsetCE [elim]: "A ⊆ B ==> (c ∉ A ==> P) ==> (c ∈ B ==> P) ==> P" -- {* Classical elimination rule. *} by (unfold subset_def) blast text {* \medskip Takes assumptions @{prop "A ⊆ B"}; @{prop "c ∈ A"} and creates the assumption @{prop "c ∈ B"}. *} ML {* local val subsetCE = thm "subsetCE" in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; *} lemma contra_subsetD: "A ⊆ B ==> c ∉ B ==> c ∉ A" by blast lemma subset_refl: "A ⊆ A" by fast lemma subset_trans: "A ⊆ B ==> B ⊆ C ==> A ⊆ C" by blast subsubsection {* Equality *} lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B" apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals]) apply (rule Collect_mem_eq) apply (rule Collect_mem_eq) done (* Due to Brian Huffman *) lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))" by(auto intro:set_ext) lemma subset_antisym [intro!]: "A ⊆ B ==> B ⊆ A ==> A = B" -- {* Anti-symmetry of the subset relation. *} by (iprover intro: set_ext subsetD) lemmas equalityI [intro!] = subset_antisym text {* \medskip Equality rules from ZF set theory -- are they appropriate here? *} lemma equalityD1: "A = B ==> A ⊆ B" by (simp add: subset_refl) lemma equalityD2: "A = B ==> B ⊆ A" by (simp add: subset_refl) text {* \medskip Be careful when adding this to the claset as @{text subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} ⊆ A"} and @{prop "A ⊆ {}"} and then back to @{prop "A = {}"}! *} lemma equalityE: "A = B ==> (A ⊆ B ==> B ⊆ A ==> P) ==> P" by (simp add: subset_refl) lemma equalityCE [elim]: "A = B ==> (c ∈ A ==> c ∈ B ==> P) ==> (c ∉ A ==> c ∉ B ==> P) ==> P" by blast text {* \medskip Lemma for creating induction formulae -- for "pattern matching" on @{text p}. To make the induction hypotheses usable, apply @{text spec} or @{text bspec} to put universal quantifiers over the free variables in @{text p}. *} lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R" by simp lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)" by simp lemma eqelem_imp_iff: "x = y ==> (x : A) = (y : A)" by simp subsubsection {* The universal set -- UNIV *} lemma UNIV_I [simp]: "x : UNIV" by (simp add: UNIV_def) declare UNIV_I [intro] -- {* unsafe makes it less likely to cause problems *} lemma UNIV_witness [intro?]: "EX x. x : UNIV" by simp lemma subset_UNIV: "A ⊆ UNIV" by (rule subsetI) (rule UNIV_I) text {* \medskip Eta-contracting these two rules (to remove @{text P}) causes them to be ignored because of their interaction with congruence rules. *} lemma ball_UNIV [simp]: "Ball UNIV P = All P" by (simp add: Ball_def) lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" by (simp add: Bex_def) subsubsection {* The empty set *} lemma empty_iff [simp]: "(c : {}) = False" by (simp add: empty_def) lemma emptyE [elim!]: "a : {} ==> P" by simp lemma empty_subsetI [iff]: "{} ⊆ A" -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} by blast lemma equals0I: "(!!y. y ∈ A ==> False) ==> A = {}" by blast lemma equals0D: "A = {} ==> a ∉ A" -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} by blast lemma ball_empty [simp]: "Ball {} P = True" by (simp add: Ball_def) lemma bex_empty [simp]: "Bex {} P = False" by (simp add: Bex_def) lemma UNIV_not_empty [iff]: "UNIV ~= {}" by (blast elim: equalityE) subsubsection {* The Powerset operator -- Pow *} lemma Pow_iff [iff]: "(A ∈ Pow B) = (A ⊆ B)" by (simp add: Pow_def) lemma PowI: "A ⊆ B ==> A ∈ Pow B" by (simp add: Pow_def) lemma PowD: "A ∈ Pow B ==> A ⊆ B" by (simp add: Pow_def) lemma Pow_bottom: "{} ∈ Pow B" by simp lemma Pow_top: "A ∈ Pow A" by (simp add: subset_refl) subsubsection {* Set complement *} lemma Compl_iff [simp]: "(c ∈ -A) = (c ∉ A)" by (unfold Compl_def) blast lemma ComplI [intro!]: "(c ∈ A ==> False) ==> c ∈ -A" by (unfold Compl_def) blast text {* \medskip This form, with negated conclusion, works well with the Classical prover. Negated assumptions behave like formulae on the right side of the notional turnstile ... *} lemma ComplD [dest!]: "c : -A ==> c~:A" by (unfold Compl_def) blast lemmas ComplE = ComplD [elim_format] subsubsection {* Binary union -- Un *} lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)" by (unfold Un_def) blast lemma UnI1 [elim?]: "c:A ==> c : A Un B" by simp lemma UnI2 [elim?]: "c:B ==> c : A Un B" by simp text {* \medskip Classical introduction rule: no commitment to @{prop A} vs @{prop B}. *} lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B" by auto lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P" by (unfold Un_def) blast subsubsection {* Binary intersection -- Int *} lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)" by (unfold Int_def) blast lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B" by simp lemma IntD1: "c : A Int B ==> c:A" by simp lemma IntD2: "c : A Int B ==> c:B" by simp lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P" by simp subsubsection {* Set difference *} lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)" by (unfold set_diff_def) blast lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B" by simp lemma DiffD1: "c : A - B ==> c : A" by simp lemma DiffD2: "c : A - B ==> c : B ==> P" by simp lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P" by simp subsubsection {* Augmenting a set -- insert *} lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)" by (unfold insert_def) blast lemma insertI1: "a : insert a B" by simp lemma insertI2: "a : B ==> a : insert b B" by simp lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P" by (unfold insert_def) blast lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B" -- {* Classical introduction rule. *} by auto lemma subset_insert_iff: "(A ⊆ insert x B) = (if x:A then A - {x} ⊆ B else A ⊆ B)" by auto subsubsection {* Singletons, using insert *} lemma singletonI [intro!]: "a : {a}" -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *} by (rule insertI1) lemma singletonD [dest!]: "b : {a} ==> b = a" by blast lemmas singletonE = singletonD [elim_format] lemma singleton_iff: "(b : {a}) = (b = a)" by blast lemma singleton_inject [dest!]: "{a} = {b} ==> a = b" by blast lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A ⊆ {b})" by blast lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A ⊆ {b})" by blast lemma subset_singletonD: "A ⊆ {x} ==> A = {} | A = {x}" by fast lemma singleton_conv [simp]: "{x. x = a} = {a}" by blast lemma singleton_conv2 [simp]: "{x. a = x} = {a}" by blast lemma diff_single_insert: "A - {x} ⊆ B ==> x ∈ A ==> A ⊆ insert x B" by blast subsubsection {* Unions of families *} text {* @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}. *} lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)" by (unfold UNION_def) blast lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)" -- {* The order of the premises presupposes that @{term A} is rigid; @{term b} may be flexible. *} by auto lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R" by (unfold UNION_def) blast lemma UN_cong [cong]: "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" by (simp add: UNION_def) subsubsection {* Intersections of families *} text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" by (unfold INTER_def) blast lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" by (unfold INTER_def) blast lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" by auto lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *} by (unfold INTER_def) blast lemma INT_cong [cong]: "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" by (simp add: INTER_def) subsubsection {* Union *} lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)" by (unfold Union_def) blast lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C" -- {* The order of the premises presupposes that @{term C} is rigid; @{term A} may be flexible. *} by auto lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R" by (unfold Union_def) blast subsubsection {* Inter *} lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)" by (unfold Inter_def) blast lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" by (simp add: Inter_def) text {* \medskip A ``destruct'' rule -- every @{term X} in @{term C} contains @{term A} as an element, but @{prop "A:X"} can hold when @{prop "X:C"} does not! This rule is analogous to @{text spec}. *} lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" by auto lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" -- {* ``Classical'' elimination rule -- does not require proving @{prop "X:C"}. *} by (unfold Inter_def) blast text {* \medskip Image of a set under a function. Frequently @{term b} does not have the syntactic form of @{term "f x"}. *} lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A" by (unfold image_def) blast lemma imageI: "x : A ==> f x : f ` A" by (rule image_eqI) (rule refl) lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A" -- {* This version's more effective when we already have the required @{term x}. *} by (unfold image_def) blast lemma imageE [elim!]: "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P" -- {* The eta-expansion gives variable-name preservation. *} by (unfold image_def) blast lemma image_Un: "f`(A Un B) = f`A Un f`B" by blast lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" by blast lemma image_subset_iff: "(f`A ⊆ B) = (∀x∈A. f x ∈ B)" -- {* This rewrite rule would confuse users if made default. *} by blast lemma subset_image_iff: "(B ⊆ f`A) = (EX AA. AA ⊆ A & B = f`AA)" apply safe prefer 2 apply fast apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast) done lemma image_subsetI: "(!!x. x ∈ A ==> f x ∈ B) ==> f`A ⊆ B" -- {* Replaces the three steps @{text subsetI}, @{text imageE}, @{text hypsubst}, but breaks too many existing proofs. *} by blast text {* \medskip Range of a function -- just a translation for image! *} lemma range_eqI: "b = f x ==> b ∈ range f" by simp lemma rangeI: "f x ∈ range f" by simp lemma rangeE [elim?]: "b ∈ range (λx. f x) ==> (!!x. b = f x ==> P) ==> P" by blast subsubsection {* Set reasoning tools *} text {* Rewrite rules for boolean case-splitting: faster than @{text "split_if [split]"}. *} lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))" by (rule split_if) lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))" by (rule split_if) text {* Split ifs on either side of the membership relation. Not for @{text "[simp]"} -- can cause goals to blow up! *} lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))" by (rule split_if) lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))" by (rule split_if) lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 lemmas mem_simps = insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} (*Would like to add these, but the existing code only searches for the outer-level constant, which in this case is just "op :"; we instead need to use term-nets to associate patterns with rules. Also, if a rule fails to apply, then the formula should be kept. [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]), ("op Int", [IntD1,IntD2]), ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] *) ML_setup {* val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs; simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs); *} declare subset_UNIV [simp] subset_refl [simp] subsubsection {* The ``proper subset'' relation *} lemma psubsetI [intro!]: "A ⊆ B ==> A ≠ B ==> A ⊂ B" by (unfold psubset_def) blast lemma psubsetE [elim!]: "[|A ⊂ B; [|A ⊆ B; ~ (B⊆A)|] ==> R|] ==> R" by (unfold psubset_def) blast lemma psubset_insert_iff: "(A ⊂ insert x B) = (if x ∈ B then A ⊂ B else if x ∈ A then A - {x} ⊂ B else A ⊆ B)" by (auto simp add: psubset_def subset_insert_iff) lemma psubset_eq: "(A ⊂ B) = (A ⊆ B & A ≠ B)" by (simp only: psubset_def) lemma psubset_imp_subset: "A ⊂ B ==> A ⊆ B" by (simp add: psubset_eq) lemma psubset_trans: "[| A ⊂ B; B ⊂ C |] ==> A ⊂ C" apply (unfold psubset_def) apply (auto dest: subset_antisym) done lemma psubsetD: "[| A ⊂ B; c ∈ A |] ==> c ∈ B" apply (unfold psubset_def) apply (auto dest: subsetD) done lemma psubset_subset_trans: "A ⊂ B ==> B ⊆ C ==> A ⊂ C" by (auto simp add: psubset_eq) lemma subset_psubset_trans: "A ⊆ B ==> B ⊂ C ==> A ⊂ C" by (auto simp add: psubset_eq) lemma psubset_imp_ex_mem: "A ⊂ B ==> ∃b. b ∈ (B - A)" by (unfold psubset_def) blast lemma atomize_ball: "(!!x. x ∈ A ==> P x) == Trueprop (∀x∈A. P x)" by (simp only: Ball_def atomize_all atomize_imp) declare atomize_ball [symmetric, rulify] subsection {* Further set-theory lemmas *} subsubsection {* Derived rules involving subsets. *} text {* @{text insert}. *} lemma subset_insertI: "B ⊆ insert a B" apply (rule subsetI) apply (erule insertI2) done lemma subset_insertI2: "A ⊆ B ==> A ⊆ insert b B" by blast lemma subset_insert: "x ∉ A ==> (A ⊆ insert x B) = (A ⊆ B)" by blast text {* \medskip Big Union -- least upper bound of a set. *} lemma Union_upper: "B ∈ A ==> B ⊆ Union A" by (iprover intro: subsetI UnionI) lemma Union_least: "(!!X. X ∈ A ==> X ⊆ C) ==> Union A ⊆ C" by (iprover intro: subsetI elim: UnionE dest: subsetD) text {* \medskip General union. *} lemma UN_upper: "a ∈ A ==> B a ⊆ (\<Union>x∈A. B x)" by blast lemma UN_least: "(!!x. x ∈ A ==> B x ⊆ C) ==> (\<Union>x∈A. B x) ⊆ C" by (iprover intro: subsetI elim: UN_E dest: subsetD) text {* \medskip Big Intersection -- greatest lower bound of a set. *} lemma Inter_lower: "B ∈ A ==> Inter A ⊆ B" by blast lemma Inter_subset: "[| !!X. X ∈ A ==> X ⊆ B; A ~= {} |] ==> \<Inter>A ⊆ B" by blast lemma Inter_greatest: "(!!X. X ∈ A ==> C ⊆ X) ==> C ⊆ Inter A" by (iprover intro: InterI subsetI dest: subsetD) lemma INT_lower: "a ∈ A ==> (\<Inter>x∈A. B x) ⊆ B a" by blast lemma INT_greatest: "(!!x. x ∈ A ==> C ⊆ B x) ==> C ⊆ (\<Inter>x∈A. B x)" by (iprover intro: INT_I subsetI dest: subsetD) text {* \medskip Finite Union -- the least upper bound of two sets. *} lemma Un_upper1: "A ⊆ A ∪ B" by blast lemma Un_upper2: "B ⊆ A ∪ B" by blast lemma Un_least: "A ⊆ C ==> B ⊆ C ==> A ∪ B ⊆ C" by blast text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *} lemma Int_lower1: "A ∩ B ⊆ A" by blast lemma Int_lower2: "A ∩ B ⊆ B" by blast lemma Int_greatest: "C ⊆ A ==> C ⊆ B ==> C ⊆ A ∩ B" by blast text {* \medskip Set difference. *} lemma Diff_subset: "A - B ⊆ A" by blast lemma Diff_subset_conv: "(A - B ⊆ C) = (A ⊆ B ∪ C)" by blast text {* \medskip Monotonicity. *} lemma mono_Un: "mono f ==> f A ∪ f B ⊆ f (A ∪ B)" by (auto simp add: mono_def) lemma mono_Int: "mono f ==> f (A ∩ B) ⊆ f A ∩ f B" by (auto simp add: mono_def) subsubsection {* Equalities involving union, intersection, inclusion, etc. *} text {* @{text "{}"}. *} lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})" -- {* supersedes @{text "Collect_False_empty"} *} by auto lemma subset_empty [simp]: "(A ⊆ {}) = (A = {})" by blast lemma not_psubset_empty [iff]: "¬ (A < {})" by (unfold psubset_def) blast lemma Collect_empty_eq [simp]: "(Collect P = {}) = (∀x. ¬ P x)" by auto lemma Collect_neg_eq: "{x. ¬ P x} = - {x. P x}" by blast lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} ∪ {x. Q x}" by blast lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} ∪ {x. Q x}" by blast lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} ∩ {x. Q x}" by blast lemma Collect_all_eq: "{x. ∀y. P x y} = (\<Inter>y. {x. P x y})" by blast lemma Collect_ball_eq: "{x. ∀y∈A. P x y} = (\<Inter>y∈A. {x. P x y})" by blast lemma Collect_ex_eq: "{x. ∃y. P x y} = (\<Union>y. {x. P x y})" by blast lemma Collect_bex_eq: "{x. ∃y∈A. P x y} = (\<Union>y∈A. {x. P x y})" by blast text {* \medskip @{text insert}. *} lemma insert_is_Un: "insert a A = {a} Un A" -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *} by blast lemma insert_not_empty [simp]: "insert a A ≠ {}" by blast lemmas empty_not_insert = insert_not_empty [symmetric, standard] declare empty_not_insert [simp] lemma insert_absorb: "a ∈ A ==> insert a A = A" -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *} -- {* with \emph{quadratic} running time *} by blast lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A" by blast lemma insert_commute: "insert x (insert y A) = insert y (insert x A)" by blast lemma insert_subset [simp]: "(insert x A ⊆ B) = (x ∈ B & A ⊆ B)" by blast lemma mk_disjoint_insert: "a ∈ A ==> ∃B. A = insert a B & a ∉ B" -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *} apply (rule_tac x = "A - {a}" in exI, blast) done lemma insert_Collect: "insert a (Collect P) = {u. u ≠ a --> P u}" by auto lemma UN_insert_distrib: "u ∈ A ==> (\<Union>x∈A. insert a (B x)) = insert a (\<Union>x∈A. B x)" by blast lemma insert_inter_insert[simp]: "insert a A ∩ insert a B = insert a (A ∩ B)" by blast lemma insert_disjoint[simp]: "(insert a A ∩ B = {}) = (a ∉ B ∧ A ∩ B = {})" "({} = insert a A ∩ B) = (a ∉ B ∧ {} = A ∩ B)" by auto lemma disjoint_insert[simp]: "(B ∩ insert a A = {}) = (a ∉ B ∧ B ∩ A = {})" "({} = A ∩ insert b B) = (b ∉ A ∧ {} = A ∩ B)" by auto text {* \medskip @{text image}. *} lemma image_empty [simp]: "f`{} = {}" by blast lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)" by blast lemma image_constant: "x ∈ A ==> (λx. c) ` A = {c}" by auto lemma image_image: "f ` (g ` A) = (λx. f (g x)) ` A" by blast lemma insert_image [simp]: "x ∈ A ==> insert (f x) (f`A) = f`A" by blast lemma image_is_empty [iff]: "(f`A = {}) = (A = {})" by blast lemma image_Collect: "f ` {x. P x} = {f x | x. P x}" -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, with its implicit quantifier and conjunction. Also image enjoys better equational properties than does the RHS. *} by blast lemma if_image_distrib [simp]: "(λx. if P x then f x else g x) ` S = (f ` (S ∩ {x. P x})) ∪ (g ` (S ∩ {x. ¬ P x}))" by (auto simp add: image_def) lemma image_cong: "M = N ==> (!!x. x ∈ N ==> f x = g x) ==> f`M = g`N" by (simp add: image_def) text {* \medskip @{text range}. *} lemma full_SetCompr_eq: "{u. ∃x. u = f x} = range f" by auto lemma range_composition [simp]: "range (λx. f (g x)) = f`range g" by (subst image_image, simp) text {* \medskip @{text Int} *} lemma Int_absorb [simp]: "A ∩ A = A" by blast lemma Int_left_absorb: "A ∩ (A ∩ B) = A ∩ B" by blast lemma Int_commute: "A ∩ B = B ∩ A" by blast lemma Int_left_commute: "A ∩ (B ∩ C) = B ∩ (A ∩ C)" by blast lemma Int_assoc: "(A ∩ B) ∩ C = A ∩ (B ∩ C)" by blast lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute -- {* Intersection is an AC-operator *} lemma Int_absorb1: "B ⊆ A ==> A ∩ B = B" by blast lemma Int_absorb2: "A ⊆ B ==> A ∩ B = A" by blast lemma Int_empty_left [simp]: "{} ∩ B = {}" by blast lemma Int_empty_right [simp]: "A ∩ {} = {}" by blast lemma disjoint_eq_subset_Compl: "(A ∩ B = {}) = (A ⊆ -B)" by blast lemma disjoint_iff_not_equal: "(A ∩ B = {}) = (∀x∈A. ∀y∈B. x ≠ y)" by blast lemma Int_UNIV_left [simp]: "UNIV ∩ B = B" by blast lemma Int_UNIV_right [simp]: "A ∩ UNIV = A" by blast lemma Int_eq_Inter: "A ∩ B = \<Inter>{A, B}" by blast lemma Int_Un_distrib: "A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)" by blast lemma Int_Un_distrib2: "(B ∪ C) ∩ A = (B ∩ A) ∪ (C ∩ A)" by blast lemma Int_UNIV [simp]: "(A ∩ B = UNIV) = (A = UNIV & B = UNIV)" by blast lemma Int_subset_iff [simp]: "(C ⊆ A ∩ B) = (C ⊆ A & C ⊆ B)" by blast lemma Int_Collect: "(x ∈ A ∩ {x. P x}) = (x ∈ A & P x)" by blast text {* \medskip @{text Un}. *} lemma Un_absorb [simp]: "A ∪ A = A" by blast lemma Un_left_absorb: "A ∪ (A ∪ B) = A ∪ B" by blast lemma Un_commute: "A ∪ B = B ∪ A" by blast lemma Un_left_commute: "A ∪ (B ∪ C) = B ∪ (A ∪ C)" by blast lemma Un_assoc: "(A ∪ B) ∪ C = A ∪ (B ∪ C)" by blast lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute -- {* Union is an AC-operator *} lemma Un_absorb1: "A ⊆ B ==> A ∪ B = B" by blast lemma Un_absorb2: "B ⊆ A ==> A ∪ B = A" by blast lemma Un_empty_left [simp]: "{} ∪ B = B" by blast lemma Un_empty_right [simp]: "A ∪ {} = A" by blast lemma Un_UNIV_left [simp]: "UNIV ∪ B = UNIV" by blast lemma Un_UNIV_right [simp]: "A ∪ UNIV = UNIV" by blast lemma Un_eq_Union: "A ∪ B = \<Union>{A, B}" by blast lemma Un_insert_left [simp]: "(insert a B) ∪ C = insert a (B ∪ C)" by blast lemma Un_insert_right [simp]: "A ∪ (insert a B) = insert a (A ∪ B)" by blast lemma Int_insert_left: "(insert a B) Int C = (if a ∈ C then insert a (B ∩ C) else B ∩ C)" by auto lemma Int_insert_right: "A ∩ (insert a B) = (if a ∈ A then insert a (A ∩ B) else A ∩ B)" by auto lemma Un_Int_distrib: "A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)" by blast lemma Un_Int_distrib2: "(B ∩ C) ∪ A = (B ∪ A) ∩ (C ∪ A)" by blast lemma Un_Int_crazy: "(A ∩ B) ∪ (B ∩ C) ∪ (C ∩ A) = (A ∪ B) ∩ (B ∪ C) ∩ (C ∪ A)" by blast lemma subset_Un_eq: "(A ⊆ B) = (A ∪ B = B)" by blast lemma Un_empty [iff]: "(A ∪ B = {}) = (A = {} & B = {})" by blast lemma Un_subset_iff [simp]: "(A ∪ B ⊆ C) = (A ⊆ C & B ⊆ C)" by blast lemma Un_Diff_Int: "(A - B) ∪ (A ∩ B) = A" by blast text {* \medskip Set complement *} lemma Compl_disjoint [simp]: "A ∩ -A = {}" by blast lemma Compl_disjoint2 [simp]: "-A ∩ A = {}" by blast lemma Compl_partition: "A ∪ -A = UNIV" by blast lemma Compl_partition2: "-A ∪ A = UNIV" by blast lemma double_complement [simp]: "- (-A) = (A::'a set)" by blast lemma Compl_Un [simp]: "-(A ∪ B) = (-A) ∩ (-B)" by blast lemma Compl_Int [simp]: "-(A ∩ B) = (-A) ∪ (-B)" by blast lemma Compl_UN [simp]: "-(\<Union>x∈A. B x) = (\<Inter>x∈A. -B x)" by blast lemma Compl_INT [simp]: "-(\<Inter>x∈A. B x) = (\<Union>x∈A. -B x)" by blast lemma subset_Compl_self_eq: "(A ⊆ -A) = (A = {})" by blast lemma Un_Int_assoc_eq: "((A ∩ B) ∪ C = A ∩ (B ∪ C)) = (C ⊆ A)" -- {* Halmos, Naive Set Theory, page 16. *} by blast lemma Compl_UNIV_eq [simp]: "-UNIV = {}" by blast lemma Compl_empty_eq [simp]: "-{} = UNIV" by blast lemma Compl_subset_Compl_iff [iff]: "(-A ⊆ -B) = (B ⊆ A)" by blast lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))" by blast text {* \medskip @{text Union}. *} lemma Union_empty [simp]: "Union({}) = {}" by blast lemma Union_UNIV [simp]: "Union UNIV = UNIV" by blast lemma Union_insert [simp]: "Union (insert a B) = a ∪ \<Union>B" by blast lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A ∪ \<Union>B" by blast lemma Union_Int_subset: "\<Union>(A ∩ B) ⊆ \<Union>A ∩ \<Union>B" by blast lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (∀x∈A. x = {})" by blast lemma empty_Union_conv [iff]: "({} = \<Union>A) = (∀x∈A. x = {})" by blast lemma Union_disjoint: "(\<Union>C ∩ A = {}) = (∀B∈C. B ∩ A = {})" by blast text {* \medskip @{text Inter}. *} lemma Inter_empty [simp]: "\<Inter>{} = UNIV" by blast lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}" by blast lemma Inter_insert [simp]: "\<Inter>(insert a B) = a ∩ \<Inter>B" by blast lemma Inter_Un_subset: "\<Inter>A ∪ \<Inter>B ⊆ \<Inter>(A ∩ B)" by blast lemma Inter_Un_distrib: "\<Inter>(A ∪ B) = \<Inter>A ∩ \<Inter>B" by blast lemma Inter_UNIV_conv [iff]: "(\<Inter>A = UNIV) = (∀x∈A. x = UNIV)" "(UNIV = \<Inter>A) = (∀x∈A. x = UNIV)" by blast+ text {* \medskip @{text UN} and @{text INT}. Basic identities: *} lemma UN_empty [simp]: "(\<Union>x∈{}. B x) = {}" by blast lemma UN_empty2 [simp]: "(\<Union>x∈A. {}) = {}" by blast lemma UN_singleton [simp]: "(\<Union>x∈A. {x}) = A" by blast lemma UN_absorb: "k ∈ I ==> A k ∪ (\<Union>i∈I. A i) = (\<Union>i∈I. A i)" by auto lemma INT_empty [simp]: "(\<Inter>x∈{}. B x) = UNIV" by blast lemma INT_absorb: "k ∈ I ==> A k ∩ (\<Inter>i∈I. A i) = (\<Inter>i∈I. A i)" by blast lemma UN_insert [simp]: "(\<Union>x∈insert a A. B x) = B a ∪ UNION A B" by blast lemma UN_Un: "(\<Union>i ∈ A ∪ B. M i) = (\<Union>i∈A. M i) ∪ (\<Union>i∈B. M i)" by blast lemma UN_UN_flatten: "(\<Union>x ∈ (\<Union>y∈A. B y). C x) = (\<Union>y∈A. \<Union>x∈B y. C x)" by blast lemma UN_subset_iff: "((\<Union>i∈I. A i) ⊆ B) = (∀i∈I. A i ⊆ B)" by blast lemma INT_subset_iff: "(B ⊆ (\<Inter>i∈I. A i)) = (∀i∈I. B ⊆ A i)" by blast lemma INT_insert [simp]: "(\<Inter>x ∈ insert a A. B x) = B a ∩ INTER A B" by blast lemma INT_Un: "(\<Inter>i ∈ A ∪ B. M i) = (\<Inter>i ∈ A. M i) ∩ (\<Inter>i∈B. M i)" by blast lemma INT_insert_distrib: "u ∈ A ==> (\<Inter>x∈A. insert a (B x)) = insert a (\<Inter>x∈A. B x)" by blast lemma Union_image_eq [simp]: "\<Union>(B`A) = (\<Union>x∈A. B x)" by blast lemma image_Union: "f ` \<Union>S = (\<Union>x∈S. f ` x)" by blast lemma Inter_image_eq [simp]: "\<Inter>(B`A) = (\<Inter>x∈A. B x)" by blast lemma UN_constant [simp]: "(\<Union>y∈A. c) = (if A = {} then {} else c)" by auto lemma INT_constant [simp]: "(\<Inter>y∈A. c) = (if A = {} then UNIV else c)" by auto lemma UN_eq: "(\<Union>x∈A. B x) = \<Union>({Y. ∃x∈A. Y = B x})" by blast lemma INT_eq: "(\<Inter>x∈A. B x) = \<Inter>({Y. ∃x∈A. Y = B x})" -- {* Look: it has an \emph{existential} quantifier *} by blast lemma UNION_empty_conv[iff]: "({} = (UN x:A. B x)) = (∀x∈A. B x = {})" "((UN x:A. B x) = {}) = (∀x∈A. B x = {})" by blast+ lemma INTER_UNIV_conv[iff]: "(UNIV = (INT x:A. B x)) = (∀x∈A. B x = UNIV)" "((INT x:A. B x) = UNIV) = (∀x∈A. B x = UNIV)" by blast+ text {* \medskip Distributive laws: *} lemma Int_Union: "A ∩ \<Union>B = (\<Union>C∈B. A ∩ C)" by blast lemma Int_Union2: "\<Union>B ∩ A = (\<Union>C∈B. C ∩ A)" by blast lemma Un_Union_image: "(\<Union>x∈C. A x ∪ B x) = \<Union>(A`C) ∪ \<Union>(B`C)" -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *} -- {* Union of a family of unions *} by blast lemma UN_Un_distrib: "(\<Union>i∈I. A i ∪ B i) = (\<Union>i∈I. A i) ∪ (\<Union>i∈I. B i)" -- {* Equivalent version *} by blast lemma Un_Inter: "A ∪ \<Inter>B = (\<Inter>C∈B. A ∪ C)" by blast lemma Int_Inter_image: "(\<Inter>x∈C. A x ∩ B x) = \<Inter>(A`C) ∩ \<Inter>(B`C)" by blast lemma INT_Int_distrib: "(\<Inter>i∈I. A i ∩ B i) = (\<Inter>i∈I. A i) ∩ (\<Inter>i∈I. B i)" -- {* Equivalent version *} by blast lemma Int_UN_distrib: "B ∩ (\<Union>i∈I. A i) = (\<Union>i∈I. B ∩ A i)" -- {* Halmos, Naive Set Theory, page 35. *} by blast lemma Un_INT_distrib: "B ∪ (\<Inter>i∈I. A i) = (\<Inter>i∈I. B ∪ A i)" by blast lemma Int_UN_distrib2: "(\<Union>i∈I. A i) ∩ (\<Union>j∈J. B j) = (\<Union>i∈I. \<Union>j∈J. A i ∩ B j)" by blast lemma Un_INT_distrib2: "(\<Inter>i∈I. A i) ∪ (\<Inter>j∈J. B j) = (\<Inter>i∈I. \<Inter>j∈J. A i ∪ B j)" by blast text {* \medskip Bounded quantifiers. The following are not added to the default simpset because (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *} lemma ball_Un: "(∀x ∈ A ∪ B. P x) = ((∀x∈A. P x) & (∀x∈B. P x))" by blast lemma bex_Un: "(∃x ∈ A ∪ B. P x) = ((∃x∈A. P x) | (∃x∈B. P x))" by blast lemma ball_UN: "(∀z ∈ UNION A B. P z) = (∀x∈A. ∀z ∈ B x. P z)" by blast lemma bex_UN: "(∃z ∈ UNION A B. P z) = (∃x∈A. ∃z∈B x. P z)" by blast text {* \medskip Set difference. *} lemma Diff_eq: "A - B = A ∩ (-B)" by blast lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A ⊆ B)" by blast lemma Diff_cancel [simp]: "A - A = {}" by blast lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)" by blast lemma Diff_triv: "A ∩ B = {} ==> A - B = A" by (blast elim: equalityE) lemma empty_Diff [simp]: "{} - A = {}" by blast lemma Diff_empty [simp]: "A - {} = A" by blast lemma Diff_UNIV [simp]: "A - UNIV = {}" by blast lemma Diff_insert0 [simp]: "x ∉ A ==> A - insert x B = A - B" by blast lemma Diff_insert: "A - insert a B = A - B - {a}" -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *} by blast lemma Diff_insert2: "A - insert a B = A - {a} - B" -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *} by blast lemma insert_Diff_if: "insert x A - B = (if x ∈ B then A - B else insert x (A - B))" by auto lemma insert_Diff1 [simp]: "x ∈ B ==> insert x A - B = A - B" by blast lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A" by blast lemma insert_Diff: "a ∈ A ==> insert a (A - {a}) = A" by blast lemma Diff_insert_absorb: "x ∉ A ==> (insert x A) - {x} = A" by auto lemma Diff_disjoint [simp]: "A ∩ (B - A) = {}" by blast lemma Diff_partition: "A ⊆ B ==> A ∪ (B - A) = B" by blast lemma double_diff: "A ⊆ B ==> B ⊆ C ==> B - (C - A) = A" by blast lemma Un_Diff_cancel [simp]: "A ∪ (B - A) = A ∪ B" by blast lemma Un_Diff_cancel2 [simp]: "(B - A) ∪ A = B ∪ A" by blast lemma Diff_Un: "A - (B ∪ C) = (A - B) ∩ (A - C)" by blast lemma Diff_Int: "A - (B ∩ C) = (A - B) ∪ (A - C)" by blast lemma Un_Diff: "(A ∪ B) - C = (A - C) ∪ (B - C)" by blast lemma Int_Diff: "(A ∩ B) - C = A ∩ (B - C)" by blast lemma Diff_Int_distrib: "C ∩ (A - B) = (C ∩ A) - (C ∩ B)" by blast lemma Diff_Int_distrib2: "(A - B) ∩ C = (A ∩ C) - (B ∩ C)" by blast lemma Diff_Compl [simp]: "A - (- B) = A ∩ B" by auto lemma Compl_Diff_eq [simp]: "- (A - B) = -A ∪ B" by blast text {* \medskip Quantification over type @{typ bool}. *} lemma all_bool_eq: "(∀b::bool. P b) = (P True & P False)" apply auto apply (tactic {* case_tac "b" 1 *}, auto) done lemma bool_induct: "P True ==> P False ==> P x" by (rule conjI [THEN all_bool_eq [THEN iffD2], THEN spec]) lemma ex_bool_eq: "(∃b::bool. P b) = (P True | P False)" apply auto apply (tactic {* case_tac "b" 1 *}, auto) done lemma Un_eq_UN: "A ∪ B = (\<Union>b. if b then A else B)" by (auto simp add: split_if_mem2) lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True ∪ A False)" apply auto apply (tactic {* case_tac "b" 1 *}, auto) done lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True ∩ A False)" apply auto apply (tactic {* case_tac "b" 1 *}, auto) done text {* \medskip @{text Pow} *} lemma Pow_empty [simp]: "Pow {} = {{}}" by (auto simp add: Pow_def) lemma Pow_insert: "Pow (insert a A) = Pow A ∪ (insert a ` Pow A)" by (blast intro: image_eqI [where ?x = "u - {a}", standard]) lemma Pow_Compl: "Pow (- A) = {-B | B. A ∈ Pow B}" by (blast intro: exI [where ?x = "- u", standard]) lemma Pow_UNIV [simp]: "Pow UNIV = UNIV" by blast lemma Un_Pow_subset: "Pow A ∪ Pow B ⊆ Pow (A ∪ B)" by blast lemma UN_Pow_subset: "(\<Union>x∈A. Pow (B x)) ⊆ Pow (\<Union>x∈A. B x)" by blast lemma subset_Pow_Union: "A ⊆ Pow (\<Union>A)" by blast lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A" by blast lemma Pow_Int_eq [simp]: "Pow (A ∩ B) = Pow A ∩ Pow B" by blast lemma Pow_INT_eq: "Pow (\<Inter>x∈A. B x) = (\<Inter>x∈A. Pow (B x))" by blast text {* \medskip Miscellany. *} lemma set_eq_subset: "(A = B) = (A ⊆ B & B ⊆ A)" by blast lemma subset_iff: "(A ⊆ B) = (∀t. t ∈ A --> t ∈ B)" by blast lemma subset_iff_psubset_eq: "(A ⊆ B) = ((A ⊂ B) | (A = B))" by (unfold psubset_def) blast lemma all_not_in_conv [iff]: "(∀x. x ∉ A) = (A = {})" by blast lemma ex_in_conv: "(∃x. x ∈ A) = (A ≠ {})" by blast lemma distinct_lemma: "f x ≠ f y ==> x ≠ y" by iprover text {* \medskip Miniscoping: pushing in quantifiers and big Unions and Intersections. *} lemma UN_simps [simp]: "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))" "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))" "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))" "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)" "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))" "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)" "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))" "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)" "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)" "!!A B f. (UN x:f`A. B x) = (UN a:A. B (f a))" by auto lemma INT_simps [simp]: "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)" "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))" "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)" "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))" "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)" "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)" "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))" "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)" "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)" "!!A B f. (INT x:f`A. B x) = (INT a:A. B (f a))" by auto lemma ball_simps [simp]: "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)" "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))" "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))" "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)" "!!P. (ALL x:{}. P x) = True" "!!P. (ALL x:UNIV. P x) = (ALL x. P x)" "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))" "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)" "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)" "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)" "!!A P f. (ALL x:f`A. P x) = (ALL x:A. P (f x))" "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)" by auto lemma bex_simps [simp]: "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)" "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))" "!!P. (EX x:{}. P x) = False" "!!P. (EX x:UNIV. P x) = (EX x. P x)" "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))" "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)" "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)" "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)" "!!A P f. (EX x:f`A. P x) = (EX x:A. P (f x))" "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)" by auto lemma ball_conj_distrib: "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))" by blast lemma bex_disj_distrib: "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))" by blast text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *} lemma UN_extend_simps: "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))" "!!A B C. (UN x:C. A x) Un B = (if C={} then B else (UN x:C. A x Un B))" "!!A B C. A Un (UN x:C. B x) = (if C={} then A else (UN x:C. A Un B x))" "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)" "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)" "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)" "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)" "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)" "!!A B C. (UN x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)" "!!A B f. (UN a:A. B (f a)) = (UN x:f`A. B x)" by auto lemma INT_extend_simps: "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))" "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))" "!!A B C. (INT x:C. A x) - B = (if C={} then UNIV-B else (INT x:C. A x - B))" "!!A B C. A - (UN x:C. B x) = (if C={} then A else (INT x:C. A - B x))" "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))" "!!A B C. ((INT x:C. A x) Un B) = (INT x:C. A x Un B)" "!!A B C. A Un (INT x:C. B x) = (INT x:C. A Un B x)" "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)" "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)" "!!A B f. (INT a:A. B (f a)) = (INT x:f`A. B x)" by auto subsubsection {* Monotonicity of various operations *} lemma image_mono: "A ⊆ B ==> f`A ⊆ f`B" by blast lemma Pow_mono: "A ⊆ B ==> Pow A ⊆ Pow B" by blast lemma Union_mono: "A ⊆ B ==> \<Union>A ⊆ \<Union>B" by blast lemma Inter_anti_mono: "B ⊆ A ==> \<Inter>A ⊆ \<Inter>B" by blast lemma UN_mono: "A ⊆ B ==> (!!x. x ∈ A ==> f x ⊆ g x) ==> (\<Union>x∈A. f x) ⊆ (\<Union>x∈B. g x)" by (blast dest: subsetD) lemma INT_anti_mono: "B ⊆ A ==> (!!x. x ∈ A ==> f x ⊆ g x) ==> (\<Inter>x∈A. f x) ⊆ (\<Inter>x∈A. g x)" -- {* The last inclusion is POSITIVE! *} by (blast dest: subsetD) lemma insert_mono: "C ⊆ D ==> insert a C ⊆ insert a D" by blast lemma Un_mono: "A ⊆ C ==> B ⊆ D ==> A ∪ B ⊆ C ∪ D" by blast lemma Int_mono: "A ⊆ C ==> B ⊆ D ==> A ∩ B ⊆ C ∩ D" by blast lemma Diff_mono: "A ⊆ C ==> D ⊆ B ==> A - B ⊆ C - D" by blast lemma Compl_anti_mono: "A ⊆ B ==> -B ⊆ -A" by blast text {* \medskip Monotonicity of implications. *} lemma in_mono: "A ⊆ B ==> x ∈ A --> x ∈ B" apply (rule impI) apply (erule subsetD, assumption) done lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)" by iprover lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)" by iprover lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)" by iprover lemma imp_refl: "P --> P" .. lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)" by iprover lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)" by iprover lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P ⊆ Collect Q" by blast lemma Int_Collect_mono: "A ⊆ B ==> (!!x. x ∈ A ==> P x --> Q x) ==> A ∩ Collect P ⊆ B ∩ Collect Q" by blast lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono Collect_mono in_mono lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c" by iprover lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c" by iprover lemma Least_mono: "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" -- {* Courtesy of Stephan Merz *} apply clarify apply (erule_tac P = "%x. x : S" in LeastI2_order, fast) apply (rule LeastI2_order) apply (auto elim: monoD intro!: order_antisym) done subsection {* Inverse image of a function *} constdefs vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) "f -` B == {x. f x : B}" subsubsection {* Basic rules *} lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)" by (unfold vimage_def) blast lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)" by simp lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B" by (unfold vimage_def) blast lemma vimageI2: "f a : A ==> a : f -` A" by (unfold vimage_def) fast lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P" by (unfold vimage_def) blast lemma vimageD: "a : f -` A ==> f a : A" by (unfold vimage_def) fast subsubsection {* Equations *} lemma vimage_empty [simp]: "f -` {} = {}" by blast lemma vimage_Compl: "f -` (-A) = -(f -` A)" by blast lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)" by blast lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)" by fast lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)" by blast lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)" by blast lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)" by blast lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}" by blast lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q" by blast lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)" -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *} by blast lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)" by blast lemma vimage_UNIV [simp]: "f -` UNIV = UNIV" by blast lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})" -- {* NOT suitable for rewriting *} by blast lemma vimage_mono: "A ⊆ B ==> f -` A ⊆ f -` B" -- {* monotonicity *} by blast subsection {* Getting the Contents of a Singleton Set *} constdefs contents :: "'a set => 'a" "contents X == THE x. X = {x}" lemma contents_eq [simp]: "contents {x} = x" by (simp add: contents_def) subsection {* Transitivity rules for calculational reasoning *} lemma set_rev_mp: "x:A ==> A ⊆ B ==> x:B" by (rule subsetD) lemma set_mp: "A ⊆ B ==> x:A ==> x:B" by (rule subsetD) lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" by (rule subst) lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" by (rule ssubst) lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" by (rule subst) lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" by (rule ssubst) lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> (!!x y. x < y ==> f x < f y) ==> f a < c" proof - assume r: "!!x y. x < y ==> f x < f y" assume "a < b" hence "f a < f b" by (rule r) also assume "f b < c" finally (order_less_trans) show ?thesis . qed lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> (!!x y. x < y ==> f x < f y) ==> a < f c" proof - assume r: "!!x y. x < y ==> f x < f y" assume "a < f b" also assume "b < c" hence "f b < f c" by (rule r) finally (order_less_trans) show ?thesis . qed lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> (!!x y. x <= y ==> f x <= f y) ==> f a < c" proof - assume r: "!!x y. x <= y ==> f x <= f y" assume "a <= b" hence "f a <= f b" by (rule r) also assume "f b < c" finally (order_le_less_trans) show ?thesis . qed lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> (!!x y. x < y ==> f x < f y) ==> a < f c" proof - assume r: "!!x y. x < y ==> f x < f y" assume "a <= f b" also assume "b < c" hence "f b < f c" by (rule r) finally (order_le_less_trans) show ?thesis . qed lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> (!!x y. x < y ==> f x < f y) ==> f a < c" proof - assume r: "!!x y. x < y ==> f x < f y" assume "a < b" hence "f a < f b" by (rule r) also assume "f b <= c" finally (order_less_le_trans) show ?thesis . qed lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> (!!x y. x <= y ==> f x <= f y) ==> a < f c" proof - assume r: "!!x y. x <= y ==> f x <= f y" assume "a < f b" also assume "b <= c" hence "f b <= f c" by (rule r) finally (order_less_le_trans) show ?thesis . qed lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> (!!x y. x <= y ==> f x <= f y) ==> a <= f c" proof - assume r: "!!x y. x <= y ==> f x <= f y" assume "a <= f b" also assume "b <= c" hence "f b <= f c" by (rule r) finally (order_trans) show ?thesis . qed lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> (!!x y. x <= y ==> f x <= f y) ==> f a <= c" proof - assume r: "!!x y. x <= y ==> f x <= f y" assume "a <= b" hence "f a <= f b" by (rule r) also assume "f b <= c" finally (order_trans) show ?thesis . qed lemma ord_le_eq_subst: "a <= b ==> f b = c ==> (!!x y. x <= y ==> f x <= f y) ==> f a <= c" proof - assume r: "!!x y. x <= y ==> f x <= f y" assume "a <= b" hence "f a <= f b" by (rule r) also assume "f b = c" finally (ord_le_eq_trans) show ?thesis . qed lemma ord_eq_le_subst: "a = f b ==> b <= c ==> (!!x y. x <= y ==> f x <= f y) ==> a <= f c" proof - assume r: "!!x y. x <= y ==> f x <= f y" assume "a = f b" also assume "b <= c" hence "f b <= f c" by (rule r) finally (ord_eq_le_trans) show ?thesis . qed lemma ord_less_eq_subst: "a < b ==> f b = c ==> (!!x y. x < y ==> f x < f y) ==> f a < c" proof - assume r: "!!x y. x < y ==> f x < f y" assume "a < b" hence "f a < f b" by (rule r) also assume "f b = c" finally (ord_less_eq_trans) show ?thesis . qed lemma ord_eq_less_subst: "a = f b ==> b < c ==> (!!x y. x < y ==> f x < f y) ==> a < f c" proof - assume r: "!!x y. x < y ==> f x < f y" assume "a = f b" also assume "b < c" hence "f b < f c" by (rule r) finally (ord_eq_less_trans) show ?thesis . qed text {* Note that this list of rules is in reverse order of priorities. *} lemmas basic_trans_rules [trans] = order_less_subst2 order_less_subst1 order_le_less_subst2 order_le_less_subst1 order_less_le_subst2 order_less_le_subst1 order_subst2 order_subst1 ord_le_eq_subst ord_eq_le_subst ord_less_eq_subst ord_eq_less_subst forw_subst back_subst rev_mp mp set_rev_mp set_mp order_neq_le_trans order_le_neq_trans order_less_trans order_less_asym' order_le_less_trans order_less_le_trans order_trans order_antisym ord_le_eq_trans ord_eq_le_trans ord_less_eq_trans ord_eq_less_trans trans end
lemma CollectI:
P a ==> a ∈ {x. P x}
lemma CollectD:
a ∈ {x. P x} ==> P a
lemma Collect_cong:
(!!x. P x = Q x) ==> {x. P x} = {x. Q x}
lemmas CollectE:
[| a ∈ {x. P x}; P a ==> PROP W1 |] ==> PROP W1
lemmas CollectE:
[| a ∈ {x. P x}; P a ==> PROP W1 |] ==> PROP W1
lemma ballI:
(!!x. x ∈ A ==> P x) ==> ∀x∈A. P x
lemmas strip:
(P ==> Q) ==> P --> Q
(!!x. P x) ==> ∀x. P x
(!!x. x ∈ A ==> P x) ==> ∀x∈A. P x
lemmas strip:
(P ==> Q) ==> P --> Q
(!!x. P x) ==> ∀x. P x
(!!x. x ∈ A ==> P x) ==> ∀x∈A. P x
lemma bspec:
[| ∀x∈A. P x; x ∈ A |] ==> P x
lemma ballE:
[| ∀x∈A. P x; P x ==> Q; x ∉ A ==> Q |] ==> Q
theorem rev_ballE:
[| ∀x∈A. P x; x ∉ A ==> Q; P x ==> Q |] ==> Q
lemma bexI:
[| P x; x ∈ A |] ==> ∃x∈A. P x
lemma rev_bexI:
[| x ∈ A; P x |] ==> ∃x∈A. P x
lemma bexCI:
[| ∀x∈A. ¬ P x ==> P a; a ∈ A |] ==> ∃x∈A. P x
lemma bexE:
[| ∃x∈A. P x; !!x. [| x ∈ A; P x |] ==> Q |] ==> Q
lemma ball_triv:
(∀x∈A. P) = ((∃x. x ∈ A) --> P)
lemma bex_triv:
(∃x∈A. P) = ((∃x. x ∈ A) ∧ P)
lemma bex_triv_one_point1:
(∃x∈A. x = a) = (a ∈ A)
lemma bex_triv_one_point2:
(∃x∈A. a = x) = (a ∈ A)
lemma bex_one_point1:
(∃x∈A. x = a ∧ P x) = (a ∈ A ∧ P a)
lemma bex_one_point2:
(∃x∈A. a = x ∧ P x) = (a ∈ A ∧ P a)
lemma ball_one_point1:
(∀x∈A. x = a --> P x) = (a ∈ A --> P a)
lemma ball_one_point2:
(∀x∈A. a = x --> P x) = (a ∈ A --> P a)
lemma ball_cong:
[| A = B; !!x. x ∈ B ==> P x = Q x |] ==> (∀x∈A. P x) = (∀x∈B. Q x)
lemma strong_ball_cong:
[| A = B; !!x. x ∈ B =simp=> P x = Q x |] ==> (∀x∈A. P x) = (∀x∈B. Q x)
lemma bex_cong:
[| A = B; !!x. x ∈ B ==> P x = Q x |] ==> (∃x∈A. P x) = (∃x∈B. Q x)
lemma strong_bex_cong:
[| A = B; !!x. x ∈ B =simp=> P x = Q x |] ==> (∃x∈A. P x) = (∃x∈B. Q x)
lemma subsetI:
(!!x. x ∈ A ==> x ∈ B) ==> A ⊆ B
lemma subsetD:
[| A ⊆ B; c ∈ A |] ==> c ∈ B
lemma rev_subsetD:
[| c ∈ A; A ⊆ B |] ==> c ∈ B
lemma subsetCE:
[| A ⊆ B; c ∉ A ==> P; c ∈ B ==> P |] ==> P
lemma contra_subsetD:
[| A ⊆ B; c ∉ B |] ==> c ∉ A
lemma subset_refl:
A ⊆ A
lemma subset_trans:
[| A ⊆ B; B ⊆ C |] ==> A ⊆ C
lemma set_ext:
(!!x. (x ∈ A) = (x ∈ B)) ==> A = B
lemma expand_set_eq:
(A = B) = (∀x. (x ∈ A) = (x ∈ B))
lemma subset_antisym:
[| A ⊆ B; B ⊆ A |] ==> A = B
lemmas equalityI:
[| A ⊆ B; B ⊆ A |] ==> A = B
lemmas equalityI:
[| A ⊆ B; B ⊆ A |] ==> A = B
lemma equalityD1:
A = B ==> A ⊆ B
lemma equalityD2:
A = B ==> B ⊆ A
lemma equalityE:
[| A = B; [| A ⊆ B; B ⊆ A |] ==> P |] ==> P
lemma equalityCE:
[| A = B; [| c ∈ A; c ∈ B |] ==> P; [| c ∉ A; c ∉ B |] ==> P |] ==> P
lemma setup_induction:
[| p ∈ A; !!z. z ∈ A ==> p = z --> R |] ==> R
lemma eqset_imp_iff:
A = B ==> (x ∈ A) = (x ∈ B)
lemma eqelem_imp_iff:
x = y ==> (x ∈ A) = (y ∈ A)
lemma UNIV_I:
x ∈ UNIV
lemma UNIV_witness:
∃x. x ∈ UNIV
lemma subset_UNIV:
A ⊆ UNIV
lemma ball_UNIV:
Ball UNIV P = All P
lemma bex_UNIV:
Bex UNIV P = Ex P
lemma empty_iff:
(c ∈ {}) = False
lemma emptyE:
a ∈ {} ==> P
lemma empty_subsetI:
{} ⊆ A
lemma equals0I:
(!!y. y ∈ A ==> False) ==> A = {}
lemma equals0D:
A = {} ==> a ∉ A
lemma ball_empty:
Ball {} P = True
lemma bex_empty:
Bex {} P = False
lemma UNIV_not_empty:
UNIV ≠ {}
lemma Pow_iff:
(A ∈ Pow B) = (A ⊆ B)
lemma PowI:
A ⊆ B ==> A ∈ Pow B
lemma PowD:
A ∈ Pow B ==> A ⊆ B
lemma Pow_bottom:
{} ∈ Pow B
lemma Pow_top:
A ∈ Pow A
lemma Compl_iff:
(c ∈ - A) = (c ∉ A)
lemma ComplI:
(c ∈ A ==> False) ==> c ∈ - A
lemma ComplD:
c ∈ - A ==> c ∉ A
lemmas ComplE:
[| c ∈ - A; c ∉ A ==> PROP W1 |] ==> PROP W1
lemmas ComplE:
[| c ∈ - A; c ∉ A ==> PROP W1 |] ==> PROP W1
lemma Un_iff:
(c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)
lemma UnI1:
c ∈ A ==> c ∈ A ∪ B
lemma UnI2:
c ∈ B ==> c ∈ A ∪ B
lemma UnCI:
(c ∉ B ==> c ∈ A) ==> c ∈ A ∪ B
lemma UnE:
[| c ∈ A ∪ B; c ∈ A ==> P; c ∈ B ==> P |] ==> P
lemma Int_iff:
(c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)
lemma IntI:
[| c ∈ A; c ∈ B |] ==> c ∈ A ∩ B
lemma IntD1:
c ∈ A ∩ B ==> c ∈ A
lemma IntD2:
c ∈ A ∩ B ==> c ∈ B
lemma IntE:
[| c ∈ A ∩ B; [| c ∈ A; c ∈ B |] ==> P |] ==> P
lemma Diff_iff:
(c ∈ A - B) = (c ∈ A ∧ c ∉ B)
lemma DiffI:
[| c ∈ A; c ∉ B |] ==> c ∈ A - B
lemma DiffD1:
c ∈ A - B ==> c ∈ A
lemma DiffD2:
[| c ∈ A - B; c ∈ B |] ==> P
lemma DiffE:
[| c ∈ A - B; [| c ∈ A; c ∉ B |] ==> P |] ==> P
lemma insert_iff:
(a ∈ insert b A) = (a = b ∨ a ∈ A)
lemma insertI1:
a ∈ insert a B
lemma insertI2:
a ∈ B ==> a ∈ insert b B
lemma insertE:
[| a ∈ insert b A; a = b ==> P; a ∈ A ==> P |] ==> P
lemma insertCI:
(a ∉ B ==> a = b) ==> a ∈ insert b B
lemma subset_insert_iff:
(A ⊆ insert x B) = (if x ∈ A then A - {x} ⊆ B else A ⊆ B)
lemma singletonI:
a ∈ {a}
lemma singletonD:
b ∈ {a} ==> b = a
lemmas singletonE:
[| b ∈ {a}; b = a ==> PROP W1 |] ==> PROP W1
lemmas singletonE:
[| b ∈ {a}; b = a ==> PROP W1 |] ==> PROP W1
lemma singleton_iff:
(b ∈ {a}) = (b = a)
lemma singleton_inject:
{a} = {b} ==> a = b
lemma singleton_insert_inj_eq:
({b} = insert a A) = (a = b ∧ A ⊆ {b})
lemma singleton_insert_inj_eq':
(insert a A = {b}) = (a = b ∧ A ⊆ {b})
lemma subset_singletonD:
A ⊆ {x} ==> A = {} ∨ A = {x}
lemma singleton_conv:
{x. x = a} = {a}
lemma singleton_conv2:
{x. a = x} = {a}
lemma diff_single_insert:
[| A - {x} ⊆ B; x ∈ A |] ==> A ⊆ insert x B
lemma UN_iff:
(b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)
lemma UN_I:
[| a ∈ A; b ∈ B a |] ==> b ∈ (UN x:A. B x)
lemma UN_E:
[| b ∈ (UN x:A. B x); !!x. [| x ∈ A; b ∈ B x |] ==> R |] ==> R
lemma UN_cong:
[| A = B; !!x. x ∈ B ==> C x = D x |] ==> (UN x:A. C x) = (UN x:B. D x)
lemma INT_iff:
(b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)
lemma INT_I:
(!!x. x ∈ A ==> b ∈ B x) ==> b ∈ (INT x:A. B x)
lemma INT_D:
[| b ∈ (INT x:A. B x); a ∈ A |] ==> b ∈ B a
lemma INT_E:
[| b ∈ (INT x:A. B x); b ∈ B a ==> R; a ∉ A ==> R |] ==> R
lemma INT_cong:
[| A = B; !!x. x ∈ B ==> C x = D x |] ==> (INT x:A. C x) = (INT x:B. D x)
lemma Union_iff:
(A ∈ Union C) = (∃X∈C. A ∈ X)
lemma UnionI:
[| X ∈ C; A ∈ X |] ==> A ∈ Union C
lemma UnionE:
[| A ∈ Union C; !!X. [| A ∈ X; X ∈ C |] ==> R |] ==> R
lemma Inter_iff:
(A ∈ Inter C) = (∀X∈C. A ∈ X)
lemma InterI:
(!!X. X ∈ C ==> A ∈ X) ==> A ∈ Inter C
lemma InterD:
[| A ∈ Inter C; X ∈ C |] ==> A ∈ X
lemma InterE:
[| A ∈ Inter C; X ∉ C ==> R; A ∈ X ==> R |] ==> R
lemma image_eqI:
[| b = f x; x ∈ A |] ==> b ∈ f ` A
lemma imageI:
x ∈ A ==> f x ∈ f ` A
lemma rev_image_eqI:
[| x ∈ A; b = f x |] ==> b ∈ f ` A
lemma imageE:
[| b ∈ f ` A; !!x. [| b = f x; x ∈ A |] ==> P |] ==> P
lemma image_Un:
f ` (A ∪ B) = f ` A ∪ f ` B
lemma image_iff:
(z ∈ f ` A) = (∃x∈A. z = f x)
lemma image_subset_iff:
(f ` A ⊆ B) = (∀x∈A. f x ∈ B)
lemma subset_image_iff:
(B ⊆ f ` A) = (∃AA⊆A. B = f ` AA)
lemma image_subsetI:
(!!x. x ∈ A ==> f x ∈ B) ==> f ` A ⊆ B
lemma range_eqI:
b = f x ==> b ∈ range f
lemma rangeI:
f x ∈ range f
lemma rangeE:
[| b ∈ range f; !!x. b = f x ==> P |] ==> P
lemma split_if_eq1:
((if Q then x else y) = b) = ((Q --> x = b) ∧ (¬ Q --> y = b))
lemma split_if_eq2:
(a = (if Q then x else y)) = ((Q --> a = x) ∧ (¬ Q --> a = y))
lemma split_if_mem1:
((if Q then x else y) ∈ b) = ((Q --> x ∈ b) ∧ (¬ Q --> y ∈ b))
lemma split_if_mem2:
(a ∈ (if Q then x else y)) = ((Q --> a ∈ x) ∧ (¬ Q --> a ∈ y))
lemmas split_ifs:
(if P then Q else R) = ((P --> Q) ∧ (¬ P --> R))
((if Q then x else y) = b) = ((Q --> x = b) ∧ (¬ Q --> y = b))
(a = (if Q then x else y)) = ((Q --> a = x) ∧ (¬ Q --> a = y))
((if Q then x else y) ∈ b) = ((Q --> x ∈ b) ∧ (¬ Q --> y ∈ b))
(a ∈ (if Q then x else y)) = ((Q --> a ∈ x) ∧ (¬ Q --> a ∈ y))
lemmas split_ifs:
(if P then Q else R) = ((P --> Q) ∧ (¬ P --> R))
((if Q then x else y) = b) = ((Q --> x = b) ∧ (¬ Q --> y = b))
(a = (if Q then x else y)) = ((Q --> a = x) ∧ (¬ Q --> a = y))
((if Q then x else y) ∈ b) = ((Q --> x ∈ b) ∧ (¬ Q --> y ∈ b))
(a ∈ (if Q then x else y)) = ((Q --> a ∈ x) ∧ (¬ Q --> a ∈ y))
lemmas mem_simps:
(a ∈ insert b A) = (a = b ∨ a ∈ A)
(c ∈ {}) = False
(c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)
(c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)
(c ∈ - A) = (c ∉ A)
(c ∈ A - B) = (c ∈ A ∧ c ∉ B)
(a ∈ {x. P x}) = P a
(b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)
(A ∈ Union C) = (∃X∈C. A ∈ X)
(b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)
(A ∈ Inter C) = (∀X∈C. A ∈ X)
lemmas mem_simps:
(a ∈ insert b A) = (a = b ∨ a ∈ A)
(c ∈ {}) = False
(c ∈ A ∪ B) = (c ∈ A ∨ c ∈ B)
(c ∈ A ∩ B) = (c ∈ A ∧ c ∈ B)
(c ∈ - A) = (c ∉ A)
(c ∈ A - B) = (c ∈ A ∧ c ∉ B)
(a ∈ {x. P x}) = P a
(b ∈ (UN x:A. B x)) = (∃x∈A. b ∈ B x)
(A ∈ Union C) = (∃X∈C. A ∈ X)
(b ∈ (INT x:A. B x)) = (∀x∈A. b ∈ B x)
(A ∈ Inter C) = (∀X∈C. A ∈ X)
lemma psubsetI:
[| A ⊆ B; A ≠ B |] ==> A ⊂ B
lemma psubsetE:
[| A ⊂ B; [| A ⊆ B; ¬ B ⊆ A |] ==> R |] ==> R
lemma psubset_insert_iff:
(A ⊂ insert x B) = (if x ∈ B then A ⊂ B else if x ∈ A then A - {x} ⊂ B else A ⊆ B)
lemma psubset_eq:
(A ⊂ B) = (A ⊆ B ∧ A ≠ B)
lemma psubset_imp_subset:
A ⊂ B ==> A ⊆ B
lemma psubset_trans:
[| A ⊂ B; B ⊂ C |] ==> A ⊂ C
lemma psubsetD:
[| A ⊂ B; c ∈ A |] ==> c ∈ B
lemma psubset_subset_trans:
[| A ⊂ B; B ⊆ C |] ==> A ⊂ C
lemma subset_psubset_trans:
[| A ⊆ B; B ⊂ C |] ==> A ⊂ C
lemma psubset_imp_ex_mem:
A ⊂ B ==> ∃b. b ∈ B - A
lemma atomize_ball:
(!!x. x ∈ A ==> P x) == ∀x∈A. P x
lemma subset_insertI:
B ⊆ insert a B
lemma subset_insertI2:
A ⊆ B ==> A ⊆ insert b B
lemma subset_insert:
x ∉ A ==> (A ⊆ insert x B) = (A ⊆ B)
lemma Union_upper:
B ∈ A ==> B ⊆ Union A
lemma Union_least:
(!!X. X ∈ A ==> X ⊆ C) ==> Union A ⊆ C
lemma UN_upper:
a ∈ A ==> B a ⊆ (UN x:A. B x)
lemma UN_least:
(!!x. x ∈ A ==> B x ⊆ C) ==> (UN x:A. B x) ⊆ C
lemma Inter_lower:
B ∈ A ==> Inter A ⊆ B
lemma Inter_subset:
[| !!X. X ∈ A ==> X ⊆ B; A ≠ {} |] ==> Inter A ⊆ B
lemma Inter_greatest:
(!!X. X ∈ A ==> C ⊆ X) ==> C ⊆ Inter A
lemma INT_lower:
a ∈ A ==> (INT x:A. B x) ⊆ B a
lemma INT_greatest:
(!!x. x ∈ A ==> C ⊆ B x) ==> C ⊆ (INT x:A. B x)
lemma Un_upper1:
A ⊆ A ∪ B
lemma Un_upper2:
B ⊆ A ∪ B
lemma Un_least:
[| A ⊆ C; B ⊆ C |] ==> A ∪ B ⊆ C
lemma Int_lower1:
A ∩ B ⊆ A
lemma Int_lower2:
A ∩ B ⊆ B
lemma Int_greatest:
[| C ⊆ A; C ⊆ B |] ==> C ⊆ A ∩ B
lemma Diff_subset:
A - B ⊆ A
lemma Diff_subset_conv:
(A - B ⊆ C) = (A ⊆ B ∪ C)
lemma mono_Un:
mono f ==> f A ∪ f B ⊆ f (A ∪ B)
lemma mono_Int:
mono f ==> f (A ∩ B) ⊆ f A ∩ f B
lemma Collect_const:
{s. P} = (if P then UNIV else {})
lemma subset_empty:
(A ⊆ {}) = (A = {})
lemma not_psubset_empty:
¬ A ⊂ {}
lemma Collect_empty_eq:
(Collect P = {}) = (∀x. ¬ P x)
lemma Collect_neg_eq:
{x. ¬ P x} = - {x. P x}
lemma Collect_disj_eq:
{x. P x ∨ Q x} = {x. P x} ∪ {x. Q x}
lemma Collect_imp_eq:
{x. P x --> Q x} = - {x. P x} ∪ {x. Q x}
lemma Collect_conj_eq:
{x. P x ∧ Q x} = {x. P x} ∩ {x. Q x}
lemma Collect_all_eq:
{x. ∀y. P x y} = (INT y. {x. P x y})
lemma Collect_ball_eq:
{x. ∀y∈A. P x y} = (INT y:A. {x. P x y})
lemma Collect_ex_eq:
{x. ∃y. P x y} = (UN y. {x. P x y})
lemma Collect_bex_eq:
{x. ∃y∈A. P x y} = (UN y:A. {x. P x y})
lemma insert_is_Un:
insert a A = {a} ∪ A
lemma insert_not_empty:
insert a A ≠ {}
lemmas empty_not_insert:
{} ≠ insert a A
lemmas empty_not_insert:
{} ≠ insert a A
lemma insert_absorb:
a ∈ A ==> insert a A = A
lemma insert_absorb2:
insert x (insert x A) = insert x A
lemma insert_commute:
insert x (insert y A) = insert y (insert x A)
lemma insert_subset:
(insert x A ⊆ B) = (x ∈ B ∧ A ⊆ B)
lemma mk_disjoint_insert:
a ∈ A ==> ∃B. A = insert a B ∧ a ∉ B
lemma insert_Collect:
insert a (Collect P) = {u. u ≠ a --> P u}
lemma UN_insert_distrib:
u ∈ A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)
lemma insert_inter_insert:
insert a A ∩ insert a B = insert a (A ∩ B)
lemma insert_disjoint:
(insert a A ∩ B = {}) = (a ∉ B ∧ A ∩ B = {})
({} = insert a A ∩ B) = (a ∉ B ∧ {} = A ∩ B)
lemma disjoint_insert:
(B ∩ insert a A = {}) = (a ∉ B ∧ B ∩ A = {})
({} = A ∩ insert b B) = (b ∉ A ∧ {} = A ∩ B)
lemma image_empty:
f ` {} = {}
lemma image_insert:
f ` insert a B = insert (f a) (f ` B)
lemma image_constant:
x ∈ A ==> (%x. c) ` A = {c}
lemma image_image:
f ` g ` A = (%x. f (g x)) ` A
lemma insert_image:
x ∈ A ==> insert (f x) (f ` A) = f ` A
lemma image_is_empty:
(f ` A = {}) = (A = {})
lemma image_Collect:
f ` {x. P x} = {f x |x. P x}
lemma if_image_distrib:
(%x. if P x then f x else g x) ` S = f ` (S ∩ {x. P x}) ∪ g ` (S ∩ {x. ¬ P x})
lemma image_cong:
[| M = N; !!x. x ∈ N ==> f x = g x |] ==> f ` M = g ` N
lemma full_SetCompr_eq:
{u. ∃x. u = f x} = range f
lemma range_composition:
range (%x. f (g x)) = f ` range g
lemma Int_absorb:
A ∩ A = A
lemma Int_left_absorb:
A ∩ (A ∩ B) = A ∩ B
lemma Int_commute:
A ∩ B = B ∩ A
lemma Int_left_commute:
A ∩ (B ∩ C) = B ∩ (A ∩ C)
lemma Int_assoc:
A ∩ B ∩ C = A ∩ (B ∩ C)
lemmas Int_ac:
A ∩ B ∩ C = A ∩ (B ∩ C)
A ∩ (A ∩ B) = A ∩ B
A ∩ B = B ∩ A
A ∩ (B ∩ C) = B ∩ (A ∩ C)
lemmas Int_ac:
A ∩ B ∩ C = A ∩ (B ∩ C)
A ∩ (A ∩ B) = A ∩ B
A ∩ B = B ∩ A
A ∩ (B ∩ C) = B ∩ (A ∩ C)
lemma Int_absorb1:
B ⊆ A ==> A ∩ B = B
lemma Int_absorb2:
A ⊆ B ==> A ∩ B = A
lemma Int_empty_left:
{} ∩ B = {}
lemma Int_empty_right:
A ∩ {} = {}
lemma disjoint_eq_subset_Compl:
(A ∩ B = {}) = (A ⊆ - B)
lemma disjoint_iff_not_equal:
(A ∩ B = {}) = (∀x∈A. ∀y∈B. x ≠ y)
lemma Int_UNIV_left:
UNIV ∩ B = B
lemma Int_UNIV_right:
A ∩ UNIV = A
lemma Int_eq_Inter:
A ∩ B = Inter {A, B}
lemma Int_Un_distrib:
A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C
lemma Int_Un_distrib2:
(B ∪ C) ∩ A = B ∩ A ∪ C ∩ A
lemma Int_UNIV:
(A ∩ B = UNIV) = (A = UNIV ∧ B = UNIV)
lemma Int_subset_iff:
(C ⊆ A ∩ B) = (C ⊆ A ∧ C ⊆ B)
lemma Int_Collect:
(x ∈ A ∩ {x. P x}) = (x ∈ A ∧ P x)
lemma Un_absorb:
A ∪ A = A
lemma Un_left_absorb:
A ∪ (A ∪ B) = A ∪ B
lemma Un_commute:
A ∪ B = B ∪ A
lemma Un_left_commute:
A ∪ (B ∪ C) = B ∪ (A ∪ C)
lemma Un_assoc:
A ∪ B ∪ C = A ∪ (B ∪ C)
lemmas Un_ac:
A ∪ B ∪ C = A ∪ (B ∪ C)
A ∪ (A ∪ B) = A ∪ B
A ∪ B = B ∪ A
A ∪ (B ∪ C) = B ∪ (A ∪ C)
lemmas Un_ac:
A ∪ B ∪ C = A ∪ (B ∪ C)
A ∪ (A ∪ B) = A ∪ B
A ∪ B = B ∪ A
A ∪ (B ∪ C) = B ∪ (A ∪ C)
lemma Un_absorb1:
A ⊆ B ==> A ∪ B = B
lemma Un_absorb2:
B ⊆ A ==> A ∪ B = A
lemma Un_empty_left:
{} ∪ B = B
lemma Un_empty_right:
A ∪ {} = A
lemma Un_UNIV_left:
UNIV ∪ B = UNIV
lemma Un_UNIV_right:
A ∪ UNIV = UNIV
lemma Un_eq_Union:
A ∪ B = Union {A, B}
lemma Un_insert_left:
insert a B ∪ C = insert a (B ∪ C)
lemma Un_insert_right:
A ∪ insert a B = insert a (A ∪ B)
lemma Int_insert_left:
insert a B ∩ C = (if a ∈ C then insert a (B ∩ C) else B ∩ C)
lemma Int_insert_right:
A ∩ insert a B = (if a ∈ A then insert a (A ∩ B) else A ∩ B)
lemma Un_Int_distrib:
A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)
lemma Un_Int_distrib2:
B ∩ C ∪ A = (B ∪ A) ∩ (C ∪ A)
lemma Un_Int_crazy:
A ∩ B ∪ B ∩ C ∪ C ∩ A = (A ∪ B) ∩ (B ∪ C) ∩ (C ∪ A)
lemma subset_Un_eq:
(A ⊆ B) = (A ∪ B = B)
lemma Un_empty:
(A ∪ B = {}) = (A = {} ∧ B = {})
lemma Un_subset_iff:
(A ∪ B ⊆ C) = (A ⊆ C ∧ B ⊆ C)
lemma Un_Diff_Int:
A - B ∪ A ∩ B = A
lemma Compl_disjoint:
A ∩ - A = {}
lemma Compl_disjoint2:
- A ∩ A = {}
lemma Compl_partition:
A ∪ - A = UNIV
lemma Compl_partition2:
- A ∪ A = UNIV
lemma double_complement:
- (- A) = A
lemma Compl_Un:
- (A ∪ B) = - A ∩ - B
lemma Compl_Int:
- (A ∩ B) = - A ∪ - B
lemma Compl_UN:
- (UN x:A. B x) = (INT x:A. - B x)
lemma Compl_INT:
- (INT x:A. B x) = (UN x:A. - B x)
lemma subset_Compl_self_eq:
(A ⊆ - A) = (A = {})
lemma Un_Int_assoc_eq:
(A ∩ B ∪ C = A ∩ (B ∪ C)) = (C ⊆ A)
lemma Compl_UNIV_eq:
- UNIV = {}
lemma Compl_empty_eq:
- {} = UNIV
lemma Compl_subset_Compl_iff:
(- A ⊆ - B) = (B ⊆ A)
lemma Compl_eq_Compl_iff:
(- A = - B) = (A = B)
lemma Union_empty:
Union {} = {}
lemma Union_UNIV:
Union UNIV = UNIV
lemma Union_insert:
Union (insert a B) = a ∪ Union B
lemma Union_Un_distrib:
Union (A ∪ B) = Union A ∪ Union B
lemma Union_Int_subset:
Union (A ∩ B) ⊆ Union A ∩ Union B
lemma Union_empty_conv:
(Union A = {}) = (∀x∈A. x = {})
lemma empty_Union_conv:
({} = Union A) = (∀x∈A. x = {})
lemma Union_disjoint:
(Union C ∩ A = {}) = (∀B∈C. B ∩ A = {})
lemma Inter_empty:
Inter {} = UNIV
lemma Inter_UNIV:
Inter UNIV = {}
lemma Inter_insert:
Inter (insert a B) = a ∩ Inter B
lemma Inter_Un_subset:
Inter A ∪ Inter B ⊆ Inter (A ∩ B)
lemma Inter_Un_distrib:
Inter (A ∪ B) = Inter A ∩ Inter B
lemma Inter_UNIV_conv:
(Inter A = UNIV) = (∀x∈A. x = UNIV)
(UNIV = Inter A) = (∀x∈A. x = UNIV)
lemma UN_empty:
(UN x:{}. B x) = {}
lemma UN_empty2:
(UN x:A. {}) = {}
lemma UN_singleton:
(UN x:A. {x}) = A
lemma UN_absorb:
k ∈ I ==> A k ∪ (UN i:I. A i) = (UN i:I. A i)
lemma INT_empty:
(INT x:{}. B x) = UNIV
lemma INT_absorb:
k ∈ I ==> A k ∩ (INT i:I. A i) = (INT i:I. A i)
lemma UN_insert:
(UN x:insert a A. B x) = B a ∪ UNION A B
lemma UN_Un:
(UN i:A ∪ B. M i) = (UN i:A. M i) ∪ (UN i:B. M i)
lemma UN_UN_flatten:
(UN x:UN y:A. B y. C x) = (UN y:A. UN x:B y. C x)
lemma UN_subset_iff:
((UN i:I. A i) ⊆ B) = (∀i∈I. A i ⊆ B)
lemma INT_subset_iff:
(B ⊆ (INT i:I. A i)) = (∀i∈I. B ⊆ A i)
lemma INT_insert:
(INT x:insert a A. B x) = B a ∩ INTER A B
lemma INT_Un:
(INT i:A ∪ B. M i) = (INT i:A. M i) ∩ (INT i:B. M i)
lemma INT_insert_distrib:
u ∈ A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)
lemma Union_image_eq:
Union (B ` A) = (UN x:A. B x)
lemma image_Union:
f ` Union S = (UN x:S. f ` x)
lemma Inter_image_eq:
Inter (B ` A) = (INT x:A. B x)
lemma UN_constant:
(UN y:A. c) = (if A = {} then {} else c)
lemma INT_constant:
(INT y:A. c) = (if A = {} then UNIV else c)
lemma UN_eq:
(UN x:A. B x) = Union {Y. ∃x∈A. Y = B x}
lemma INT_eq:
(INT x:A. B x) = Inter {Y. ∃x∈A. Y = B x}
lemma UNION_empty_conv:
({} = (UN x:A. B x)) = (∀x∈A. B x = {})
((UN x:A. B x) = {}) = (∀x∈A. B x = {})
lemma INTER_UNIV_conv:
(UNIV = (INT x:A. B x)) = (∀x∈A. B x = UNIV)
((INT x:A. B x) = UNIV) = (∀x∈A. B x = UNIV)
lemma Int_Union:
A ∩ Union B = (UN C:B. A ∩ C)
lemma Int_Union2:
Union B ∩ A = (UN C:B. C ∩ A)
lemma Un_Union_image:
(UN x:C. A x ∪ B x) = Union (A ` C) ∪ Union (B ` C)
lemma UN_Un_distrib:
(UN i:I. A i ∪ B i) = (UN i:I. A i) ∪ (UN i:I. B i)
lemma Un_Inter:
A ∪ Inter B = (INT C:B. A ∪ C)
lemma Int_Inter_image:
(INT x:C. A x ∩ B x) = Inter (A ` C) ∩ Inter (B ` C)
lemma INT_Int_distrib:
(INT i:I. A i ∩ B i) = (INT i:I. A i) ∩ (INT i:I. B i)
lemma Int_UN_distrib:
B ∩ (UN i:I. A i) = (UN i:I. B ∩ A i)
lemma Un_INT_distrib:
B ∪ (INT i:I. A i) = (INT i:I. B ∪ A i)
lemma Int_UN_distrib2:
(UN i:I. A i) ∩ (UN j:J. B j) = (UN i:I. UN j:J. A i ∩ B j)
lemma Un_INT_distrib2:
(INT i:I. A i) ∪ (INT j:J. B j) = (INT i:I. INT j:J. A i ∪ B j)
lemma ball_Un:
(∀x∈A ∪ B. P x) = ((∀x∈A. P x) ∧ (∀x∈B. P x))
lemma bex_Un:
(∃x∈A ∪ B. P x) = ((∃x∈A. P x) ∨ (∃x∈B. P x))
lemma ball_UN:
(∀z∈UNION A B. P z) = (∀x∈A. ∀z∈B x. P z)
lemma bex_UN:
(∃z∈UNION A B. P z) = (∃x∈A. ∃z∈B x. P z)
lemma Diff_eq:
A - B = A ∩ - B
lemma Diff_eq_empty_iff:
(A - B = {}) = (A ⊆ B)
lemma Diff_cancel:
A - A = {}
lemma Diff_idemp:
A - B - B = A - B
lemma Diff_triv:
A ∩ B = {} ==> A - B = A
lemma empty_Diff:
{} - A = {}
lemma Diff_empty:
A - {} = A
lemma Diff_UNIV:
A - UNIV = {}
lemma Diff_insert0:
x ∉ A ==> A - insert x B = A - B
lemma Diff_insert:
A - insert a B = A - B - {a}
lemma Diff_insert2:
A - insert a B = A - {a} - B
lemma insert_Diff_if:
insert x A - B = (if x ∈ B then A - B else insert x (A - B))
lemma insert_Diff1:
x ∈ B ==> insert x A - B = A - B
lemma insert_Diff_single:
insert a (A - {a}) = insert a A
lemma insert_Diff:
a ∈ A ==> insert a (A - {a}) = A
lemma Diff_insert_absorb:
x ∉ A ==> insert x A - {x} = A
lemma Diff_disjoint:
A ∩ (B - A) = {}
lemma Diff_partition:
A ⊆ B ==> A ∪ (B - A) = B
lemma double_diff:
[| A ⊆ B; B ⊆ C |] ==> B - (C - A) = A
lemma Un_Diff_cancel:
A ∪ (B - A) = A ∪ B
lemma Un_Diff_cancel2:
B - A ∪ A = B ∪ A
lemma Diff_Un:
A - (B ∪ C) = (A - B) ∩ (A - C)
lemma Diff_Int:
A - B ∩ C = A - B ∪ (A - C)
lemma Un_Diff:
A ∪ B - C = A - C ∪ (B - C)
lemma Int_Diff:
A ∩ B - C = A ∩ (B - C)
lemma Diff_Int_distrib:
C ∩ (A - B) = C ∩ A - C ∩ B
lemma Diff_Int_distrib2:
(A - B) ∩ C = A ∩ C - B ∩ C
lemma Diff_Compl:
A - - B = A ∩ B
lemma Compl_Diff_eq:
- (A - B) = - A ∪ B
lemma all_bool_eq:
(∀b. P b) = (P True ∧ P False)
lemma bool_induct:
[| P True; P False |] ==> P x
lemma ex_bool_eq:
(∃b. P b) = (P True ∨ P False)
lemma Un_eq_UN:
A ∪ B = (UN b. if b then A else B)
lemma UN_bool_eq:
(UN b. A b) = A True ∪ A False
lemma INT_bool_eq:
(INT b. A b) = A True ∩ A False
lemma Pow_empty:
Pow {} = {{}}
lemma Pow_insert:
Pow (insert a A) = Pow A ∪ insert a ` Pow A
lemma Pow_Compl:
Pow (- A) = {- B |B. A ∈ Pow B}
lemma Pow_UNIV:
Pow UNIV = UNIV
lemma Un_Pow_subset:
Pow A ∪ Pow B ⊆ Pow (A ∪ B)
lemma UN_Pow_subset:
(UN x:A. Pow (B x)) ⊆ Pow (UN x:A. B x)
lemma subset_Pow_Union:
A ⊆ Pow (Union A)
lemma Union_Pow_eq:
Union (Pow A) = A
lemma Pow_Int_eq:
Pow (A ∩ B) = Pow A ∩ Pow B
lemma Pow_INT_eq:
Pow (INT x:A. B x) = (INT x:A. Pow (B x))
lemma set_eq_subset:
(A = B) = (A ⊆ B ∧ B ⊆ A)
lemma subset_iff:
(A ⊆ B) = (∀t. t ∈ A --> t ∈ B)
lemma subset_iff_psubset_eq:
(A ⊆ B) = (A ⊂ B ∨ A = B)
lemma all_not_in_conv:
(∀x. x ∉ A) = (A = {})
lemma ex_in_conv:
(∃x. x ∈ A) = (A ≠ {})
lemma distinct_lemma:
f x ≠ f y ==> x ≠ y
lemma UN_simps:
(UN x:C. insert a (B x)) = (if C = {} then {} else insert a (UN x:C. B x))
(UN x:C. A x ∪ B) = (if C = {} then {} else (UN x:C. A x) ∪ B)
(UN x:C. A ∪ B x) = (if C = {} then {} else A ∪ (UN x:C. B x))
(UN x:C. A x ∩ B) = (UN x:C. A x) ∩ B
(UN x:C. A ∩ B x) = A ∩ (UN x:C. B x)
(UN x:C. A x - B) = (UN x:C. A x) - B
(UN x:C. A - B x) = A - (INT x:C. B x)
(UN x:Union A. B x) = (UN y:A. UN x:y. B x)
(UN z:UNION A B. C z) = (UN x:A. UN z:B x. C z)
(UN x:f ` A. B x) = (UN a:A. B (f a))
lemma INT_simps:
(INT x:C. A x ∩ B) = (if C = {} then UNIV else (INT x:C. A x) ∩ B)
(INT x:C. A ∩ B x) = (if C = {} then UNIV else A ∩ (INT x:C. B x))
(INT x:C. A x - B) = (if C = {} then UNIV else (INT x:C. A x) - B)
(INT x:C. A - B x) = (if C = {} then UNIV else A - (UN x:C. B x))
(INT x:C. insert a (B x)) = insert a (INT x:C. B x)
(INT x:C. A x ∪ B) = (INT x:C. A x) ∪ B
(INT x:C. A ∪ B x) = A ∪ (INT x:C. B x)
(INT x:Union A. B x) = (INT y:A. INT x:y. B x)
(INT z:UNION A B. C z) = (INT x:A. INT z:B x. C z)
(INT x:f ` A. B x) = (INT a:A. B (f a))
lemma ball_simps:
(∀x∈A. P x ∨ Q) = ((∀x∈A. P x) ∨ Q)
(∀x∈A. P ∨ Q x) = (P ∨ (∀x∈A. Q x))
(∀x∈A. P --> Q x) = (P --> (∀x∈A. Q x))
(∀x∈A. P x --> Q) = ((∃x∈A. P x) --> Q)
(∀x∈{}. P x) = True
(∀x∈UNIV. P x) = (∀x. P x)
(∀x∈insert a B. P x) = (P a ∧ (∀x∈B. P x))
(∀x∈Union A. P x) = (∀y∈A. ∀x∈y. P x)
(∀x∈UNION A B. P x) = (∀a∈A. ∀x∈B a. P x)
(∀x∈Collect Q. P x) = (∀x. Q x --> P x)
(∀x∈f ` A. P x) = (∀x∈A. P (f x))
(¬ (∀x∈A. P x)) = (∃x∈A. ¬ P x)
lemma bex_simps:
(∃x∈A. P x ∧ Q) = ((∃x∈A. P x) ∧ Q)
(∃x∈A. P ∧ Q x) = (P ∧ (∃x∈A. Q x))
(∃x∈{}. P x) = False
(∃x∈UNIV. P x) = (∃x. P x)
(∃x∈insert a B. P x) = (P a ∨ (∃x∈B. P x))
(∃x∈Union A. P x) = (∃y∈A. ∃x∈y. P x)
(∃x∈UNION A B. P x) = (∃a∈A. ∃x∈B a. P x)
(∃x∈Collect Q. P x) = (∃x. Q x ∧ P x)
(∃x∈f ` A. P x) = (∃x∈A. P (f x))
(¬ (∃x∈A. P x)) = (∀x∈A. ¬ P x)
lemma ball_conj_distrib:
(∀x∈A. P x ∧ Q x) = ((∀x∈A. P x) ∧ (∀x∈A. Q x))
lemma bex_disj_distrib:
(∃x∈A. P x ∨ Q x) = ((∃x∈A. P x) ∨ (∃x∈A. Q x))
lemma UN_extend_simps:
insert a (UN x:C. B x) = (if C = {} then {a} else UN x:C. insert a (B x))
(UN x:C. A x) ∪ B = (if C = {} then B else UN x:C. A x ∪ B)
A ∪ (UN x:C. B x) = (if C = {} then A else UN x:C. A ∪ B x)
(UN x:C. A x) ∩ B = (UN x:C. A x ∩ B)
A ∩ (UN x:C. B x) = (UN x:C. A ∩ B x)
(UN x:C. A x) - B = (UN x:C. A x - B)
A - (INT x:C. B x) = (UN x:C. A - B x)
(UN y:A. UN x:y. B x) = (UN x:Union A. B x)
(UN x:A. UN z:B x. C z) = (UN z:UNION A B. C z)
(UN a:A. B (f a)) = (UN x:f ` A. B x)
lemma INT_extend_simps:
(INT x:C. A x) ∩ B = (if C = {} then B else INT x:C. A x ∩ B)
A ∩ (INT x:C. B x) = (if C = {} then A else INT x:C. A ∩ B x)
(INT x:C. A x) - B = (if C = {} then UNIV - B else INT x:C. A x - B)
A - (UN x:C. B x) = (if C = {} then A else INT x:C. A - B x)
insert a (INT x:C. B x) = (INT x:C. insert a (B x))
(INT x:C. A x) ∪ B = (INT x:C. A x ∪ B)
A ∪ (INT x:C. B x) = (INT x:C. A ∪ B x)
(INT y:A. INT x:y. B x) = (INT x:Union A. B x)
(INT x:A. INT z:B x. C z) = (INT z:UNION A B. C z)
(INT a:A. B (f a)) = (INT x:f ` A. B x)
lemma image_mono:
A ⊆ B ==> f ` A ⊆ f ` B
lemma Pow_mono:
A ⊆ B ==> Pow A ⊆ Pow B
lemma Union_mono:
A ⊆ B ==> Union A ⊆ Union B
lemma Inter_anti_mono:
B ⊆ A ==> Inter A ⊆ Inter B
lemma UN_mono:
[| A ⊆ B; !!x. x ∈ A ==> f x ⊆ g x |] ==> (UN x:A. f x) ⊆ (UN x:B. g x)
lemma INT_anti_mono:
[| B ⊆ A; !!x. x ∈ A ==> f x ⊆ g x |] ==> (INT x:A. f x) ⊆ (INT x:A. g x)
lemma insert_mono:
C ⊆ D ==> insert a C ⊆ insert a D
lemma Un_mono:
[| A ⊆ C; B ⊆ D |] ==> A ∪ B ⊆ C ∪ D
lemma Int_mono:
[| A ⊆ C; B ⊆ D |] ==> A ∩ B ⊆ C ∩ D
lemma Diff_mono:
[| A ⊆ C; D ⊆ B |] ==> A - B ⊆ C - D
lemma Compl_anti_mono:
A ⊆ B ==> - B ⊆ - A
lemma in_mono:
A ⊆ B ==> x ∈ A --> x ∈ B
lemma conj_mono:
[| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∧ P2.0 --> Q1.0 ∧ Q2.0
lemma disj_mono:
[| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∨ P2.0 --> Q1.0 ∨ Q2.0
lemma imp_mono:
[| Q1.0 --> P1.0; P2.0 --> Q2.0 |] ==> (P1.0 --> P2.0) --> Q1.0 --> Q2.0
lemma imp_refl:
P --> P
lemma ex_mono:
(!!x. P x --> Q x) ==> (∃x. P x) --> (∃x. Q x)
lemma all_mono:
(!!x. P x --> Q x) ==> (∀x. P x) --> (∀x. Q x)
lemma Collect_mono:
(!!x. P x --> Q x) ==> Collect P ⊆ Collect Q
lemma Int_Collect_mono:
[| A ⊆ B; !!x. x ∈ A ==> P x --> Q x |] ==> A ∩ Collect P ⊆ B ∩ Collect Q
lemmas basic_monos:
A ⊆ A
P --> P
[| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∨ P2.0 --> Q1.0 ∨ Q2.0
[| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∧ P2.0 --> Q1.0 ∧ Q2.0
(!!x. P x --> Q x) ==> (∃x. P x) --> (∃x. Q x)
(!!x. P x --> Q x) ==> Collect P ⊆ Collect Q
A ⊆ B ==> x ∈ A --> x ∈ B
lemmas basic_monos:
A ⊆ A
P --> P
[| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∨ P2.0 --> Q1.0 ∨ Q2.0
[| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∧ P2.0 --> Q1.0 ∧ Q2.0
(!!x. P x --> Q x) ==> (∃x. P x) --> (∃x. Q x)
(!!x. P x --> Q x) ==> Collect P ⊆ Collect Q
A ⊆ B ==> x ∈ A --> x ∈ B
lemma eq_to_mono:
[| a = b; c = d; b --> d |] ==> a --> c
lemma eq_to_mono2:
[| a = b; c = d; ¬ b --> ¬ d |] ==> ¬ a --> ¬ c
lemma Least_mono:
[| mono f; ∃x∈S. ∀y∈S. x ≤ y |] ==> (LEAST y. y ∈ f ` S) = f (LEAST x. x ∈ S)
lemma vimage_eq:
(a ∈ f -` B) = (f a ∈ B)
lemma vimage_singleton_eq:
(a ∈ f -` {b}) = (f a = b)
lemma vimageI:
[| f a = b; b ∈ B |] ==> a ∈ f -` B
lemma vimageI2:
f a ∈ A ==> a ∈ f -` A
lemma vimageE:
[| a ∈ f -` B; !!x. [| f a = x; x ∈ B |] ==> P |] ==> P
lemma vimageD:
a ∈ f -` A ==> f a ∈ A
lemma vimage_empty:
f -` {} = {}
lemma vimage_Compl:
f -` (- A) = - f -` A
lemma vimage_Un:
f -` (A ∪ B) = f -` A ∪ f -` B
lemma vimage_Int:
f -` (A ∩ B) = f -` A ∩ f -` B
lemma vimage_Union:
f -` Union A = (UN X:A. f -` X)
lemma vimage_UN:
f -` (UN x:A. B x) = (UN x:A. f -` B x)
lemma vimage_INT:
f -` (INT x:A. B x) = (INT x:A. f -` B x)
lemma vimage_Collect_eq:
f -` Collect P = {y. P (f y)}
lemma vimage_Collect:
(!!x. P (f x) = Q x) ==> f -` Collect P = Collect Q
lemma vimage_insert:
f -` insert a B = f -` {a} ∪ f -` B
lemma vimage_Diff:
f -` (A - B) = f -` A - f -` B
lemma vimage_UNIV:
f -` UNIV = UNIV
lemma vimage_eq_UN:
f -` B = (UN y:B. f -` {y})
lemma vimage_mono:
A ⊆ B ==> f -` A ⊆ f -` B
lemma contents_eq:
contents {x} = x
lemma set_rev_mp:
[| x ∈ A; A ⊆ B |] ==> x ∈ B
lemma set_mp:
[| A ⊆ B; x ∈ A |] ==> x ∈ B
lemma ord_le_eq_trans:
[| a ≤ b; b = c |] ==> a ≤ c
lemma ord_eq_le_trans:
[| a = b; b ≤ c |] ==> a ≤ c
lemma ord_less_eq_trans:
[| a < b; b = c |] ==> a < c
lemma ord_eq_less_trans:
[| a = b; b < c |] ==> a < c
lemma order_less_subst2:
[| a < b; f b < c; !!x y. x < y ==> f x < f y |] ==> f a < c
lemma order_less_subst1:
[| a < f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
lemma order_le_less_subst2:
[| a ≤ b; f b < c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a < c
lemma order_le_less_subst1:
[| a ≤ f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
lemma order_less_le_subst2:
[| a < b; f b ≤ c; !!x y. x < y ==> f x < f y |] ==> f a < c
lemma order_less_le_subst1:
[| a < f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a < f c
lemma order_subst1:
[| a ≤ f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a ≤ f c
lemma order_subst2:
[| a ≤ b; f b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a ≤ c
lemma ord_le_eq_subst:
[| a ≤ b; f b = c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a ≤ c
lemma ord_eq_le_subst:
[| a = f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a ≤ f c
lemma ord_less_eq_subst:
[| a < b; f b = c; !!x y. x < y ==> f x < f y |] ==> f a < c
lemma ord_eq_less_subst:
[| a = f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
lemmas basic_trans_rules:
[| a < b; f b < c; !!x y. x < y ==> f x < f y |] ==> f a < c
[| a < f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
[| a ≤ b; f b < c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a < c
[| a ≤ f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
[| a < b; f b ≤ c; !!x y. x < y ==> f x < f y |] ==> f a < c
[| a < f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a < f c
[| a ≤ b; f b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a ≤ c
[| a ≤ f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a ≤ f c
[| a ≤ b; f b = c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a ≤ c
[| a = f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a ≤ f c
[| a < b; f b = c; !!x y. x < y ==> f x < f y |] ==> f a < c
[| a = f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
[| a = b; P b |] ==> P a
[| P a; a = b |] ==> P b
[| P; P --> Q |] ==> Q
[| P --> Q; P |] ==> Q
[| x ∈ A; A ⊆ B |] ==> x ∈ B
[| A ⊆ B; x ∈ A |] ==> x ∈ B
[| a ≠ b; a ≤ b |] ==> a < b
[| a ≤ b; a ≠ b |] ==> a < b
[| x < y; y < z |] ==> x < z
[| a < b; b < a |] ==> P
[| x ≤ y; y < z |] ==> x < z
[| x < y; y ≤ z |] ==> x < z
[| x ≤ y; y ≤ z |] ==> x ≤ z
[| x ≤ y; y ≤ x |] ==> x = y
[| a ≤ b; b = c |] ==> a ≤ c
[| a = b; b ≤ c |] ==> a ≤ c
[| a < b; b = c |] ==> a < c
[| a = b; b < c |] ==> a < c
[| r = s; s = t |] ==> r = t
lemmas basic_trans_rules:
[| a < b; f b < c; !!x y. x < y ==> f x < f y |] ==> f a < c
[| a < f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
[| a ≤ b; f b < c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a < c
[| a ≤ f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
[| a < b; f b ≤ c; !!x y. x < y ==> f x < f y |] ==> f a < c
[| a < f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a < f c
[| a ≤ b; f b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a ≤ c
[| a ≤ f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a ≤ f c
[| a ≤ b; f b = c; !!x y. x ≤ y ==> f x ≤ f y |] ==> f a ≤ c
[| a = f b; b ≤ c; !!x y. x ≤ y ==> f x ≤ f y |] ==> a ≤ f c
[| a < b; f b = c; !!x y. x < y ==> f x < f y |] ==> f a < c
[| a = f b; b < c; !!x y. x < y ==> f x < f y |] ==> a < f c
[| a = b; P b |] ==> P a
[| P a; a = b |] ==> P b
[| P; P --> Q |] ==> Q
[| P --> Q; P |] ==> Q
[| x ∈ A; A ⊆ B |] ==> x ∈ B
[| A ⊆ B; x ∈ A |] ==> x ∈ B
[| a ≠ b; a ≤ b |] ==> a < b
[| a ≤ b; a ≠ b |] ==> a < b
[| x < y; y < z |] ==> x < z
[| a < b; b < a |] ==> P
[| x ≤ y; y < z |] ==> x < z
[| x < y; y ≤ z |] ==> x < z
[| x ≤ y; y ≤ z |] ==> x ≤ z
[| x ≤ y; y ≤ x |] ==> x = y
[| a ≤ b; b = c |] ==> a ≤ c
[| a = b; b ≤ c |] ==> a ≤ c
[| a < b; b = c |] ==> a < c
[| a = b; b < c |] ==> a < c
[| r = s; s = t |] ==> r = t