Theory equalities

(*  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: "AB  xA  xB"
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  AB. P(x))  (x  A. P(x))  (x  B. P(x))"
  by blast

lemma bex_Un: "(x  AB. P(x))  (x  A. P(x)) | (x  B. P(x))"
  by blast

lemma ball_UN: "(z  (xA. B(x)). P(z))  (xA. z  B(x). P(z))"
  by blast

lemma bex_UN: "(z  (xA. B(x)). P(z))  (xA. zB(x). P(z))"
  by blast

subsection‹Converse of a Relation›

lemma converse_iff [simp]: "a,b converse(r)  b,ar"
by (unfold converse_def, blast)

lemma converseI [intro!]: "a,br  b,aconverse(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,yr  P
      P"
by (unfold converse_def, blast)

lemma converse_converse: "rSigma(A,B)  converse(converse(r)) = r"
by blast

lemma converse_type: "rA*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 termcons

lemma cons_subsetI: "aC; BC  cons(a,B)  C"
by blast

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

lemma cons_subset_iff [iff]: "cons(a,B)C  aC  BC"
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: "A0  A=0"
by blast

lemma subset_cons_iff: "Ccons(a,B)  CB | (aC  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 aC 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: "aC  {a}  C"
by blast

lemma singleton_subsetD: "{a}  C    aC"
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: "ij;  ij  succ(i)j"
by (unfold succ_def, blast)

lemma succ_subsetE:
    "succ(i)  j;  ij;  ij  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: "CA;  CB  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: "AB  A  B = A"
by (blast elim!: equalityE)

lemma subset_Int_iff2: "AB  B  A = A"
by (blast elim!: equalityE)

lemma Int_Diff_eq: "CA  (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: "AC;  BC  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: "AB  A  B = B"
by (blast elim!: equalityE)

lemma subset_Un_iff2: "AB  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: "CA;  C  B = 0  C  A-B"
by blast

lemma subset_Diff_cons_iff: "B  A - cons(c,C)    BA-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} ≡ 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 blast

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

lemma Diff_partition: "AB  A  (B-A) = B"
by blast

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

lemma double_complement: "AB; BC  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)    CA"
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  (xA. x  C)"
by blast

lemma Union_upper: "BA  B  (A)"
by blast

lemma Union_least: "x. xA  xC  (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  (BC. B  A = 0)"
by (blast elim!: equalityE)

lemma Union_empty_iff: "(A) = 0  (BA. B=0)"
by blast

lemma Int_Union2: "(B)  A = (CB. C  A)"
by blast

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

lemma Inter_subset_iff: "A0    C  (A)  (xA. C  x)"
by blast

lemma Inter_lower: "BA  (A)  B"
by blast

lemma Inter_greatest: "A0;  x. xA  Cx  C  (A)"
by blast

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

lemma INT_lower: "xA  (xA. B(x))  B(x)"
by blast

lemma INT_greatest: "A0;  x. xA  CB(x)  C  (xA. B(x))"
by force

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

lemma Inter_Un_subset:
     "zA; zB  (A)  (B)  (A  B)"
by blast

(* A good challenge: Inter is ill-behaved on the empty set *)
lemma Inter_Un_distrib:
     "A0;  B0  (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  (iI. B(i))  A = (iI. A  B(i))"
by (blast elim!: equalityE)

lemma UN_subset_iff: "(xA. B(x))  C  (xA. B(x)  C)"
by blast

lemma UN_upper: "xA  B(x)  (xA. B(x))"
by (erule RepFunI [THEN Union_upper])

lemma UN_least: "x. xA  B(x)C  (xA. B(x))  C"
by blast

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

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

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

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

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

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

lemma UN_UN_flatten: "(x  (yA. B(y)). C(x)) = (yA. x B(y). C(x))"
by blast

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

lemma Un_INT_distrib: "I0  B  (iI. A(i)) = (iI. B  A(i))"
by auto

lemma Int_UN_distrib2:
     "(iI. A(i))  (jJ. B(j)) = (iI. jJ. A(i)  B(j))"
by blast

lemma Un_INT_distrib2: "I0;  J0 
      (iI. A(i))  (jJ. B(j)) = (iI. jJ. A(i)  B(j))"
by auto

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

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

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

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

lemma INT_Union_eq:
     "0  A  (x (A). B(x)) = (yA. xy. B(x))"
apply (subgoal_tac "xA. x0")
   prefer 2 apply blast
apply (force simp add: Inter_def ball_conj_distrib)
done

lemma INT_UN_eq:
     "(xA. B(x)  0)
       (z (xA. B(x)). C(z)) = (xA. 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:
     "(iI. A(i)  B(i)) = (iI. A(i))    (iI. B(i))"
by blast

lemma INT_Int_distrib:
     "I0  (iI. A(i)  B(i)) = (iI. A(i))  (iI. B(i))"
by (blast elim!: not_emptyE)

lemma UN_Int_subset:
     "(zI  J. A(z))  (zI. A(z))  (zJ. A(z))"
by blast

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

lemma Diff_UN: "I0  B - (iI. A(i)) = (iI. B - A(i))"
by (blast elim!: not_emptyE)

lemma Diff_INT: "I0  B - (iI. A(i)) = (iI. 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  (yA. C(y)). B(x)) = (yA. xC(y). B(x))"
by blast

lemma SUM_UN_distrib2:
     "(iI. jJ. C(i,j)) = (jJ. iI. C(i,j))"
by blast

lemma SUM_Un_distrib1:
     "(iI  J. C(i)) = (iI. C(i))  (jJ. C(j))"
by blast

lemma SUM_Un_distrib2:
     "(iI. A(i)  B(i)) = (iI. A(i))  (iI. 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:
     "(iI  J. C(i)) = (iI. C(i))  (jJ. C(j))"
by blast

lemma SUM_Int_distrib2:
     "(iI. A(i)  B(i)) = (iI. A(i))  (iI. 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: "(iI. A(i)) = (iI. {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: "bB  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(xA. B(x)) = (xA. domain(B(x)))"
by blast

lemma domain_Union: "domain((A)) = (xA. 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: "aA  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,ar  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: "(xS. 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; cb  domain(r-{a,b}) = domain(r)"
by blast

lemma range_Diff_eq: "c,b  r; ca  range(r-{a,b}) = range(r)"
by blast


subsection‹Image of a Set under a Function or Relation›

lemma image_iff: "b  r``A  (xA. x,br)"
by (unfold image_def, blast)

lemma image_singleton_iff: "b  r``{a}  a,br"
by (rule image_iff [THEN iff_trans], blast)

lemma imageI [intro]: "a,b r;  aA  b  r``A"
by (unfold image_def, blast)

lemma imageE [elim!]:
    "b: r``A;  x.x,b r;  xA  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 `` (xA. B(x)) = (xA. 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: "BA  (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  (yB. a,yr)"
by (unfold vimage_def image_def converse_def, blast)

lemma vimage_singleton_iff: "a  r-``{b}  a,br"
by (rule vimage_iff [THEN iff_trans], blast)

lemma vimageI [intro]: "a,b r;  bB  a  r-``B"
by (unfold vimage_def, blast)

lemma vimageE [elim!]:
    "a: r-``B;  x.a,x r;  xB  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 = (yB. 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: "BA  (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(xA. B(x)) = (xA. converse(B(x)))"
by blast

(*Unfolding Inter avoids using excluded middle on A=0*)
lemma converse_INT [simp]:
     "converse(xA. B(x)) = (xA. 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: "(xA. Pow(B(x)))  Pow(xA. 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: "A0  Pow(xA. B(x)) = (xA. Pow(B(x)))"
by (blast elim!: not_emptyE)


subsection‹RepFun›

lemma RepFun_subset: "x. xA  f(x)  B  {f(x). xA}  B"
by blast

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

lemma RepFun_constant [simp]: "{c. xA} = (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: "{xcons(a,B). P(x)} =
      (if P(a) then cons(a, {xB. P(x)}) else {xB. 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(xA. B(x), P) = (xA. Collect(B(x), P))"
by blast

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

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

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

lemma Collect_conj_eq: "{xA. 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 (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