# Theory equalities

Up to index of Isabelle/ZF

theory equalities
imports pair
`(*  Title:      ZF/equalities.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1992  University of Cambridge*)header{*Basic Equalities and Inclusions*}theory equalities imports pair begintext{*These cover union, intersection, converse, domain, range, etc.  Philippede Groote proved many of the inclusions.*}lemma in_mono: "A⊆B ==> x∈A --> x∈B"by blastlemma the_eq_0 [simp]: "(THE x. False) = 0"by (blast intro: the_0)subsection{*Bounded Quantifiers*}text {* \medskip  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 blastlemma bex_Un: "(∃x ∈ A∪B. P(x)) <-> (∃x ∈ A. P(x)) | (∃x ∈ B. P(x))";  by blastlemma ball_UN: "(∀z ∈ (\<Union>x∈A. B(x)). P(z)) <-> (∀x∈A. ∀z ∈ B(x). P(z))"  by blastlemma bex_UN: "(∃z ∈ (\<Union>x∈A. B(x)). P(z)) <-> (∃x∈A. ∃z∈B(x). P(z))"  by blastsubsection{*Converse of a Relation*}lemma converse_iff [simp]: "<a,b>∈ converse(r) <-> <b,a>∈r"by (unfold converse_def, blast)lemma converseI [intro!]: "<a,b>∈r ==> <b,a>∈converse(r)"by (unfold converse_def, blast)lemma converseD: "<a,b> ∈ converse(r) ==> <b,a> ∈ r"by (unfold converse_def, blast)lemma converseE [elim!]:    "[| yx ∈ converse(r);        !!x y. [| yx=<y,x>;  <x,y>∈r |] ==> P |]     ==> P"by (unfold converse_def, blast)lemma converse_converse: "r⊆Sigma(A,B) ==> converse(converse(r)) = r"by blastlemma converse_type: "r⊆A*B ==> converse(r)⊆B*A"by blastlemma converse_prod [simp]: "converse(A*B) = B*A"by blastlemma converse_empty [simp]: "converse(0) = 0"by blastlemma converse_subset_iff:     "A ⊆ Sigma(X,Y) ==> converse(A) ⊆ converse(B) <-> A ⊆ B"by blastsubsection{*Finite Set Constructions Using @{term cons}*}lemma cons_subsetI: "[| a∈C; B⊆C |] ==> cons(a,B) ⊆ C"by blastlemma subset_consI: "B ⊆ cons(a,B)"by blastlemma cons_subset_iff [iff]: "cons(a,B)⊆C <-> a∈C & B⊆C"by blast(*A safe special case of subset elimination, adding no new variables  [| cons(a,B) ⊆ C; [| a ∈ C; B ⊆ C |] ==> R |] ==> R *)lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]lemma subset_empty_iff: "A⊆0 <-> A=0"by blastlemma subset_cons_iff: "C⊆cons(a,B) <-> C⊆B | (a∈C & C-{a} ⊆ B)"by blast(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)lemma cons_eq: "{a} ∪ B = cons(a,B)"by blastlemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"by blastlemma cons_absorb: "a: B ==> cons(a,B) = B"by blastlemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"by blastlemma Diff_cons_eq: "cons(a,B) - C = (if a∈C then B-C else cons(a,B-C))"by autolemma equal_singleton [rule_format]: "[| a: C;  ∀y∈C. y=b |] ==> C = {b}"by blastlemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"by blast(** singletons **)lemma singleton_subsetI: "a∈C ==> {a} ⊆ C"by blastlemma singleton_subsetD: "{a} ⊆ C  ==>  a∈C"by blast(** succ **)lemma subset_succI: "i ⊆ succ(i)"by blast(*But if j is an ordinal or is transitive, then @{term"i∈j"} implies @{term"i⊆j"}!  See @{text"Ord_succ_subsetI}*)lemma succ_subsetI: "[| i∈j;  i⊆j |] ==> succ(i)⊆j"by (unfold succ_def, blast)lemma succ_subsetE:    "[| succ(i) ⊆ j;  [| i∈j;  i⊆j |] ==> P |] ==> P"by (unfold succ_def, blast)lemma succ_subset_iff: "succ(a) ⊆ B <-> (a ⊆ B & a ∈ B)"by (unfold succ_def, blast)subsection{*Binary Intersection*}(** Intersection is the greatest lower bound of two sets **)lemma Int_subset_iff: "C ⊆ A ∩ B <-> C ⊆ A & C ⊆ B"by blastlemma Int_lower1: "A ∩ B ⊆ A"by blastlemma Int_lower2: "A ∩ B ⊆ B"by blastlemma Int_greatest: "[| C⊆A;  C⊆B |] ==> C ⊆ A ∩ B"by blastlemma Int_cons: "cons(a,B) ∩ C ⊆ cons(a, B ∩ C)"by blastlemma Int_absorb [simp]: "A ∩ A = A"by blastlemma Int_left_absorb: "A ∩ (A ∩ B) = A ∩ B"by blastlemma Int_commute: "A ∩ B = B ∩ A"by blastlemma Int_left_commute: "A ∩ (B ∩ C) = B ∩ (A ∩ C)"by blastlemma Int_assoc: "(A ∩ B) ∩ C  =  A ∩ (B ∩ C)"by blast(*Intersection is an AC-operator*)lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commutelemma Int_absorb1: "B ⊆ A ==> A ∩ B = B"  by blastlemma Int_absorb2: "A ⊆ B ==> A ∩ B = A"  by blastlemma Int_Un_distrib: "A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)"by blastlemma Int_Un_distrib2: "(B ∪ C) ∩ A = (B ∩ A) ∪ (C ∩ A)"by blastlemma subset_Int_iff: "A⊆B <-> A ∩ B = A"by (blast elim!: equalityE)lemma subset_Int_iff2: "A⊆B <-> B ∩ A = A"by (blast elim!: equalityE)lemma Int_Diff_eq: "C⊆A ==> (A-B) ∩ C = C-B"by blastlemma Int_cons_left:     "cons(a,A) ∩ B = (if a ∈ B then cons(a, A ∩ B) else A ∩ B)"by autolemma Int_cons_right:     "A ∩ cons(a, B) = (if a ∈ A then cons(a, A ∩ B) else A ∩ B)"by autolemma cons_Int_distrib: "cons(x, A ∩ B) = cons(x, A) ∩ cons(x, B)"by autosubsection{*Binary Union*}(** Union is the least upper bound of two sets *)lemma Un_subset_iff: "A ∪ B ⊆ C <-> A ⊆ C & B ⊆ C"by blastlemma Un_upper1: "A ⊆ A ∪ B"by blastlemma Un_upper2: "B ⊆ A ∪ B"by blastlemma Un_least: "[| A⊆C;  B⊆C |] ==> A ∪ B ⊆ C"by blastlemma Un_cons: "cons(a,B) ∪ C = cons(a, B ∪ C)"by blastlemma Un_absorb [simp]: "A ∪ A = A"by blastlemma Un_left_absorb: "A ∪ (A ∪ B) = A ∪ B"by blastlemma Un_commute: "A ∪ B = B ∪ A"by blastlemma Un_left_commute: "A ∪ (B ∪ C) = B ∪ (A ∪ C)"by blastlemma Un_assoc: "(A ∪ B) ∪ C  =  A ∪ (B ∪ C)"by blast(*Union is an AC-operator*)lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commutelemma Un_absorb1: "A ⊆ B ==> A ∪ B = B"  by blastlemma Un_absorb2: "B ⊆ A ==> A ∪ B = A"  by blastlemma Un_Int_distrib: "(A ∩ B) ∪ C  =  (A ∪ C) ∩ (B ∪ C)"by blastlemma subset_Un_iff: "A⊆B <-> A ∪ B = B"by (blast elim!: equalityE)lemma subset_Un_iff2: "A⊆B <-> B ∪ A = B"by (blast elim!: equalityE)lemma Un_empty [iff]: "(A ∪ B = 0) <-> (A = 0 & B = 0)"by blastlemma Un_eq_Union: "A ∪ B = \<Union>({A, B})"by blastsubsection{*Set Difference*}lemma Diff_subset: "A-B ⊆ A"by blastlemma Diff_contains: "[| C⊆A;  C ∩ B = 0 |] ==> C ⊆ A-B"by blastlemma subset_Diff_cons_iff: "B ⊆ A - cons(c,C)  <->  B⊆A-C & c ∉ B"by blastlemma Diff_cancel: "A - A = 0"by blastlemma Diff_triv: "A  ∩ B = 0 ==> A - B = A"by blastlemma empty_Diff [simp]: "0 - A = 0"by blastlemma Diff_0 [simp]: "A - 0 = A"by blastlemma Diff_eq_0_iff: "A - B = 0 <-> A ⊆ B"by (blast elim: equalityE)(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)lemma Diff_cons: "A - cons(a,B) = A - B - {a}"by blast(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"by blastlemma Diff_disjoint: "A ∩ (B-A) = 0"by blastlemma Diff_partition: "A⊆B ==> A ∪ (B-A) = B"by blastlemma subset_Un_Diff: "A ⊆ B ∪ (A - B)"by blastlemma double_complement: "[| A⊆B; B⊆C |] ==> B-(C-A) = A"by blastlemma double_complement_Un: "(A ∪ B) - (B-A) = A"by blastlemma Un_Int_crazy: "(A ∩ B) ∪ (B ∩ C) ∪ (C ∩ A) = (A ∪ B) ∩ (B ∪ C) ∩ (C ∪ A)"apply blastdonelemma Diff_Un: "A - (B ∪ C) = (A-B) ∩ (A-C)"by blastlemma Diff_Int: "A - (B ∩ C) = (A-B) ∪ (A-C)"by blastlemma Un_Diff: "(A ∪ B) - C = (A - C) ∪ (B - C)"by blastlemma Int_Diff: "(A ∩ B) - C = A ∩ (B - C)"by blastlemma Diff_Int_distrib: "C ∩ (A-B) = (C ∩ A) - (C ∩ B)"by blastlemma Diff_Int_distrib2: "(A-B) ∩ C = (A ∩ C) - (B ∩ C)"by blast(*Halmos, Naive Set Theory, page 16.*)lemma Un_Int_assoc_iff: "(A ∩ B) ∪ C = A ∩ (B ∪ C)  <->  C⊆A"by (blast elim!: equalityE)subsection{*Big Union and Intersection*}(** Big Union is the least upper bound of a set  **)lemma Union_subset_iff: "\<Union>(A) ⊆ C <-> (∀x∈A. x ⊆ C)"by blastlemma Union_upper: "B∈A ==> B ⊆ \<Union>(A)"by blastlemma Union_least: "[| !!x. x∈A ==> x⊆C |] ==> \<Union>(A) ⊆ C"by blastlemma Union_cons [simp]: "\<Union>(cons(a,B)) = a ∪ \<Union>(B)"by blastlemma Union_Un_distrib: "\<Union>(A ∪ B) = \<Union>(A) ∪ \<Union>(B)"by blastlemma Union_Int_subset: "\<Union>(A ∩ B) ⊆ \<Union>(A) ∩ \<Union>(B)"by blastlemma Union_disjoint: "\<Union>(C) ∩ A = 0 <-> (∀B∈C. B ∩ A = 0)"by (blast elim!: equalityE)lemma Union_empty_iff: "\<Union>(A) = 0 <-> (∀B∈A. B=0)"by blastlemma Int_Union2: "\<Union>(B) ∩ A = (\<Union>C∈B. C ∩ A)"by blast(** Big Intersection is the greatest lower bound of a nonempty set **)lemma Inter_subset_iff: "A≠0  ==>  C ⊆ \<Inter>(A) <-> (∀x∈A. C ⊆ x)"by blastlemma Inter_lower: "B∈A ==> \<Inter>(A) ⊆ B"by blastlemma Inter_greatest: "[| A≠0;  !!x. x∈A ==> C⊆x |] ==> C ⊆ \<Inter>(A)"by blast(** Intersection of a family of sets  **)lemma INT_lower: "x∈A ==> (\<Inter>x∈A. B(x)) ⊆ B(x)"by blastlemma INT_greatest: "[| A≠0;  !!x. x∈A ==> C⊆B(x) |] ==> C ⊆ (\<Inter>x∈A. B(x))"by forcelemma Inter_0 [simp]: "\<Inter>(0) = 0"by (unfold Inter_def, blast)lemma Inter_Un_subset:     "[| z∈A; z∈B |] ==> \<Inter>(A) ∪ \<Inter>(B) ⊆ \<Inter>(A ∩ B)"by blast(* A good challenge: Inter is ill-behaved on the empty set *)lemma Inter_Un_distrib:     "[| A≠0;  B≠0 |] ==> \<Inter>(A ∪ B) = \<Inter>(A) ∩ \<Inter>(B)"by blastlemma Union_singleton: "\<Union>({b}) = b"by blastlemma Inter_singleton: "\<Inter>({b}) = b"by blastlemma Inter_cons [simp]:     "\<Inter>(cons(a,B)) = (if B=0 then a else a ∩ \<Inter>(B))"by forcesubsection{*Unions and Intersections of Families*}lemma subset_UN_iff_eq: "A ⊆ (\<Union>i∈I. B(i)) <-> A = (\<Union>i∈I. A ∩ B(i))"by (blast elim!: equalityE)lemma UN_subset_iff: "(\<Union>x∈A. B(x)) ⊆ C <-> (∀x∈A. B(x) ⊆ C)"by blastlemma UN_upper: "x∈A ==> B(x) ⊆ (\<Union>x∈A. B(x))"by (erule RepFunI [THEN Union_upper])lemma UN_least: "[| !!x. x∈A ==> B(x)⊆C |] ==> (\<Union>x∈A. B(x)) ⊆ C"by blastlemma Union_eq_UN: "\<Union>(A) = (\<Union>x∈A. x)"by blastlemma Inter_eq_INT: "\<Inter>(A) = (\<Inter>x∈A. x)"by (unfold Inter_def, blast)lemma UN_0 [simp]: "(\<Union>i∈0. A(i)) = 0"by blastlemma UN_singleton: "(\<Union>x∈A. {x}) = A"by blastlemma UN_Un: "(\<Union>i∈ A ∪ B. C(i)) = (\<Union>i∈ A. C(i)) ∪ (\<Union>i∈B. C(i))"by blastlemma INT_Un: "(\<Inter>i∈I ∪ J. A(i)) =               (if I=0 then \<Inter>j∈J. A(j)                       else if J=0 then \<Inter>i∈I. A(i)                       else ((\<Inter>i∈I. A(i)) ∩  (\<Inter>j∈J. A(j))))"by (simp, blast intro!: equalityI)lemma UN_UN_flatten: "(\<Union>x ∈ (\<Union>y∈A. B(y)). C(x)) = (\<Union>y∈A. \<Union>x∈ B(y). C(x))"by blast(*Halmos, Naive Set Theory, page 35.*)lemma Int_UN_distrib: "B ∩ (\<Union>i∈I. A(i)) = (\<Union>i∈I. B ∩ A(i))"by blastlemma Un_INT_distrib: "I≠0 ==> B ∪ (\<Inter>i∈I. A(i)) = (\<Inter>i∈I. B ∪ A(i))"by autolemma Int_UN_distrib2:     "(\<Union>i∈I. A(i)) ∩ (\<Union>j∈J. B(j)) = (\<Union>i∈I. \<Union>j∈J. A(i) ∩ B(j))"by blastlemma Un_INT_distrib2: "[| I≠0;  J≠0 |] ==>      (\<Inter>i∈I. A(i)) ∪ (\<Inter>j∈J. B(j)) = (\<Inter>i∈I. \<Inter>j∈J. A(i) ∪ B(j))"by autolemma UN_constant [simp]: "(\<Union>y∈A. c) = (if A=0 then 0 else c)"by forcelemma INT_constant [simp]: "(\<Inter>y∈A. c) = (if A=0 then 0 else c)"by forcelemma UN_RepFun [simp]: "(\<Union>y∈ RepFun(A,f). B(y)) = (\<Union>x∈A. B(f(x)))"by blastlemma INT_RepFun [simp]: "(\<Inter>x∈RepFun(A,f). B(x))    = (\<Inter>a∈A. B(f(a)))"by (auto simp add: Inter_def)lemma INT_Union_eq:     "0 ∉ A ==> (\<Inter>x∈ \<Union>(A). B(x)) = (\<Inter>y∈A. \<Inter>x∈y. B(x))"apply (subgoal_tac "∀x∈A. x≠0") prefer 2 apply blastapply (force simp add: Inter_def ball_conj_distrib)donelemma INT_UN_eq:     "(∀x∈A. B(x) ≠ 0)      ==> (\<Inter>z∈ (\<Union>x∈A. B(x)). C(z)) = (\<Inter>x∈A. \<Inter>z∈ B(x). C(z))"apply (subst INT_Union_eq, blast)apply (simp add: Inter_def)done(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:    Union of a family of unions **)lemma UN_Un_distrib:     "(\<Union>i∈I. A(i) ∪ B(i)) = (\<Union>i∈I. A(i))  ∪  (\<Union>i∈I. B(i))"by blastlemma INT_Int_distrib:     "I≠0 ==> (\<Inter>i∈I. A(i) ∩ B(i)) = (\<Inter>i∈I. A(i)) ∩ (\<Inter>i∈I. B(i))"by (blast elim!: not_emptyE)lemma UN_Int_subset:     "(\<Union>z∈I ∩ J. A(z)) ⊆ (\<Union>z∈I. A(z)) ∩ (\<Union>z∈J. A(z))"by blast(** Devlin, page 12, exercise 5: Complements **)lemma Diff_UN: "I≠0 ==> B - (\<Union>i∈I. A(i)) = (\<Inter>i∈I. B - A(i))"by (blast elim!: not_emptyE)lemma Diff_INT: "I≠0 ==> B - (\<Inter>i∈I. A(i)) = (\<Union>i∈I. B - A(i))"by (blast elim!: not_emptyE)(** Unions and Intersections with General Sum **)(*Not suitable for rewriting: LOOPS!*)lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) ∪ Sigma(B,C)"by blast(*Not suitable for rewriting: LOOPS!*)lemma Sigma_cons2: "A * cons(b,B) = A*{b} ∪ A*B"by blastlemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) ∪ Sigma(A,B)"by blastlemma Sigma_succ2: "A * succ(B) = A*{B} ∪ A*B"by blastlemma SUM_UN_distrib1:     "(Σ x ∈ (\<Union>y∈A. C(y)). B(x)) = (\<Union>y∈A. Σ x∈C(y). B(x))"by blastlemma SUM_UN_distrib2:     "(Σ i∈I. \<Union>j∈J. C(i,j)) = (\<Union>j∈J. Σ i∈I. C(i,j))"by blastlemma SUM_Un_distrib1:     "(Σ i∈I ∪ J. C(i)) = (Σ i∈I. C(i)) ∪ (Σ j∈J. C(j))"by blastlemma SUM_Un_distrib2:     "(Σ i∈I. A(i) ∪ B(i)) = (Σ i∈I. A(i)) ∪ (Σ i∈I. B(i))"by blast(*First-order version of the above, for rewriting*)lemma prod_Un_distrib2: "I * (A ∪ B) = I*A ∪ I*B"by (rule SUM_Un_distrib2)lemma SUM_Int_distrib1:     "(Σ i∈I ∩ J. C(i)) = (Σ i∈I. C(i)) ∩ (Σ j∈J. C(j))"by blastlemma SUM_Int_distrib2:     "(Σ i∈I. A(i) ∩ B(i)) = (Σ i∈I. A(i)) ∩ (Σ i∈I. B(i))"by blast(*First-order version of the above, for rewriting*)lemma prod_Int_distrib2: "I * (A ∩ B) = I*A ∩ I*B"by (rule SUM_Int_distrib2)(*Cf Aczel, Non-Well-Founded Sets, page 115*)lemma SUM_eq_UN: "(Σ i∈I. A(i)) = (\<Union>i∈I. {i} * A(i))"by blastlemma times_subset_iff:     "(A'*B' ⊆ A*B) <-> (A' = 0 | B' = 0 | (A'⊆A) & (B'⊆B))"by blastlemma Int_Sigma_eq:     "(Σ x ∈ A'. B'(x)) ∩ (Σ x ∈ A. B(x)) = (Σ x ∈ A' ∩ A. B'(x) ∩ B(x))"by blast(** Domain **)lemma domain_iff: "a: domain(r) <-> (∃y. <a,y>∈ r)"by (unfold domain_def, blast)lemma domainI [intro]: "<a,b>∈ r ==> a: domain(r)"by (unfold domain_def, blast)lemma domainE [elim!]:    "[| a ∈ domain(r);  !!y. <a,y>∈ r ==> P |] ==> P"by (unfold domain_def, blast)lemma domain_subset: "domain(Sigma(A,B)) ⊆ A"by blastlemma domain_of_prod: "b∈B ==> domain(A*B) = A"by blastlemma domain_0 [simp]: "domain(0) = 0"by blastlemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"by blastlemma domain_Un_eq [simp]: "domain(A ∪ B) = domain(A) ∪ domain(B)"by blastlemma domain_Int_subset: "domain(A ∩ B) ⊆ domain(A) ∩ domain(B)"by blastlemma domain_Diff_subset: "domain(A) - domain(B) ⊆ domain(A - B)"by blastlemma domain_UN: "domain(\<Union>x∈A. B(x)) = (\<Union>x∈A. domain(B(x)))"by blastlemma domain_Union: "domain(\<Union>(A)) = (\<Union>x∈A. domain(x))"by blast(** Range **)lemma rangeI [intro]: "<a,b>∈ r ==> b ∈ range(r)"apply (unfold range_def)apply (erule converseI [THEN domainI])donelemma rangeE [elim!]: "[| b ∈ range(r);  !!x. <x,b>∈ r ==> P |] ==> P"by (unfold range_def, blast)lemma range_subset: "range(A*B) ⊆ B"apply (unfold range_def)apply (subst converse_prod)apply (rule domain_subset)donelemma range_of_prod: "a∈A ==> range(A*B) = B"by blastlemma range_0 [simp]: "range(0) = 0"by blastlemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"by blastlemma range_Un_eq [simp]: "range(A ∪ B) = range(A) ∪ range(B)"by blastlemma range_Int_subset: "range(A ∩ B) ⊆ range(A) ∩ range(B)"by blastlemma range_Diff_subset: "range(A) - range(B) ⊆ range(A - B)"by blastlemma domain_converse [simp]: "domain(converse(r)) = range(r)"by blastlemma range_converse [simp]: "range(converse(r)) = domain(r)"by blast(** Field **)lemma fieldI1: "<a,b>∈ r ==> a ∈ field(r)"by (unfold field_def, blast)lemma fieldI2: "<a,b>∈ r ==> b ∈ field(r)"by (unfold field_def, blast)lemma fieldCI [intro]:    "(~ <c,a>∈r ==> <a,b>∈ r) ==> a ∈ field(r)"apply (unfold field_def, blast)donelemma fieldE [elim!]:     "[| a ∈ field(r);         !!x. <a,x>∈ r ==> P;         !!x. <x,a>∈ r ==> P        |] ==> P"by (unfold field_def, blast)lemma field_subset: "field(A*B) ⊆ A ∪ B"by blastlemma domain_subset_field: "domain(r) ⊆ field(r)"apply (unfold field_def)apply (rule Un_upper1)donelemma range_subset_field: "range(r) ⊆ field(r)"apply (unfold field_def)apply (rule Un_upper2)donelemma domain_times_range: "r ⊆ Sigma(A,B) ==> r ⊆ domain(r)*range(r)"by blastlemma field_times_field: "r ⊆ Sigma(A,B) ==> r ⊆ field(r)*field(r)"by blastlemma relation_field_times_field: "relation(r) ==> r ⊆ field(r)*field(r)"by (simp add: relation_def, blast)lemma field_of_prod: "field(A*A) = A"by blastlemma field_0 [simp]: "field(0) = 0"by blastlemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"by blastlemma field_Un_eq [simp]: "field(A ∪ B) = field(A) ∪ field(B)"by blastlemma field_Int_subset: "field(A ∩ B) ⊆ field(A) ∩ field(B)"by blastlemma field_Diff_subset: "field(A) - field(B) ⊆ field(A - B)"by blastlemma field_converse [simp]: "field(converse(r)) = field(r)"by blast(** The Union of a set of relations is a relation -- Lemma for fun_Union **)lemma rel_Union: "(∀x∈S. ∃A B. x ⊆ A*B) ==>                  \<Union>(S) ⊆ domain(\<Union>(S)) * range(\<Union>(S))"by blast(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)lemma rel_Un: "[| r ⊆ A*B;  s ⊆ C*D |] ==> (r ∪ s) ⊆ (A ∪ C) * (B ∪ D)"by blastlemma domain_Diff_eq: "[| <a,c> ∈ r; c≠b |] ==> domain(r-{<a,b>}) = domain(r)"by blastlemma range_Diff_eq: "[| <c,b> ∈ r; c≠a |] ==> range(r-{<a,b>}) = range(r)"by blastsubsection{*Image of a Set under a Function or Relation*}lemma image_iff: "b ∈ r``A <-> (∃x∈A. <x,b>∈r)"by (unfold image_def, blast)lemma image_singleton_iff: "b ∈ r``{a} <-> <a,b>∈r"by (rule image_iff [THEN iff_trans], blast)lemma imageI [intro]: "[| <a,b>∈ r;  a∈A |] ==> b ∈ r``A"by (unfold image_def, blast)lemma imageE [elim!]:    "[| b: r``A;  !!x.[| <x,b>∈ r;  x∈A |] ==> P |] ==> P"by (unfold image_def, blast)lemma image_subset: "r ⊆ A*B ==> r``C ⊆ B"by blastlemma image_0 [simp]: "r``0 = 0"by blastlemma image_Un [simp]: "r``(A ∪ B) = (r``A) ∪ (r``B)"by blastlemma image_UN: "r `` (\<Union>x∈A. B(x)) = (\<Union>x∈A. r `` B(x))"by blastlemma Collect_image_eq:     "{z ∈ Sigma(A,B). P(z)} `` C = (\<Union>x ∈ A. {y ∈ B(x). x ∈ C & P(<x,y>)})"by blastlemma image_Int_subset: "r``(A ∩ B) ⊆ (r``A) ∩ (r``B)"by blastlemma image_Int_square_subset: "(r ∩ A*A)``B ⊆ (r``B) ∩ A"by blastlemma image_Int_square: "B⊆A ==> (r ∩ A*A)``B = (r``B) ∩ A"by blast(*Image laws for special relations*)lemma image_0_left [simp]: "0``A = 0"by blastlemma image_Un_left: "(r ∪ s)``A = (r``A) ∪ (s``A)"by blastlemma image_Int_subset_left: "(r ∩ s)``A ⊆ (r``A) ∩ (s``A)"by blastsubsection{*Inverse Image of a Set under a Function or Relation*}lemma vimage_iff:    "a ∈ r-``B <-> (∃y∈B. <a,y>∈r)"by (unfold vimage_def image_def converse_def, blast)lemma vimage_singleton_iff: "a ∈ r-``{b} <-> <a,b>∈r"by (rule vimage_iff [THEN iff_trans], blast)lemma vimageI [intro]: "[| <a,b>∈ r;  b∈B |] ==> a ∈ r-``B"by (unfold vimage_def, blast)lemma vimageE [elim!]:    "[| a: r-``B;  !!x.[| <a,x>∈ r;  x∈B |] ==> P |] ==> P"apply (unfold vimage_def, blast)donelemma vimage_subset: "r ⊆ A*B ==> r-``C ⊆ A"apply (unfold vimage_def)apply (erule converse_type [THEN image_subset])donelemma vimage_0 [simp]: "r-``0 = 0"by blastlemma vimage_Un [simp]: "r-``(A ∪ B) = (r-``A) ∪ (r-``B)"by blastlemma vimage_Int_subset: "r-``(A ∩ B) ⊆ (r-``A) ∩ (r-``B)"by blast(*NOT suitable for rewriting*)lemma vimage_eq_UN: "f -``B = (\<Union>y∈B. f-``{y})"by blastlemma function_vimage_Int:     "function(f) ==> f-``(A ∩ B) = (f-``A)  ∩  (f-``B)"by (unfold function_def, blast)lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"by (unfold function_def, blast)lemma function_image_vimage: "function(f) ==> f `` (f-`` A) ⊆ A"by (unfold function_def, blast)lemma vimage_Int_square_subset: "(r ∩ A*A)-``B ⊆ (r-``B) ∩ A"by blastlemma vimage_Int_square: "B⊆A ==> (r ∩ A*A)-``B = (r-``B) ∩ A"by blast(*Invese image laws for special relations*)lemma vimage_0_left [simp]: "0-``A = 0"by blastlemma vimage_Un_left: "(r ∪ s)-``A = (r-``A) ∪ (s-``A)"by blastlemma vimage_Int_subset_left: "(r ∩ s)-``A ⊆ (r-``A) ∩ (s-``A)"by blast(** Converse **)lemma converse_Un [simp]: "converse(A ∪ B) = converse(A) ∪ converse(B)"by blastlemma converse_Int [simp]: "converse(A ∩ B) = converse(A) ∩ converse(B)"by blastlemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"by blastlemma converse_UN [simp]: "converse(\<Union>x∈A. B(x)) = (\<Union>x∈A. converse(B(x)))"by blast(*Unfolding Inter avoids using excluded middle on A=0*)lemma converse_INT [simp]:     "converse(\<Inter>x∈A. B(x)) = (\<Inter>x∈A. converse(B(x)))"apply (unfold Inter_def, blast)donesubsection{*Powerset Operator*}lemma Pow_0 [simp]: "Pow(0) = {0}"by blastlemma Pow_insert: "Pow (cons(a,A)) = Pow(A) ∪ {cons(a,X) . X: Pow(A)}"apply (rule equalityI, safe)apply (erule swap)apply (rule_tac a = "x-{a}" in RepFun_eqI, auto)donelemma Un_Pow_subset: "Pow(A) ∪ Pow(B) ⊆ Pow(A ∪ B)"by blastlemma UN_Pow_subset: "(\<Union>x∈A. Pow(B(x))) ⊆ Pow(\<Union>x∈A. B(x))"by blastlemma subset_Pow_Union: "A ⊆ Pow(\<Union>(A))"by blastlemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"by blastlemma Union_Pow_iff: "\<Union>(A) ∈ Pow(B) <-> A ∈ Pow(Pow(B))"by blastlemma Pow_Int_eq [simp]: "Pow(A ∩ B) = Pow(A) ∩ Pow(B)"by blastlemma Pow_INT_eq: "A≠0 ==> Pow(\<Inter>x∈A. B(x)) = (\<Inter>x∈A. Pow(B(x)))"by (blast elim!: not_emptyE)subsection{*RepFun*}lemma RepFun_subset: "[| !!x. x∈A ==> f(x) ∈ B |] ==> {f(x). x∈A} ⊆ B"by blastlemma RepFun_eq_0_iff [simp]: "{f(x).x∈A}=0 <-> A=0"by blastlemma RepFun_constant [simp]: "{c. x∈A} = (if A=0 then 0 else {c})"by forcesubsection{*Collect*}lemma Collect_subset: "Collect(A,P) ⊆ A"by blastlemma Collect_Un: "Collect(A ∪ B, P) = Collect(A,P) ∪ Collect(B,P)"by blastlemma Collect_Int: "Collect(A ∩ B, P) = Collect(A,P) ∩ Collect(B,P)"by blastlemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"by blastlemma Collect_cons: "{x∈cons(a,B). P(x)} =      (if P(a) then cons(a, {x∈B. P(x)}) else {x∈B. P(x)})"by (simp, blast)lemma Int_Collect_self_eq: "A ∩ Collect(A,P) = Collect(A,P)"by blastlemma Collect_Collect_eq [simp]:     "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"by blastlemma Collect_Int_Collect_eq:     "Collect(A,P) ∩ Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"by blastlemma Collect_Union_eq [simp]:     "Collect(\<Union>x∈A. B(x), P) = (\<Union>x∈A. Collect(B(x), P))"by blastlemma Collect_Int_left: "{x∈A. P(x)} ∩ B = {x ∈ A ∩ B. P(x)}"by blastlemma Collect_Int_right: "A ∩ {x∈B. P(x)} = {x ∈ A ∩ B. P(x)}"by blastlemma Collect_disj_eq: "{x∈A. P(x) | Q(x)} = Collect(A, P) ∪ Collect(A, Q)"by blastlemma Collect_conj_eq: "{x∈A. P(x) & Q(x)} = Collect(A, P) ∩ Collect(A, Q)"by blastlemmas subset_SIs = subset_refl cons_subsetI subset_consI                    Union_least UN_least Un_least                    Inter_greatest Int_greatest RepFun_subset                    Un_upper1 Un_upper2 Int_lower1 Int_lower2ML {*val subset_cs =  claset_of (@{context}    delrules [@{thm subsetI}, @{thm subsetCE}]    addSIs @{thms subset_SIs}    addIs  [@{thm Union_upper}, @{thm Inter_lower}]    addSEs [@{thm cons_subsetE}]);val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);*}end`