Quelle  equalities.thy

(*  Title:      ZF/equalities.thy
  Author: Lawrence C Paulson, Cambridge University Computer Laboratory
  Copyright 1992 University of Cambridge
*)

section‹Basic Equalities and Inclusions›

theory equalities imports pair begin

text‹These cover union, intersection, converse, domain, range, etc. Philippe
 de Groote proved many of the inclusions.›

lemma in_mono: "A⊆B ==> x∈A ⟶ x∈B"
by blast

lemma 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 ‹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 ∈ (∪x∈A. B(x)). P(z)) ⟷ (∀x∈A. ∀z ∈ B(x). P(z))"
  by blast

lemma bex_UN: "(∃z ∈ (∪x∈A. B(x)). P(z)) ⟷ (∃x∈A. ∃z∈B(x). P(z))"
  by blast

subsection‹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 blast

lemma converse_type: "r⊆A*B ==> converse(r)⊆B*A"
by blast

lemma converse_prod [simp]: "converse(A*B) = B*A"
by blast

lemma converse_empty [simp]: "converse(0) = 0"
by blast

lemma converse_subset_iff:
     "A ⊆ Sigma(X,Y) ==> converse(A) ⊆ converse(B) ⟷ A ⊆ B"
by blast


subsection‹Finite Set Constructions Using 🍋‹cons›\›

lemma cons_subsetI: "[a∈C; B⊆C] ==> cons(a,B) ⊆ C"
by blast

lemma subset_consI: "B ⊆ cons(a,B)"
by blast

lemma 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
  \<lbrakk>cons(a,B) \<subseteq> C; \<lbrakk>a \<in> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R *)
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]

lemma subset_empty_iff: "A⊆0 ⟷ A=0"
by blast

lemma 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 blast

lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
by blast

lemma cons_absorb: "a: B ==> cons(a,B) = B"
by blast

lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
by blast

lemma Diff_cons_eq: "cons(a,B) - C = (if a∈C then B-C else cons(a,B-C))"
by auto

lemma equal_singleton: "[a: C; ∧y. y ∈C ==> y=b] ==> C = {b}"
by blast

lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
by blast

(** singletons **)

lemma singleton_subsetI: "a∈C ==> {a} ⊆ C"
by blast

lemma 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\<in>j"} implies @{term"i\<subseteq>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 blast

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

lemma Int_cons: "cons(a,B) ∩ C ⊆ cons(a, B ∩ C)"
by blast

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

(*Intersection is an AC-operator*)
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute

lemma Int_absorb1: "B ⊆ A ==> A ∩ B = B"
  by blast

lemma Int_absorb2: "A ⊆ B ==> A ∩ B = A"
  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 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 blast

lemma Int_cons_left:
     "cons(a,A) ∩ B = (if a ∈ B then cons(a, A ∩ B) else A ∩ B)"
by auto

lemma Int_cons_right:
     "A ∩ cons(a, B) = (if a ∈ A then cons(a, A ∩ B) else A ∩ B)"
by auto

lemma cons_Int_distrib: "cons(x, A ∩ B) = cons(x, A) ∩ cons(x, B)"
by auto

subsection‹Binary Union›

(** Union is the least upper bound of two sets *)

lemma Un_subset_iff: "A ∪ B ⊆ C ⟷ A ⊆ C ∧ B ⊆ C"
by blast

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

lemma Un_cons: "cons(a,B) ∪ C = cons(a, B ∪ C)"
by blast

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

(*Union is an AC-operator*)
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute

lemma Un_absorb1: "A ⊆ B ==> A ∪ B = B"
  by blast

lemma Un_absorb2: "B ⊆ A ==> A ∪ B = A"
  by blast

lemma Un_Int_distrib: "(A ∩ B) ∪ C = (A ∪ C) ∩ (B ∪ C)"
by blast

lemma 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 blast

lemma Un_eq_Union: "A ∪ B = ∪({A, B})"
by blast

subsection‹Set Difference›

lemma Diff_subset: "A-B ⊆ A"
by blast

lemma Diff_contains: "[C⊆A; C ∩ B = 0] ==> C ⊆ A-B"
by blast

lemma subset_Diff_cons_iff: "B ⊆ A - cons(c,C) ⟷ B⊆A-C ∧ c ∉ B"
by blast

lemma Diff_cancel: "A - A = 0"
by blast

lemma Diff_triv: "A ∩ B = 0 ==> A - B = A"
by blast

lemma empty_Diff [simp]: "0 - A = 0"
by blast

lemma Diff_0 [simp]: "A - 0 = A"
by blast

lemma Diff_eq_0_iff: "A - B = 0 ⟷ A ⊆ B"
by (blast elim: equalityE)

(*NOT SUITABLE FOR REWRITING since {a} \<equiv> cons(a,0)*)
lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
by blast

(*NOT SUITABLE FOR REWRITING since {a} \<equiv> cons(a,0)*)
lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
by blast

lemma Diff_disjoint: "A ∩ (B-A) = 0"
by blast

lemma Diff_partition: "A⊆B ==> A ∪ (B-A) = B"
by blast

lemma subset_Un_Diff: "A ⊆ B ∪ (A - B)"
by blast

lemma double_complement: "[A⊆B; B⊆C] ==> B-(C-A) = A"
by blast

lemma double_complement_Un: "(A ∪ B) - (B-A) = A"
by blast

lemma Un_Int_crazy:
 "(A ∩ B) ∪ (B ∩ C) ∪ (C ∩ A) = (A ∪ B) ∩ (B ∪ C) ∩ (C ∪ A)"
apply blast
done

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

(*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: "∪(A) ⊆ C ⟷ (∀x∈A. x ⊆ C)"
by blast

lemma Union_upper: "B∈A ==> B ⊆ ∪(A)"
by blast

lemma Union_least: "[∧x. x∈A ==> x⊆C] ==> ∪(A) ⊆ C"
by blast

lemma Union_cons [simp]: "∪(cons(a,B)) = a ∪ ∪(B)"
by blast

lemma Union_Un_distrib: "∪(A ∪ B) = ∪(A) ∪ ∪(B)"
by blast

lemma Union_Int_subset: "∪(A ∩ B) ⊆ ∪(A) ∩ ∪(B)"
by blast

lemma Union_disjoint: "∪(C) ∩ A = 0 ⟷ (∀B∈C. B ∩ A = 0)"
by (blast elim!: equalityE)

lemma Union_empty_iff: "∪(A) = 0 ⟷ (∀B∈A. B=0)"
by blast

lemma Int_Union2: "∪(B) ∩ A = (∪C∈B. C ∩ A)"
by blast

(** Big Intersection is the greatest lower bound of a nonempty set **)

lemma Inter_subset_iff: "A≠0 ==> C ⊆ ∩(A) ⟷ (∀x∈A. C ⊆ x)"
by blast

lemma Inter_lower: "B∈A ==> ∩(A) ⊆ B"
by blast

lemma Inter_greatest: "[A≠0; ∧x. x∈A ==> C⊆x] ==> C ⊆ ∩(A)"
by blast

(** Intersection of a family of sets  **)

lemma INT_lower: "x∈A ==> (∩x∈A. B(x)) ⊆ B(x)"
by blast

lemma INT_greatest: "[A≠0; ∧x. x∈A ==> C⊆B(x)] ==> C ⊆ (∩x∈A. B(x))"
by force

lemma Inter_0 [simp]: "∩(0) = 0"
by (unfold Inter_def, blast)

lemma Inter_Un_subset:
     "[z∈A; z∈B] ==> ∩(A) ∪ ∩(B) ⊆ ∩(A ∩ B)"
by blast

(* A good challenge: Inter is ill-behaved on the empty set *)
lemma Inter_Un_distrib:
     "[A≠0; B≠0] ==> ∩(A ∪ B) = ∩(A) ∩ ∩(B)"
by blast

lemma Union_singleton: "∪({b}) = b"
by blast

lemma Inter_singleton: "∩({b}) = b"
by blast

lemma Inter_cons [simp]:
     "∩(cons(a,B)) = (if B=0 then a else a ∩ ∩(B))"
by force

subsection‹Unions and Intersections of Families›

lemma subset_UN_iff_eq: "A ⊆ (∪i∈I. B(i)) ⟷ A = (∪i∈I. A ∩ B(i))"
by (blast elim!: equalityE)

lemma UN_subset_iff: "(∪x∈A. B(x)) ⊆ C ⟷ (∀x∈A. B(x) ⊆ C)"
by blast

lemma UN_upper: "x∈A ==> B(x) ⊆ (∪x∈A. B(x))"
by (erule RepFunI [THEN Union_upper])

lemma UN_least: "[∧x. x∈A ==> B(x)⊆C] ==> (∪x∈A. B(x)) ⊆ C"
by blast

lemma Union_eq_UN: "∪(A) = (∪x∈A. x)"
by blast

lemma Inter_eq_INT: "∩(A) = (∩x∈A. x)"
by (unfold Inter_def, blast)

lemma UN_0 [simp]: "(∪i∈0. A(i)) = 0"
by blast

lemma UN_singleton: "(∪x∈A. {x}) = A"
by blast

lemma UN_Un: "(∪i∈ A ∪ B. C(i)) = (∪i∈ A. C(i)) ∪ (∪i∈B. C(i))"
by blast

lemma INT_Un: "(∩i∈I ∪ J. A(i)) =
               (if I=0 then ∩j∈J. A(j)
                       else if J=0 then ∩i∈I. A(i)
                       else ((∩i∈I. A(i)) ∩ (∩j∈J. A(j))))"
by (simp, blast intro!: equalityI)

lemma UN_UN_flatten: "(∪x ∈ (∪y∈A. B(y)). C(x)) = (∪y∈A. ∪x∈ B(y). C(x))"
by blast

(*Halmos, Naive Set Theory, page 35.*)
lemma Int_UN_distrib: "B ∩ (∪i∈I. A(i)) = (∪i∈I. B ∩ A(i))"
by blast

lemma Un_INT_distrib: "I≠0 ==> B ∪ (∩i∈I. A(i)) = (∩i∈I. B ∪ A(i))"
by auto

lemma Int_UN_distrib2:
     "(∪i∈I. A(i)) ∩ (∪j∈J. B(j)) = (∪i∈I. ∪j∈J. A(i) ∩ B(j))"
by blast

lemma Un_INT_distrib2: "[I≠0; J≠0] ==>
      (∩i∈I. A(i)) ∪ (∩j∈J. B(j)) = (∩i∈I. ∩j∈J. A(i) ∪ B(j))"
by auto

lemma UN_constant [simp]: "(∪y∈A. c) = (if A=0 then 0 else c)"
by force

lemma INT_constant [simp]: "(∩y∈A. c) = (if A=0 then 0 else c)"
by force

lemma UN_RepFun [simp]: "(∪y∈ RepFun(A,f). B(y)) = (∪x∈A. B(f(x)))"
by blast

lemma INT_RepFun [simp]: "(∩x∈RepFun(A,f). B(x)) = (∩a∈A. B(f(a)))"
by (auto simp add: Inter_def)

lemma INT_Union_eq:
     "0 ∉ A ==> (∩x∈ ∪(A). B(x)) = (∩y∈A. ∩x∈y. B(x))"
apply (subgoal_tac "∀x∈A. x≠0")
   prefer 2 apply blast
apply (force simp add: Inter_def ball_conj_distrib)
done

lemma INT_UN_eq:
     "(∀x∈A. B(x) ≠ 0)
      ==> (∩z∈ (∪x∈A. B(x)). C(z)) = (∩x∈A. ∩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:
     "(∪i∈I. A(i) ∪ B(i)) = (∪i∈I. A(i)) ∪ (∪i∈I. B(i))"
by blast

lemma INT_Int_distrib:
     "I≠0 ==> (∩i∈I. A(i) ∩ B(i)) = (∩i∈I. A(i)) ∩ (∩i∈I. B(i))"
by (blast elim!: not_emptyE)

lemma UN_Int_subset:
     "(∪z∈I ∩ J. A(z)) ⊆ (∪z∈I. A(z)) ∩ (∪z∈J. A(z))"
by blast

(** Devlin, page 12, exercise 5: Complements **)

lemma Diff_UN: "I≠0 ==> B - (∪i∈I. A(i)) = (∩i∈I. B - A(i))"
by (blast elim!: not_emptyE)

lemma Diff_INT: "I≠0 ==> B - (∩i∈I. A(i)) = (∪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 blast

lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) ∪ Sigma(A,B)"
by blast

lemma Sigma_succ2: "A * succ(B) = A*{B} ∪ A*B"
by blast

lemma SUM_UN_distrib1:
     "(∑x ∈ (∪y∈A. C(y)). B(x)) = (∪y∈A. ∑x∈C(y). B(x))"
by blast

lemma SUM_UN_distrib2:
     "(∑i∈I. ∪j∈J. C(i,j)) = (∪j∈J. ∑i∈I. C(i,j))"
by blast

lemma SUM_Un_distrib1:
     "(∑i∈I ∪ J. C(i)) = (∑i∈I. C(i)) ∪ (∑j∈J. C(j))"
by blast

lemma 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 blast

lemma 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)) = (∪i∈I. {i} * A(i))"
by blast

lemma times_subset_iff:
     "(A'*B' ⊆ A*B) ⟷ (A' = 0 | B' = 0 | (A'⊆A) ∧ (B'⊆B))"
by blast

lemma 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 blast

lemma domain_of_prod: "b∈B ==> domain(A*B) = A"
by blast

lemma domain_0 [simp]: "domain(0) = 0"
by blast

lemma domain_cons [simp]: "domain(cons(⟨a,b⟩,r)) = cons(a, domain(r))"
by blast

lemma domain_Un_eq [simp]: "domain(A ∪ B) = domain(A) ∪ domain(B)"
by blast

lemma domain_Int_subset: "domain(A ∩ B) ⊆ domain(A) ∩ domain(B)"
by blast

lemma domain_Diff_subset: "domain(A) - domain(B) ⊆ domain(A - B)"
by blast

lemma domain_UN: "domain(∪x∈A. B(x)) = (∪x∈A. domain(B(x)))"
by blast

lemma domain_Union: "domain(∪(A)) = (∪x∈A. domain(x))"
by blast


(** Range **)

lemma rangeI [intro]: "⟨a,b⟩∈ r ==> b ∈ range(r)"
  unfolding range_def
apply (erule converseI [THEN domainI])
done

lemma rangeE [elim!]: "[b ∈ range(r); ∧x. ⟨x,b⟩∈ r ==> P] ==> P"
by (unfold range_def, blast)

lemma range_subset: "range(A*B) ⊆ B"
  unfolding range_def
apply (subst converse_prod)
apply (rule domain_subset)
done

lemma range_of_prod: "a∈A ==> range(A*B) = B"
by blast

lemma range_0 [simp]: "range(0) = 0"
by blast

lemma range_cons [simp]: "range(cons(⟨a,b⟩,r)) = cons(b, range(r))"
by blast

lemma range_Un_eq [simp]: "range(A ∪ B) = range(A) ∪ range(B)"
by blast

lemma range_Int_subset: "range(A ∩ B) ⊆ range(A) ∩ range(B)"
by blast

lemma range_Diff_subset: "range(A) - range(B) ⊆ range(A - B)"
by blast

lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
by blast

lemma 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)
done

lemma 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 blast

lemma domain_subset_field: "domain(r) ⊆ field(r)"
  unfolding field_def
apply (rule Un_upper1)
done

lemma range_subset_field: "range(r) ⊆ field(r)"
  unfolding field_def
apply (rule Un_upper2)
done

lemma domain_times_range: "r ⊆ Sigma(A,B) ==> r ⊆ domain(r)*range(r)"
by blast

lemma field_times_field: "r ⊆ Sigma(A,B) ==> r ⊆ field(r)*field(r)"
by blast

lemma 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 blast

lemma field_0 [simp]: "field(0) = 0"
by blast

lemma field_cons [simp]: "field(cons(⟨a,b⟩,r)) = cons(a, cons(b, field(r)))"
by blast

lemma field_Un_eq [simp]: "field(A ∪ B) = field(A) ∪ field(B)"
by blast

lemma field_Int_subset: "field(A ∩ B) ⊆ field(A) ∩ field(B)"
by blast

lemma field_Diff_subset: "field(A) - field(B) ⊆ field(A - B)"
by blast

lemma 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) ==>
                  ∪(S) ⊆ domain(∪(S)) * range(∪(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 blast

lemma domain_Diff_eq: "[⟨a,c⟩ ∈ r; c≠b] ==> domain(r-{⟨a,b⟩}) = domain(r)"
by blast

lemma range_Diff_eq: "[⟨c,b⟩ ∈ r; c≠a] ==> range(r-{⟨a,b⟩}) = range(r)"
by blast


subsection‹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 blast

lemma image_0 [simp]: "r``0 = 0"
by blast

lemma image_Un [simp]: "r``(A ∪ B) = (r``A) ∪ (r``B)"
by blast

lemma image_UN: "r `` (∪x∈A. B(x)) = (∪x∈A. r `` B(x))"
by blast

lemma Collect_image_eq:
     "{z ∈ Sigma(A,B). P(z)} `` C = (∪x ∈ A. {y ∈ B(x). x ∈ C ∧ P(⟨x,y⟩)})"
by blast

lemma image_Int_subset: "r``(A ∩ B) ⊆ (r``A) ∩ (r``B)"
by blast

lemma image_Int_square_subset: "(r ∩ A*A)``B ⊆ (r``B) ∩ A"
by blast

lemma 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 blast

lemma image_Un_left: "(r ∪ s)``A = (r``A) ∪ (s``A)"
by blast

lemma image_Int_subset_left: "(r ∩ s)``A ⊆ (r``A) ∩ (s``A)"
by blast


subsection‹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)
done

lemma vimage_subset: "r ⊆ A*B ==> r-``C ⊆ A"
  unfolding vimage_def
apply (erule converse_type [THEN image_subset])
done

lemma vimage_0 [simp]: "r-``0 = 0"
by blast

lemma vimage_Un [simp]: "r-``(A ∪ B) = (r-``A) ∪ (r-``B)"
by blast

lemma vimage_Int_subset: "r-``(A ∩ B) ⊆ (r-``A) ∩ (r-``B)"
by blast

(*NOT suitable for rewriting*)
lemma vimage_eq_UN: "f -``B = (∪y∈B. f-``{y})"
by blast

lemma 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 blast

lemma 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 blast

lemma vimage_Un_left: "(r ∪ s)-``A = (r-``A) ∪ (s-``A)"
by blast

lemma 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 blast

lemma converse_Int [simp]: "converse(A ∩ B) = converse(A) ∩ converse(B)"
by blast

lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
by blast

lemma converse_UN [simp]: "converse(∪x∈A. B(x)) = (∪x∈A. converse(B(x)))"
by blast

(*Unfolding Inter avoids using excluded middle on A=0*)
lemma converse_INT [simp]:
     "converse(∩x∈A. B(x)) = (∩x∈A. converse(B(x)))"
apply (unfold Inter_def, blast)
done


subsection‹Powerset Operator›

lemma Pow_0 [simp]: "Pow(0) = {0}"
by blast

lemma 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)
done

lemma Un_Pow_subset: "Pow(A) ∪ Pow(B) ⊆ Pow(A ∪ B)"
by blast

lemma UN_Pow_subset: "(∪x∈A. Pow(B(x))) ⊆ Pow(∪x∈A. B(x))"
by blast

lemma subset_Pow_Union: "A ⊆ Pow(∪(A))"
by blast

lemma Union_Pow_eq [simp]: "∪(Pow(A)) = A"
by blast

lemma Union_Pow_iff: "∪(A) ∈ Pow(B) ⟷ A ∈ Pow(Pow(B))"
by blast

lemma Pow_Int_eq [simp]: "Pow(A ∩ B) = Pow(A) ∩ Pow(B)"
by blast

lemma Pow_INT_eq: "A≠0 ==> Pow(∩x∈A. B(x)) = (∩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 blast

lemma RepFun_eq_0_iff [simp]: "{f(x).x∈A}=0 ⟷ A=0"
by blast

lemma RepFun_constant [simp]: "{c. x∈A} = (if A=0 then 0 else {c})"
by force


subsection‹Collect›

lemma Collect_subset: "Collect(A,P) ⊆ A"
by blast

lemma Collect_Un: "Collect(A ∪ B, P) = Collect(A,P) ∪ Collect(B,P)"
by blast

lemma Collect_Int: "Collect(A ∩ B, P) = Collect(A,P) ∩ Collect(B,P)"
by blast

lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
by blast

lemma 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 blast

lemma Collect_Collect_eq [simp]:
     "Collect(Collect(A,P), Q) = Collect(A, λx. P(x) ∧ Q(x))"
by blast

lemma Collect_Int_Collect_eq:
     "Collect(A,P) ∩ Collect(A,Q) = Collect(A, λx. P(x) ∧ Q(x))"
by blast

lemma Collect_Union_eq [simp]:
     "Collect(∪x∈A. B(x), P) = (∪x∈A. Collect(B(x), P))"
by blast

lemma Collect_Int_left: "{x∈A. P(x)} ∩ B = {x ∈ A ∩ B. P(x)}"
by blast

lemma Collect_Int_right: "A ∩ {x∈B. P(x)} = {x ∈ A ∩ B. P(x)}"
by blast

lemma Collect_disj_eq: "{x∈A. P(x) | Q(x)} = Collect(A, P) ∪ Collect(A, Q)"
by blast

lemma Collect_conj_eq: "{x∈A. P(x) ∧ Q(x)} = Collect(A, P) ∩ Collect(A, Q)"
by blast

lemmas 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_lower2

ML ‹
 val subset_cs =
  claset_of (🍋
  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 (🍋 delrules [@{thm equalityI}]);
 ›

end