(* Title: ZF/equalities.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
section\<open>Basic Equalities and Inclusions\<close>
theory equalities imports pair begin
text\<open>These cover union, intersection, converse, domain, range, etc. Philippe
de Groote proved many of the inclusions.\<close>
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\<open>Bounded Quantifiers\<close>
text \<open>\medskip
The following are not added to the default simpset because
(a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
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\<open>Converse of a Relation\<close>
lemma converse_iff [simp]: "\ converse(r) \ \r"
by (unfold converse_def, blast)
lemma converseI [intro!]: "\r ==> \converse(r)"
by (unfold converse_def, blast)
lemma converseD: " \ converse(r) ==> \ r"
by (unfold converse_def, blast)
lemma converseE [elim!]:
"[| yx \ converse(r);
!!x y. [| yx=<y,x>; <x,y>\<in>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\<open>Finite Set Constructions Using \<^term>\<open>cons\<close>\<close>
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
[| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> 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\<open>Binary Intersection\<close>
(** 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\<open>Binary Union\<close>
(** 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\<open>Set Difference\<close>
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} == 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: "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\<open>Big Union and Intersection\<close>
(** 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\<open>Unions and Intersections of Families\<close>
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 \<Inter>j\<in>J. A(j)
else if J=0 then \<Inter>i\<in>I. A(i)
else ((\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>j\<in>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 |] ==>
(\<Inter>i\<in>I. A(i)) \<union> (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) \<union> 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)
==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> 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. \ r)"
by (unfold domain_def, blast)
lemma domainI [intro]: "\ r ==> a: domain(r)"
by (unfold domain_def, blast)
lemma domainE [elim!]:
"[| a \ domain(r); !!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(,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]: "\ r ==> b \ range(r)"
apply (unfold range_def)
apply (erule converseI [THEN domainI])
done
lemma rangeE [elim!]: "[| b \ range(r); !!x. \ 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)
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(,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: "\ r ==> a \ field(r)"
by (unfold field_def, blast)
lemma fieldI2: "\ r ==> b \ field(r)"
by (unfold field_def, blast)
lemma fieldCI [intro]:
"(~ \r ==> \ r) ==> a \ field(r)"
apply (unfold field_def, blast)
done
lemma fieldE [elim!]:
"[| a \ field(r);
!!x. <a,x>\<in> r ==> P;
!!x. <x,a>\<in> 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)"
apply (unfold field_def)
apply (rule Un_upper1)
done
lemma range_subset_field: "range(r) \ field(r)"
apply (unfold 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(,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) ==>
\<Union>(S) \<subseteq> 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 blast
lemma domain_Diff_eq: "[| \ r; c\b |] ==> domain(r-{}) = domain(r)"
by blast
lemma range_Diff_eq: "[| \ r; c\a |] ==> range(r-{}) = range(r)"
by blast
subsection\<open>Image of a Set under a Function or Relation\<close>
lemma image_iff: "b \ r``A \ (\x\A. \r)"
by (unfold image_def, blast)
lemma image_singleton_iff: "b \ r``{a} \ \r"
by (rule image_iff [THEN iff_trans], blast)
lemma imageI [intro]: "[| \ r; a\A |] ==> b \ r``A"
by (unfold image_def, blast)
lemma imageE [elim!]:
"[| b: r``A; !!x.[| \ 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()})"
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\<open>Inverse Image of a Set under a Function or Relation\<close>
lemma vimage_iff:
"a \ r-``B \ (\y\B. \r)"
by (unfold vimage_def image_def converse_def, blast)
lemma vimage_singleton_iff: "a \ r-``{b} \ \r"
by (rule vimage_iff [THEN iff_trans], blast)
lemma vimageI [intro]: "[| \ r; b\B |] ==> a \ r-``B"
by (unfold vimage_def, blast)
lemma vimageE [elim!]:
"[| a: r-``B; !!x.[| \ r; x\B |] ==> P |] ==> P"
apply (unfold vimage_def, blast)
done
lemma vimage_subset: "r \ A*B ==> r-``C \ A"
apply (unfold 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\<open>Powerset Operator\<close>
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\<open>RepFun\<close>
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\<open>Collect\<close>
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\<in>B. P(x)}) else {x\<in>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 \<open>
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}]);
\<close>
end
¤ Dauer der Verarbeitung: 0.29 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
