# HG changeset patch
# User lcp
# Date 785718064 -3600
# Node ID 2054fa3c8d76c6d237e7cf13a5c08cd9b0fa3e54
# Parent  9dcce140bdfce7b284a7e2b374ae6fe8998faf6d
tidied proofs, using fast_tac etc. as much as possible

diff -r 9dcce140bdfc -r 2054fa3c8d76 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Fri Nov 25 00:00:35 1994 +0100
+++ b/src/ZF/Fixedpt.ML	Fri Nov 25 00:01:04 1994 +0100
@@ -54,10 +54,10 @@
 (**** Proof of Knaster-Tarski Theorem for the lfp ****)
 
 (*lfp is contained in each pre-fixedpoint*)
-val prems = goalw Fixedpt.thy [lfp_def]
-    "[| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
-by (rtac (PowI RS CollectI RS Inter_lower) 1);
-by (REPEAT (resolve_tac prems 1));
+goalw Fixedpt.thy [lfp_def]
+    "!!A. [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
+by (fast_tac ZF_cs 1);
+(*or  by (rtac (PowI RS CollectI RS Inter_lower) 1); *)
 val lfp_lowerbound = result();
 
 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
diff -r 9dcce140bdfc -r 2054fa3c8d76 src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Fri Nov 25 00:00:35 1994 +0100
+++ b/src/ZF/QPair.ML	Fri Nov 25 00:01:04 1994 +0100
@@ -1,9 +1,9 @@
-(*  Title: 	ZF/qpair.ML
+(*  Title: 	ZF/QPair.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For qpair.thy.  
+For QPair.thy.  
 
 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
 structures in ZF.  Does not precisely follow Quine's construction.  Thanks
@@ -71,23 +71,26 @@
  (fn [major]=>
   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
 
+val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
+
+
 val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
 \    QSigma(A,B) = QSigma(A',B')"
  (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
 
 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
- (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
+ (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]);
 
 val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0"
- (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
+ (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]);
 
 
 (*** Eliminator - qsplit ***)
 
 val qsplit = prove_goalw QPair.thy [qsplit_def]
     "qsplit(%x y.c(x,y), <a;b>) = c(a,b)"
- (fn _ => [ (fast_tac (ZF_cs addIs [the_equality] addEs [QPair_inject]) 1) ]);
+ (fn _ => [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]);
 
 val qsplit_type = prove_goal QPair.thy
     "[|  p:QSigma(A,B);   \
@@ -99,8 +102,6 @@
     (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
 
 
-val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
-
 (*** qconverse ***)
 
 val qconverseI = prove_goalw QPair.thy [qconverse_def]
@@ -208,8 +209,9 @@
 val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
 
 val qsum_cs = 
-    qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
-             addSDs [QInl_inject,QInr_inject];
+    qpair_cs addSIs [PartI, QInlI, QInrI] 
+             addSEs [PartE, qsumE, QInl_neq_QInr, QInr_neq_QInl]
+             addSDs [QInl_inject, QInr_inject];
 
 goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
 by (fast_tac qsum_cs 1);
@@ -261,21 +263,17 @@
 (** Rules for the Part primitive **)
 
 goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
 val Part_QInl = result();
 
 goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
 val Part_QInr = result();
 
 goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
 val Part_QInr2 = result();
 
 goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (rtac equalityI 1);
-by (rtac Un_least 1);
-by (rtac Part_subset 1);
-by (rtac Part_subset 1);
-by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
 val Part_qsum_equality = result();
diff -r 9dcce140bdfc -r 2054fa3c8d76 src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Fri Nov 25 00:00:35 1994 +0100
+++ b/src/ZF/Sum.ML	Fri Nov 25 00:01:04 1994 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	ZF/sum
+(*  Title: 	ZF/Sum
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -8,6 +8,35 @@
 
 open Sum;
 
+(*** Rules for the Part primitive ***)
+
+goalw Sum.thy [Part_def]
+    "a : Part(A,h) <-> a:A & (EX y. a=h(y))";
+by (rtac separation 1);
+val Part_iff = result();
+
+goalw Sum.thy [Part_def]
+    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
+by (REPEAT (ares_tac [exI,CollectI] 1));
+val Part_eqI = result();
+
+val PartI = refl RSN (2,Part_eqI);
+
+val major::prems = goalw Sum.thy [Part_def]
+    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
+\    |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (etac exE 1);
+by (REPEAT (ares_tac prems 1));
+val PartE = result();
+
+goalw Sum.thy [Part_def] "Part(A,h) <= A";
+by (rtac Collect_subset 1);
+val Part_subset = result();
+
+
+(*** Rules for Disjoint Sums ***)
+
 val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
 
 goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
@@ -61,8 +90,9 @@
 val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE);
 val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE);
 
-val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
-                   addSDs [Inl_inject,Inr_inject];
+val sum_cs = ZF_cs addSIs [PartI, InlI, InrI] 
+                   addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl]
+                   addSDs [Inl_inject, Inr_inject];
 
 val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
 			     Inl_Inr_iff, Inr_Inl_iff];
@@ -125,37 +155,23 @@
 val expand_case = result();
 
 
-(** Rules for the Part primitive **)
-
-goalw Sum.thy [Part_def]
-    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
-by (REPEAT (ares_tac [exI,CollectI] 1));
-val Part_eqI = result();
-
-val PartI = refl RSN (2,Part_eqI);
-
-val major::prems = goalw Sum.thy [Part_def]
-    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
-\    |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (etac exE 1);
-by (REPEAT (ares_tac prems 1));
-val PartE = result();
-
-goalw Sum.thy [Part_def] "Part(A,h) <= A";
-by (rtac Collect_subset 1);
-val Part_subset = result();
-
 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
-by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1);
+by (fast_tac sum_cs 1);
 val Part_mono = result();
 
+goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
+by (fast_tac (sum_cs addSIs [equalityI]) 1);
+val Part_Collect = result();
+
+val Part_CollectE =
+    Part_Collect RS equalityD1 RS subsetD RS CollectE |> standard;
+
 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
-by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (sum_cs addIs [equalityI]) 1);
 val Part_Inl = result();
 
 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
-by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (sum_cs addIs [equalityI]) 1);
 val Part_Inr = result();
 
 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
@@ -163,17 +179,13 @@
 val PartD1 = result();
 
 goal Sum.thy "Part(A,%x.x) = A";
-by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (sum_cs addIs [equalityI]) 1);
 val Part_id = result();
 
 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
-by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (sum_cs addIs [equalityI]) 1);
 val Part_Inr2 = result();
 
 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
-by (rtac equalityI 1);
-by (rtac Un_least 1);
-by (rtac Part_subset 1);
-by (rtac Part_subset 1);
-by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1);
+by (fast_tac (sum_cs addIs [equalityI]) 1);
 val Part_sum_equality = result();
diff -r 9dcce140bdfc -r 2054fa3c8d76 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Fri Nov 25 00:00:35 1994 +0100
+++ b/src/ZF/mono.ML	Fri Nov 25 00:01:04 1994 +0100
@@ -82,7 +82,7 @@
 
 goal QPair.thy "!!A B C D. [| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
 \                          QSigma(A,B) <= QSigma(C,D)";
-by (fast_tac (ZF_cs addIs [QSigmaI] addSEs [QSigmaE]) 1);
+by (fast_tac qpair_cs 1);
 val QSigma_mono_lemma = result();
 val QSigma_mono = ballI RSN (2,QSigma_mono_lemma);
 
@@ -109,17 +109,15 @@
 by (fast_tac ZF_cs 1);
 val domain_mono = result();
 
-val [prem] = goal ZF.thy "r <= Sigma(A,B) ==> domain(r) <= A";
-by (rtac (domain_subset RS (prem RS domain_mono RS subset_trans)) 1);
-val domain_rel_subset = result();
+val domain_rel_subset = 
+	[domain_mono, domain_subset] MRS subset_trans |> standard;
 
 goal ZF.thy "!!r s. r<=s ==> range(r)<=range(s)";
 by (fast_tac ZF_cs 1);
 val range_mono = result();
 
-val [prem] = goal ZF.thy "r <= A*B ==> range(r) <= B";
-by (rtac (range_subset RS (prem RS range_mono RS subset_trans)) 1);
-val range_rel_subset = result();
+val range_rel_subset = 
+	[range_mono, range_subset] MRS subset_trans |> standard;
 
 goal ZF.thy "!!r s. r<=s ==> field(r)<=field(s)";
 by (fast_tac ZF_cs 1);
@@ -159,9 +157,7 @@
 (** Monotonicity of implications -- some could go to FOL **)
 
 goal ZF.thy "!!A B x. A<=B ==> x:A --> x:B";
-by (rtac impI 1);
-by (etac subsetD 1);
-by (assume_tac 1);
+by (fast_tac ZF_cs 1);
 val in_mono = result();
 
 goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";