--- a/src/ZF/equalities.thy Wed Jul 09 12:41:47 2003 +0200
+++ b/src/ZF/equalities.thy Thu Jul 10 17:14:41 2003 +0200
@@ -12,7 +12,7 @@
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"
+lemma in_mono: "A\<subseteq>B ==> x\<in>A --> x\<in>B"
by blast
lemma the_eq_0 [simp]: "(THE x. False) = 0"
@@ -38,25 +38,25 @@
subsection{*Converse of a Relation*}
-lemma converse_iff [simp]: "<a,b>: converse(r) <-> <b,a>:r"
+lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
by (unfold converse_def, blast)
-lemma converseI [intro!]: "<a,b>:r ==> <b,a>:converse(r)"
+lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
by (unfold converse_def, blast)
-lemma converseD: "<a,b> : converse(r) ==> <b,a> : r"
+lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r"
by (unfold converse_def, blast)
lemma converseE [elim!]:
- "[| yx : converse(r);
- !!x y. [| yx=<y,x>; <x,y>:r |] ==> P |]
+ "[| yx \<in> 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"
+lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r"
by blast
-lemma converse_type: "r<=A*B ==> converse(r)<=B*A"
+lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A"
by blast
lemma converse_prod [simp]: "converse(A*B) = B*A"
@@ -66,29 +66,29 @@
by blast
lemma converse_subset_iff:
- "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
+ "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
by blast
subsection{*Finite Set Constructions Using @{term cons}*}
-lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C"
+lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C"
by blast
-lemma subset_consI: "B <= cons(a,B)"
+lemma subset_consI: "B \<subseteq> cons(a,B)"
by blast
-lemma cons_subset_iff [iff]: "cons(a,B)<=C <-> a:C & B<=C"
+lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
by blast
(*A safe special case of subset elimination, adding no new variables
- [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
+ [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
-lemma subset_empty_iff: "A<=0 <-> A=0"
+lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
by blast
-lemma subset_cons_iff: "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
+lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
by blast
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
@@ -115,28 +115,28 @@
(** singletons **)
-lemma singleton_subsetI: "a:C ==> {a} <= C"
+lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C"
by blast
-lemma singleton_subsetD: "{a} <= C ==> a:C"
+lemma singleton_subsetD: "{a} \<subseteq> C ==> a\<in>C"
by blast
(** succ **)
-lemma subset_succI: "i <= succ(i)"
+lemma subset_succI: "i \<subseteq> succ(i)"
by blast
-(*But if j is an ordinal or is transitive, then i:j implies i<=j!
+(*But if j is an ordinal or is transitive, then i\<in>j implies i\<subseteq>j!
See ordinal/Ord_succ_subsetI*)
-lemma succ_subsetI: "[| i:j; i<=j |] ==> succ(i)<=j"
+lemma succ_subsetI: "[| i\<in>j; i\<subseteq>j |] ==> succ(i)\<subseteq>j"
by (unfold succ_def, blast)
lemma succ_subsetE:
- "[| succ(i) <= j; [| i:j; i<=j |] ==> P |] ==> P"
+ "[| succ(i) \<subseteq> j; [| i\<in>j; i\<subseteq>j |] ==> P |] ==> P"
by (unfold succ_def, blast)
-lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)"
+lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
by (unfold succ_def, blast)
@@ -144,19 +144,19 @@
(** Intersection is the greatest lower bound of two sets **)
-lemma Int_subset_iff: "C <= A Int B <-> C <= A & C <= B"
+lemma Int_subset_iff: "C \<subseteq> A Int B <-> C \<subseteq> A & C \<subseteq> B"
by blast
-lemma Int_lower1: "A Int B <= A"
+lemma Int_lower1: "A Int B \<subseteq> A"
by blast
-lemma Int_lower2: "A Int B <= B"
+lemma Int_lower2: "A Int B \<subseteq> B"
by blast
-lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B"
+lemma Int_greatest: "[| C\<subseteq>A; C\<subseteq>B |] ==> C \<subseteq> A Int B"
by blast
-lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)"
+lemma Int_cons: "cons(a,B) Int C \<subseteq> cons(a, B Int C)"
by blast
lemma Int_absorb [simp]: "A Int A = A"
@@ -189,21 +189,21 @@
lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)"
by blast
-lemma subset_Int_iff: "A<=B <-> A Int B = A"
+lemma subset_Int_iff: "A\<subseteq>B <-> A Int B = A"
by (blast elim!: equalityE)
-lemma subset_Int_iff2: "A<=B <-> B Int A = A"
+lemma subset_Int_iff2: "A\<subseteq>B <-> B Int A = A"
by (blast elim!: equalityE)
-lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
+lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) Int C = C-B"
by blast
lemma Int_cons_left:
- "cons(a,A) Int B = (if a : B then cons(a, A Int B) else A Int B)"
+ "cons(a,A) Int B = (if a \<in> B then cons(a, A Int B) else A Int B)"
by auto
lemma Int_cons_right:
- "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)"
+ "A Int cons(a, B) = (if a \<in> A then cons(a, A Int B) else A Int B)"
by auto
lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
@@ -213,16 +213,16 @@
(** Union is the least upper bound of two sets *)
-lemma Un_subset_iff: "A Un B <= C <-> A <= C & B <= C"
+lemma Un_subset_iff: "A Un B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
by blast
-lemma Un_upper1: "A <= A Un B"
+lemma Un_upper1: "A \<subseteq> A Un B"
by blast
-lemma Un_upper2: "B <= A Un B"
+lemma Un_upper2: "B \<subseteq> A Un B"
by blast
-lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C"
+lemma Un_least: "[| A\<subseteq>C; B\<subseteq>C |] ==> A Un B \<subseteq> C"
by blast
lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
@@ -255,10 +255,10 @@
lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)"
by blast
-lemma subset_Un_iff: "A<=B <-> A Un B = B"
+lemma subset_Un_iff: "A\<subseteq>B <-> A Un B = B"
by (blast elim!: equalityE)
-lemma subset_Un_iff2: "A<=B <-> B Un A = B"
+lemma subset_Un_iff2: "A\<subseteq>B <-> B Un A = B"
by (blast elim!: equalityE)
lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)"
@@ -269,13 +269,13 @@
subsection{*Set Difference*}
-lemma Diff_subset: "A-B <= A"
+lemma Diff_subset: "A-B \<subseteq> A"
by blast
-lemma Diff_contains: "[| C<=A; C Int B = 0 |] ==> C <= A-B"
+lemma Diff_contains: "[| C\<subseteq>A; C Int B = 0 |] ==> C \<subseteq> A-B"
by blast
-lemma subset_Diff_cons_iff: "B <= A - cons(c,C) <-> B<=A-C & c ~: B"
+lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C) <-> B\<subseteq>A-C & c ~: B"
by blast
lemma Diff_cancel: "A - A = 0"
@@ -290,7 +290,7 @@
lemma Diff_0 [simp]: "A - 0 = A"
by blast
-lemma Diff_eq_0_iff: "A - B = 0 <-> A <= B"
+lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
by (blast elim: equalityE)
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
@@ -304,13 +304,13 @@
lemma Diff_disjoint: "A Int (B-A) = 0"
by blast
-lemma Diff_partition: "A<=B ==> A Un (B-A) = B"
+lemma Diff_partition: "A\<subseteq>B ==> A Un (B-A) = B"
by blast
-lemma subset_Un_Diff: "A <= B Un (A - B)"
+lemma subset_Un_Diff: "A \<subseteq> B Un (A - B)"
by blast
-lemma double_complement: "[| A<=B; B<=C |] ==> B-(C-A) = A"
+lemma double_complement: "[| A\<subseteq>B; B\<subseteq>C |] ==> B-(C-A) = A"
by blast
lemma double_complement_Un: "(A Un B) - (B-A) = A"
@@ -340,7 +340,7 @@
by blast
(*Halmos, Naive Set Theory, page 16.*)
-lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C) <-> C<=A"
+lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C) <-> C\<subseteq>A"
by (blast elim!: equalityE)
@@ -348,13 +348,13 @@
(** Big Union is the least upper bound of a set **)
-lemma Union_subset_iff: "Union(A) <= C <-> (\<forall>x\<in>A. x <= C)"
+lemma Union_subset_iff: "Union(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
by blast
-lemma Union_upper: "B:A ==> B <= Union(A)"
+lemma Union_upper: "B\<in>A ==> B \<subseteq> Union(A)"
by blast
-lemma Union_least: "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
+lemma Union_least: "[| !!x. x\<in>A ==> x\<subseteq>C |] ==> Union(A) \<subseteq> C"
by blast
lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
@@ -363,7 +363,7 @@
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
by blast
-lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)"
+lemma Union_Int_subset: "Union(A Int B) \<subseteq> Union(A) Int Union(B)"
by blast
lemma Union_disjoint: "Union(C) Int A = 0 <-> (\<forall>B\<in>C. B Int A = 0)"
@@ -372,39 +372,38 @@
lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
by blast
-lemma Int_Union2: "Union(B) Int A = (UN C:B. C Int A)"
+lemma Int_Union2: "Union(B) Int A = (\<Union>C\<in>B. C Int A)"
by blast
(** Big Intersection is the greatest lower bound of a nonempty set **)
-lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (\<forall>x\<in>A. C <= x)"
+lemma Inter_subset_iff: "A\<noteq>0 ==> C \<subseteq> Inter(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
by blast
-lemma Inter_lower: "B:A ==> Inter(A) <= B"
+lemma Inter_lower: "B\<in>A ==> Inter(A) \<subseteq> B"
by blast
-lemma Inter_greatest: "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
+lemma Inter_greatest: "[| A\<noteq>0; !!x. x\<in>A ==> C\<subseteq>x |] ==> C \<subseteq> Inter(A)"
by blast
(** Intersection of a family of sets **)
-lemma INT_lower: "x:A ==> (\<Inter>x\<in>A. B(x)) <= B(x)"
+lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)"
by blast
-lemma INT_greatest:
- "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (\<Inter>x\<in>A. B(x))"
-by blast
+lemma INT_greatest: "[| A\<noteq>0; !!x. x\<in>A ==> C\<subseteq>B(x) |] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))"
+by force
-lemma Inter_0: "Inter(0) = 0"
+lemma Inter_0 [simp]: "Inter(0) = 0"
by (unfold Inter_def, blast)
lemma Inter_Un_subset:
- "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"
+ "[| z\<in>A; z\<in>B |] ==> Inter(A) Un Inter(B) \<subseteq> Inter(A Int B)"
by blast
(* A good challenge: Inter is ill-behaved on the empty set *)
lemma Inter_Un_distrib:
- "[| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"
+ "[| A\<noteq>0; B\<noteq>0 |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"
by blast
lemma Union_singleton: "Union({b}) = b"
@@ -419,16 +418,16 @@
subsection{*Unions and Intersections of Families*}
-lemma subset_UN_iff_eq: "A <= (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A Int B(i))"
+lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A Int B(i))"
by (blast elim!: equalityE)
-lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) <= C <-> (\<forall>x\<in>A. B(x) <= C)"
+lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
by blast
-lemma UN_upper: "x:A ==> B(x) <= (\<Union>x\<in>A. B(x))"
+lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
by (erule RepFunI [THEN Union_upper])
-lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (\<Union>x\<in>A. B(x)) <= C"
+lemma UN_least: "[| !!x. x\<in>A ==> B(x)\<subseteq>C |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C"
by blast
lemma Union_eq_UN: "Union(A) = (\<Union>x\<in>A. x)"
@@ -446,12 +445,11 @@
lemma UN_Un: "(\<Union>i\<in> A Un B. C(i)) = (\<Union>i\<in> A. C(i)) Un (\<Union>i\<in>B. C(i))"
by blast
-lemma INT_Un: "(\<Inter>i\<in>I Un 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)) Int (\<Inter>j\<in>J. A(j))))"
-apply simp
-apply (blast intro!: equalityI)
-done
+lemma INT_Un: "(\<Inter>i\<in>I Un 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)) Int (\<Inter>j\<in>J. A(j))))"
+by (simp, blast intro!: equalityI)
lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))"
by blast
@@ -460,22 +458,22 @@
lemma Int_UN_distrib: "B Int (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B Int A(i))"
by blast
-lemma Un_INT_distrib: "i:I ==> B Un (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B Un A(i))"
-by blast
+lemma Un_INT_distrib: "I\<noteq>0 ==> B Un (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B Un A(i))"
+by auto
lemma Int_UN_distrib2:
"(\<Union>i\<in>I. A(i)) Int (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) Int B(j))"
by blast
-lemma Un_INT_distrib2: "[| i:I; j:J |] ==>
+lemma Un_INT_distrib2: "[| I\<noteq>0; J\<noteq>0 |] ==>
(\<Inter>i\<in>I. A(i)) Un (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) Un B(j))"
-by blast
+by auto
-lemma UN_constant: "a: A ==> (\<Union>y\<in>A. c) = c"
-by blast
+lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)"
+by force
-lemma INT_constant: "a: A ==> (\<Inter>y\<in>A. c) = c"
-by blast
+lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)"
+by force
lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
by blast
@@ -506,20 +504,21 @@
by blast
lemma INT_Int_distrib:
- "i:I ==> (\<Inter>i\<in>I. A(i) Int B(i)) = (\<Inter>i\<in>I. A(i)) Int (\<Inter>i\<in>I. B(i))"
-by blast
+ "I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) Int B(i)) = (\<Inter>i\<in>I. A(i)) Int (\<Inter>i\<in>I. B(i))"
+by (blast elim!: not_emptyE)
lemma UN_Int_subset:
- "(\<Union>z\<in>I Int J. A(z)) <= (\<Union>z\<in>I. A(z)) Int (\<Union>z\<in>J. A(z))"
+ "(\<Union>z\<in>I Int J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) Int (\<Union>z\<in>J. A(z))"
by blast
(** Devlin, page 12, exercise 5: Complements **)
-lemma Diff_UN: "i:I ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
-by blast
+lemma Diff_UN: "I\<noteq>0 ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
+by (blast elim!: not_emptyE)
-lemma Diff_INT: "i:I ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
-by blast
+lemma Diff_INT: "I\<noteq>0 ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
+by (blast elim!: not_emptyE)
+
(** Unions and Intersections with General Sum **)
@@ -538,19 +537,19 @@
by blast
lemma SUM_UN_distrib1:
- "(SUM x:(\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. SUM x:C(y). B(x))"
+ "(\<Sigma>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma>x\<in>C(y). B(x))"
by blast
lemma SUM_UN_distrib2:
- "(SUM i:I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. SUM i:I. C(i,j))"
+ "(\<Sigma>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma>i\<in>I. C(i,j))"
by blast
lemma SUM_Un_distrib1:
- "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))"
+ "(\<Sigma>i\<in>I Un J. C(i)) = (\<Sigma>i\<in>I. C(i)) Un (\<Sigma>j\<in>J. C(j))"
by blast
lemma SUM_Un_distrib2:
- "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))"
+ "(\<Sigma>i\<in>I. A(i) Un B(i)) = (\<Sigma>i\<in>I. A(i)) Un (\<Sigma>i\<in>I. B(i))"
by blast
(*First-order version of the above, for rewriting*)
@@ -558,11 +557,11 @@
by (rule SUM_Un_distrib2)
lemma SUM_Int_distrib1:
- "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))"
+ "(\<Sigma>i\<in>I Int J. C(i)) = (\<Sigma>i\<in>I. C(i)) Int (\<Sigma>j\<in>J. C(j))"
by blast
lemma SUM_Int_distrib2:
- "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))"
+ "(\<Sigma>i\<in>I. A(i) Int B(i)) = (\<Sigma>i\<in>I. A(i)) Int (\<Sigma>i\<in>I. B(i))"
by blast
(*First-order version of the above, for rewriting*)
@@ -570,11 +569,11 @@
by (rule SUM_Int_distrib2)
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
-lemma SUM_eq_UN: "(SUM i:I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
+lemma SUM_eq_UN: "(\<Sigma>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
by blast
lemma times_subset_iff:
- "(A'*B' <= A*B) <-> (A' = 0 | B' = 0 | (A'<=A) & (B'<=B))"
+ "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
by blast
lemma Int_Sigma_eq:
@@ -583,20 +582,20 @@
(** Domain **)
-lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
+lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>\<in> r)"
by (unfold domain_def, blast)
-lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
+lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
by (unfold domain_def, blast)
lemma domainE [elim!]:
- "[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P"
+ "[| a \<in> domain(r); !!y. <a,y>\<in> r ==> P |] ==> P"
by (unfold domain_def, blast)
-lemma domain_subset: "domain(Sigma(A,B)) <= A"
+lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A"
by blast
-lemma domain_of_prod: "b:B ==> domain(A*B) = A"
+lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A"
by blast
lemma domain_0 [simp]: "domain(0) = 0"
@@ -608,10 +607,10 @@
lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)"
by blast
-lemma domain_Int_subset: "domain(A Int B) <= domain(A) Int domain(B)"
+lemma domain_Int_subset: "domain(A Int B) \<subseteq> domain(A) Int domain(B)"
by blast
-lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)"
+lemma domain_Diff_subset: "domain(A) - domain(B) \<subseteq> domain(A - B)"
by blast
lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
@@ -623,21 +622,21 @@
(** Range **)
-lemma rangeI [intro]: "<a,b>: r ==> b : range(r)"
+lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)"
apply (unfold range_def)
apply (erule converseI [THEN domainI])
done
-lemma rangeE [elim!]: "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P"
+lemma rangeE [elim!]: "[| b \<in> range(r); !!x. <x,b>\<in> r ==> P |] ==> P"
by (unfold range_def, blast)
-lemma range_subset: "range(A*B) <= B"
+lemma range_subset: "range(A*B) \<subseteq> B"
apply (unfold range_def)
apply (subst converse_prod)
apply (rule domain_subset)
done
-lemma range_of_prod: "a:A ==> range(A*B) = B"
+lemma range_of_prod: "a\<in>A ==> range(A*B) = B"
by blast
lemma range_0 [simp]: "range(0) = 0"
@@ -649,10 +648,10 @@
lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)"
by blast
-lemma range_Int_subset: "range(A Int B) <= range(A) Int range(B)"
+lemma range_Int_subset: "range(A Int B) \<subseteq> range(A) Int range(B)"
by blast
-lemma range_Diff_subset: "range(A) - range(B) <= range(A - B)"
+lemma range_Diff_subset: "range(A) - range(B) \<subseteq> range(A - B)"
by blast
lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
@@ -664,43 +663,43 @@
(** Field **)
-lemma fieldI1: "<a,b>: r ==> a : field(r)"
+lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)"
by (unfold field_def, blast)
-lemma fieldI2: "<a,b>: r ==> b : field(r)"
+lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)"
by (unfold field_def, blast)
lemma fieldCI [intro]:
- "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
+ "(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> 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"
+ "[| a \<in> 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 Un B"
+lemma field_subset: "field(A*B) \<subseteq> A Un B"
by blast
-lemma domain_subset_field: "domain(r) <= field(r)"
+lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
apply (unfold field_def)
apply (rule Un_upper1)
done
-lemma range_subset_field: "range(r) <= field(r)"
+lemma range_subset_field: "range(r) \<subseteq> field(r)"
apply (unfold field_def)
apply (rule Un_upper2)
done
-lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
+lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)"
by blast
-lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
+lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)"
by blast
-lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)"
+lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)"
by (simp add: relation_def, blast)
lemma field_of_prod: "field(A*A) = A"
@@ -715,47 +714,47 @@
lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)"
by blast
-lemma field_Int_subset: "field(A Int B) <= field(A) Int field(B)"
+lemma field_Int_subset: "field(A Int B) \<subseteq> field(A) Int field(B)"
by blast
-lemma field_Diff_subset: "field(A) - field(B) <= field(A - B)"
+lemma field_Diff_subset: "field(A) - field(B) \<subseteq> 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: "(\<forall>x\<in>S. EX A B. x <= A*B) ==>
- Union(S) <= domain(Union(S)) * range(Union(S))"
+lemma rel_Union: "(\<forall>x\<in>S. EX A B. x \<subseteq> 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 Un s) <= (A Un C) * (B Un D)"
+lemma rel_Un: "[| r \<subseteq> A*B; s \<subseteq> C*D |] ==> (r Un s) \<subseteq> (A Un C) * (B Un D)"
by blast
-lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
+lemma domain_Diff_eq: "[| <a,c> \<in> 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)"
+lemma range_Diff_eq: "[| <c,b> \<in> 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 <-> (\<exists>x\<in>A. <x,b>:r)"
+lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
by (unfold image_def, blast)
-lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
+lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
by (rule image_iff [THEN iff_trans], blast)
-lemma imageI [intro]: "[| <a,b>: r; a:A |] ==> b : r``A"
+lemma imageI [intro]: "[| <a,b>\<in> r; a\<in>A |] ==> b \<in> r``A"
by (unfold image_def, blast)
lemma imageE [elim!]:
- "[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P"
+ "[| b: r``A; !!x.[| <x,b>\<in> r; x\<in>A |] ==> P |] ==> P"
by (unfold image_def, blast)
-lemma image_subset: "r <= A*B ==> r``C <= B"
+lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B"
by blast
lemma image_0 [simp]: "r``0 = 0"
@@ -764,13 +763,13 @@
lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)"
by blast
-lemma image_Int_subset: "r``(A Int B) <= (r``A) Int (r``B)"
+lemma image_Int_subset: "r``(A Int B) \<subseteq> (r``A) Int (r``B)"
by blast
-lemma image_Int_square_subset: "(r Int A*A)``B <= (r``B) Int A"
+lemma image_Int_square_subset: "(r Int A*A)``B \<subseteq> (r``B) Int A"
by blast
-lemma image_Int_square: "B<=A ==> (r Int A*A)``B = (r``B) Int A"
+lemma image_Int_square: "B\<subseteq>A ==> (r Int A*A)``B = (r``B) Int A"
by blast
@@ -781,28 +780,28 @@
lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)"
by blast
-lemma image_Int_subset_left: "(r Int s)``A <= (r``A) Int (s``A)"
+lemma image_Int_subset_left: "(r Int s)``A \<subseteq> (r``A) Int (s``A)"
by blast
subsection{*Inverse Image of a Set under a Function or Relation*}
lemma vimage_iff:
- "a : r-``B <-> (\<exists>y\<in>B. <a,y>:r)"
+ "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
by (unfold vimage_def image_def converse_def, blast)
-lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
+lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
by (rule vimage_iff [THEN iff_trans], blast)
-lemma vimageI [intro]: "[| <a,b>: r; b:B |] ==> a : r-``B"
+lemma vimageI [intro]: "[| <a,b>\<in> r; b\<in>B |] ==> a \<in> r-``B"
by (unfold vimage_def, blast)
lemma vimageE [elim!]:
- "[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P"
+ "[| a: r-``B; !!x.[| <a,x>\<in> r; x\<in>B |] ==> P |] ==> P"
apply (unfold vimage_def, blast)
done
-lemma vimage_subset: "r <= A*B ==> r-``C <= A"
+lemma vimage_subset: "r \<subseteq> A*B ==> r-``C \<subseteq> A"
apply (unfold vimage_def)
apply (erule converse_type [THEN image_subset])
done
@@ -813,7 +812,7 @@
lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)"
by blast
-lemma vimage_Int_subset: "r-``(A Int B) <= (r-``A) Int (r-``B)"
+lemma vimage_Int_subset: "r-``(A Int B) \<subseteq> (r-``A) Int (r-``B)"
by blast
(*NOT suitable for rewriting*)
@@ -827,13 +826,13 @@
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"
+lemma function_image_vimage: "function(f) ==> f `` (f-`` A) \<subseteq> A"
by (unfold function_def, blast)
-lemma vimage_Int_square_subset: "(r Int A*A)-``B <= (r-``B) Int A"
+lemma vimage_Int_square_subset: "(r Int A*A)-``B \<subseteq> (r-``B) Int A"
by blast
-lemma vimage_Int_square: "B<=A ==> (r Int A*A)-``B = (r-``B) Int A"
+lemma vimage_Int_square: "B\<subseteq>A ==> (r Int A*A)-``B = (r-``B) Int A"
by blast
@@ -845,7 +844,7 @@
lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)"
by blast
-lemma vimage_Int_subset_left: "(r Int s)-``A <= (r-``A) Int (s-``A)"
+lemma vimage_Int_subset_left: "(r Int s)-``A \<subseteq> (r-``A) Int (s-``A)"
by blast
@@ -881,13 +880,13 @@
apply (rule_tac a = "x-{a}" in RepFun_eqI, auto)
done
-lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)"
+lemma Un_Pow_subset: "Pow(A) Un Pow(B) \<subseteq> Pow(A Un B)"
by blast
-lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) <= Pow(\<Union>x\<in>A. B(x))"
+lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))"
by blast
-lemma subset_Pow_Union: "A <= Pow(Union(A))"
+lemma subset_Pow_Union: "A \<subseteq> Pow(Union(A))"
by blast
lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
@@ -899,26 +898,25 @@
lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
by blast
-lemma Pow_INT_eq: "x:A ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
-by blast
+lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>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"
+lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
by blast
-lemma RepFun_eq_0_iff [simp]: "{f(x).x:A}=0 <-> A=0"
+lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
by blast
-lemma RepFun_constant [simp]: "{c. x:A} = (if A=0 then 0 else {c})"
-apply auto
-apply blast
-done
+lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
+by force
+
subsection{*Collect*}
-lemma Collect_subset: "Collect(A,P) <= A"
+lemma Collect_subset: "Collect(A,P) \<subseteq> A"
by blast
lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
@@ -930,8 +928,8 @@
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)})"
+lemma Collect_cons: "{x\<in>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 Int Collect(A,P) = Collect(A,P)"
@@ -949,16 +947,16 @@
"Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
by blast
-lemma Collect_Int_left: "{x:A. P(x)} Int B = {x : A Int B. P(x)}"
+lemma Collect_Int_left: "{x\<in>A. P(x)} Int B = {x \<in> A Int B. P(x)}"
by blast
-lemma Collect_Int_right: "A Int {x:B. P(x)} = {x : A Int B. P(x)}"
+lemma Collect_Int_right: "A Int {x\<in>B. P(x)} = {x \<in> A Int B. P(x)}"
by blast
-lemma Collect_disj_eq: "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
+lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
by blast
-lemma Collect_conj_eq: "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
+lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
by blast
lemmas subset_SIs = subset_refl cons_subsetI subset_consI