--- a/src/ZF/equalities.thy Fri Jun 28 20:01:09 2002 +0200
+++ b/src/ZF/equalities.thy Sat Jun 29 21:33:06 2002 +0200
@@ -3,13 +3,14 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Converse, domain, range of a relation or function.
-And set theory equalities involving Union, Intersection, Inclusion, etc.
- (Thanks also to Philippe de Groote.)
+Basic equations (and inclusions) involving union, intersection,
+converse, domain, range, etc.
+
+Thanks also to Philippe de Groote.
*)
-theory equalities = pair + subset:
+theory equalities = pair:
(*FIXME: move to ZF.thy or even to FOL.thy??*)
lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
@@ -23,6 +24,33 @@
lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
by blast
+(** Monotonicity of implications -- some could go to FOL **)
+
+lemma in_mono: "A<=B ==> x:A --> x:B"
+by blast
+
+lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
+by fast (*or (IntPr.fast_tac 1)*)
+
+lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
+by fast (*or (IntPr.fast_tac 1)*)
+
+lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
+by fast (*or (IntPr.fast_tac 1)*)
+
+lemma imp_refl: "P-->P"
+by (rule impI, assumption)
+
+(*The quantifier monotonicity rules are also intuitionistically valid*)
+lemma ex_mono:
+ "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"
+by blast
+
+lemma all_mono:
+ "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"
+by blast
+
+
lemma the_eq_0 [simp]: "(THE x. False) = 0"
by (blast intro: the_0)
@@ -77,143 +105,27 @@
by blast
-(*** domain ***)
-
-lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
-by (unfold domain_def, blast)
+(** cons; Finite Sets **)
-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"
+lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C"
by blast
-(*** range ***)
-
-lemma rangeI [intro]: "<a,b>: r ==> b : range(r)"
-apply (unfold 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"
-apply (unfold range_def)
-apply (subst converse_prod)
-apply (rule domain_subset)
-done
-
-
-(*** 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 Un 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)"
+lemma subset_consI: "B <= cons(a,B)"
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)
-
-
-(*** Image of a set under a function/relation ***)
-
-lemma image_iff: "b : r``A <-> (EX 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"
-apply (unfold image_def, blast)
-done
-
-lemma image_subset: "r <= A*B ==> r``C <= B"
+lemma cons_subset_iff [iff]: "cons(a,B)<=C <-> a:C & B<=C"
by blast
-
-(*** Inverse image of a set under a function/relation ***)
-
-lemma vimage_iff:
- "a : r-``B <-> (EX y:B. <a,y>:r)"
-apply (unfold vimage_def image_def converse_def, blast)
-done
-
-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)
+(*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, standard]
-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"
-apply (unfold vimage_def)
-apply (erule converse_type [THEN image_subset])
-done
-
-
-(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==>
- Union(S) <= domain(Union(S)) * range(Union(S))"
+lemma subset_empty_iff: "A<=0 <-> A=0"
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)"
-by blast
-
-lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
+lemma subset_cons_iff: "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
by blast
-lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
-by blast
-
-
-
-(** Finite Sets **)
-
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
lemma cons_eq: "{a} Un B = cons(a,B)"
by blast
@@ -233,9 +145,50 @@
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
by blast
-(** Binary Intersection **)
+(** 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 i:j implies i<=j!
+ See ordinal/Ord_succ_subsetI*)
+lemma succ_subsetI: "[| i:j; i<=j |] ==> succ(i)<=j"
+by (unfold succ_def, blast)
-(*NOT an equality, but it seems to belong here...*)
+lemma succ_subsetE:
+ "[| succ(i) <= j; [| i:j; i<=j |] ==> P |] ==> P"
+apply (unfold succ_def, blast)
+done
+
+lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)"
+by (unfold succ_def, blast)
+
+
+(*** Binary Intersection ***)
+
+(** Intersection is the greatest lower bound of two sets **)
+
+lemma Int_subset_iff: "C <= A Int B <-> C <= A & C <= B"
+by blast
+
+lemma Int_lower1: "A Int B <= A"
+by blast
+
+lemma Int_lower2: "A Int B <= B"
+by blast
+
+lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B"
+by blast
+
lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)"
by blast
@@ -272,7 +225,21 @@
lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
by blast
-(** Binary Union **)
+(*** Binary Union ***)
+
+(** Union is the least upper bound of two sets *)
+
+lemma Un_subset_iff: "A Un B <= C <-> A <= C & B <= C"
+by blast
+
+lemma Un_upper1: "A <= A Un B"
+by blast
+
+lemma Un_upper2: "B <= A Un B"
+by blast
+
+lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C"
+by blast
lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
by blast
@@ -310,7 +277,16 @@
lemma Un_eq_Union: "A Un B = Union({A, B})"
by blast
-(** Simple properties of Diff -- set difference **)
+(*** Set difference ***)
+
+lemma Diff_subset: "A-B <= A"
+by blast
+
+lemma Diff_contains: "[| C<=A; C Int 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
@@ -378,7 +354,18 @@
by (blast elim!: equalityE)
-(** Big Union and Intersection **)
+(*** Big Union and Intersection ***)
+
+(** Big Union is the least upper bound of a set **)
+
+lemma Union_subset_iff: "Union(A) <= C <-> (ALL x:A. x <= C)"
+by blast
+
+lemma Union_upper: "B:A ==> B <= Union(A)"
+by blast
+
+lemma Union_least: "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
+by blast
lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
by blast
@@ -395,10 +382,31 @@
lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)"
by blast
+(** Big Intersection is the greatest lower bound of a nonempty set **)
+
+lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"
+by blast
+
+lemma Inter_lower: "B:A ==> Inter(A) <= B"
+by blast
+
+lemma Inter_greatest: "[| a:A; !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
+by blast
+
+(** Intersection of a family of sets **)
+
+lemma INT_lower: "x:A ==> (INT x:A. B(x)) <= B(x)"
+by blast
+
+lemma INT_greatest:
+ "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
+by blast
+
lemma Inter_0: "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)"
+lemma Inter_Un_subset:
+ "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"
by blast
(* A good challenge: Inter is ill-behaved on the empty set *)
@@ -416,7 +424,19 @@
"Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
by force
-(** Unions and Intersections of Families **)
+(*** Unions and Intersections of Families ***)
+
+lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"
+by (blast elim!: equalityE)
+
+lemma UN_subset_iff: "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
+by blast
+
+lemma UN_upper: "x:A ==> B(x) <= (UN x:A. B(x))"
+by (erule RepFunI [THEN Union_upper])
+
+lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
+by blast
lemma Union_eq_UN: "Union(A) = (UN x:A. x)"
by blast
@@ -436,7 +456,7 @@
lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j)
else if J=0 then INT i:I. A(i)
else ((INT i:I. A(i)) Int (INT j:J. A(j))))"
-apply auto
+apply simp
apply (blast intro!: equalityI)
done
@@ -562,6 +582,19 @@
(** Domain **)
+lemma domain_iff: "a: domain(r) <-> (EX 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
@@ -580,9 +613,6 @@
lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)"
by blast
-lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
-by blast
-
lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))"
by blast
@@ -592,6 +622,20 @@
(** Range **)
+lemma rangeI [intro]: "<a,b>: r ==> b : range(r)"
+apply (unfold 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"
+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
@@ -610,12 +654,54 @@
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 Un 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
@@ -637,8 +723,39 @@
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: "(ALL x:S. EX A B. x <= A*B) ==>
+ Union(S) <= domain(Union(S)) * range(Union(S))"
+by blast
-(** Image **)
+(** 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)"
+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
+
+
+(*** Image of a set under a function/relation ***)
+
+lemma image_iff: "b : r``A <-> (EX 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
@@ -667,7 +784,27 @@
by blast
-(** Inverse Image **)
+(*** Inverse image of a set under a function/relation ***)
+
+lemma vimage_iff:
+ "a : r-``B <-> (EX 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"
+apply (unfold vimage_def)
+apply (erule converse_type [THEN image_subset])
+done
lemma vimage_0 [simp]: "r-``0 = 0"
by blast
@@ -760,7 +897,10 @@
lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"
by blast
-(** RepFun **)
+(*** 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
@@ -770,7 +910,10 @@
apply blast
done
-(** Collect **)
+(*** Collect ***)
+
+lemma Collect_subset: "Collect(A,P) <= A"
+by blast
lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
by blast
@@ -800,10 +943,74 @@
"Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
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
+
+(*First, ML bindings from the old file subset.ML*)
+ML
+{*
+val cons_subsetI = thm "cons_subsetI";
+val subset_consI = thm "subset_consI";
+val cons_subset_iff = thm "cons_subset_iff";
+val cons_subsetE = thm "cons_subsetE";
+val subset_empty_iff = thm "subset_empty_iff";
+val subset_cons_iff = thm "subset_cons_iff";
+val subset_succI = thm "subset_succI";
+val succ_subsetI = thm "succ_subsetI";
+val succ_subsetE = thm "succ_subsetE";
+val succ_subset_iff = thm "succ_subset_iff";
+val singleton_subsetI = thm "singleton_subsetI";
+val singleton_subsetD = thm "singleton_subsetD";
+val Union_subset_iff = thm "Union_subset_iff";
+val Union_upper = thm "Union_upper";
+val Union_least = thm "Union_least";
+val subset_UN_iff_eq = thm "subset_UN_iff_eq";
+val UN_subset_iff = thm "UN_subset_iff";
+val UN_upper = thm "UN_upper";
+val UN_least = thm "UN_least";
+val Inter_subset_iff = thm "Inter_subset_iff";
+val Inter_lower = thm "Inter_lower";
+val Inter_greatest = thm "Inter_greatest";
+val INT_lower = thm "INT_lower";
+val INT_greatest = thm "INT_greatest";
+val Un_subset_iff = thm "Un_subset_iff";
+val Un_upper1 = thm "Un_upper1";
+val Un_upper2 = thm "Un_upper2";
+val Un_least = thm "Un_least";
+val Int_subset_iff = thm "Int_subset_iff";
+val Int_lower1 = thm "Int_lower1";
+val Int_lower2 = thm "Int_lower2";
+val Int_greatest = thm "Int_greatest";
+val Diff_subset = thm "Diff_subset";
+val Diff_contains = thm "Diff_contains";
+val subset_Diff_cons_iff = thm "subset_Diff_cons_iff";
+val Collect_subset = thm "Collect_subset";
+val RepFun_subset = thm "RepFun_subset";
+
+val subset_SIs = thms "subset_SIs";
+
+val subset_cs = claset()
+ delrules [subsetI, subsetCE]
+ addSIs subset_SIs
+ addIs [Union_upper, Inter_lower]
+ addSEs [cons_subsetE];
+*}
+(*subset_cs is a claset for subset reasoning*)
+
ML
{*
val ZF_cs = claset() delrules [equalityI];
+val in_mono = thm "in_mono";
+val conj_mono = thm "conj_mono";
+val disj_mono = thm "disj_mono";
+val imp_mono = thm "imp_mono";
+val imp_refl = thm "imp_refl";
+val ex_mono = thm "ex_mono";
+val all_mono = thm "all_mono";
+
val converse_iff = thm "converse_iff";
val converseI = thm "converseI";
val converseD = thm "converseD";