# HG changeset patch
# User paulson
# Date 848586505 -3600
# Node ID ebf910e7ec8714c084dd596edd55e3a5a46c65b0
# Parent  f869dc8858413cf307b7a1dae969517353944606
Tidied up some proofs, ...

diff -r f869dc885841 -r ebf910e7ec87 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Thu Nov 21 15:19:09 1996 +0100
+++ b/src/HOL/Integ/Equiv.ML	Thu Nov 21 15:28:25 1996 +0100
@@ -1,9 +1,7 @@
 (*  Title:      Equiv.ML
     ID:         $Id$
-    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
-                Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994 Universita' di Firenze
-    Copyright   1993  University of Cambridge
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
 
 Equivalence relations in HOL Set Theory 
 *)
@@ -40,7 +38,7 @@
     "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
-by (safe_tac (!claset));
+by (Step_tac 1);
 by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3);
 by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE])));
 qed "comp_equivI";
@@ -50,7 +48,7 @@
 (*Lemma for the next result*)
 goalw Equiv.thy [equiv_def,trans_def,sym_def]
     "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
-by (safe_tac (!claset));
+by (Step_tac 1);
 by (rtac ImageI 1);
 by (Fast_tac 2);
 by (Fast_tac 1);
@@ -62,9 +60,8 @@
 by (Fast_tac 1);
 qed "equiv_class_eq";
 
-val prems = goalw Equiv.thy [equiv_def,refl_def]
-    "[| equiv A r;  a: A |] ==> a: r^^{a}";
-by (cut_facts_tac prems 1);
+goalw Equiv.thy [equiv_def,refl_def]
+    "!!A r. [| equiv A r;  a: A |] ==> a: r^^{a}";
 by (Fast_tac 1);
 qed "equiv_class_self";
 
@@ -74,9 +71,9 @@
 by (Fast_tac 1);
 qed "subset_equiv_class";
 
-val prems = goal Equiv.thy
-    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
-by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
+goal Equiv.thy
+    "!!A r. [| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
+by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
 qed "eq_equiv_class";
 
 (*thus r^^{a} = r^^{b} as well*)
@@ -92,7 +89,7 @@
 
 goal Equiv.thy
     "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
-by (safe_tac (!claset));
+by (Step_tac 1);
 by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
 by ((rtac eq_equiv_class 3) THEN 
     (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
@@ -104,7 +101,7 @@
 
 goal Equiv.thy
     "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
-by (safe_tac (!claset));
+by (Step_tac 1);
 by ((rtac eq_equiv_class 1) THEN 
     (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
 by ((rtac equiv_class_eq 1) THEN 
@@ -115,10 +112,8 @@
 
 (** Introduction/elimination rules -- needed? **)
 
-val prems = goalw Equiv.thy [quotient_def] "x:A ==> r^^{x}: A/r";
-by (rtac UN_I 1);
-by (resolve_tac prems 1);
-by (rtac singletonI 1);
+goalw Equiv.thy [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
+by (Fast_tac 1);
 qed "quotientI";
 
 val [major,minor] = goalw Equiv.thy [quotient_def]
@@ -156,50 +151,43 @@
 val UN_singleton = ballI RSN (2,UN_singleton_lemma);
 
 
-(** These proofs really require as local premises
+(** These proofs really require the local premises
      equiv A r;  congruent r b
 **)
 
 (*Conversion rule*)
-val prems as [equivA,bcong,_] = goal Equiv.thy
-    "[| equiv A r;  congruent r b;  a: A |] ==> (UN x:r^^{a}. b(x)) = b(a)";
-by (cut_facts_tac prems 1);
-by (rtac UN_singleton 1);
-by (rtac equiv_class_self 1);
-by (assume_tac 1);
-by (assume_tac 1);
+goal Equiv.thy "!!A r. [| equiv A r;  congruent r b;  a: A |] \
+\                      ==> (UN x:r^^{a}. b(x)) = b(a)";
+by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
 by (Fast_tac 1);
 qed "UN_equiv_class";
 
-(*Resolve th against the "local" premises*)
-val localize = RSLIST [equivA,bcong];
-
 (*type checking of  UN x:r``{a}. b(x) *)
-val _::_::prems = goalw Equiv.thy [quotient_def]
+val prems = goalw Equiv.thy [quotient_def]
     "[| equiv A r;  congruent r b;  X: A/r;     \
-\       !!x.  x : A ==> b(x) : B |]     \
+\       !!x.  x : A ==> b(x) : B |]             \
 \    ==> (UN x:X. b(x)) : B";
 by (cut_facts_tac prems 1);
-by (safe_tac (!claset));
-by (stac (localize UN_equiv_class) 1);
+by (Step_tac 1);
+by (stac UN_equiv_class 1);
 by (REPEAT (ares_tac prems 1));
 qed "UN_equiv_class_type";
 
 (*Sufficient conditions for injectiveness.  Could weaken premises!
   major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
 *)
-val _::_::prems = goalw Equiv.thy [quotient_def]
+val prems = goalw Equiv.thy [quotient_def]
     "[| equiv A r;   congruent r b;  \
-\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
+\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;        \
 \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
 \    ==> X=Y";
 by (cut_facts_tac prems 1);
-by (safe_tac ((!claset) delrules [equalityI]));
-by (rtac (equivA RS equiv_class_eq) 1);
+by (Step_tac 1);
+by (rtac equiv_class_eq 1);
 by (REPEAT (ares_tac prems 1));
 by (etac box_equals 1);
-by (REPEAT (ares_tac [localize UN_equiv_class] 1));
+by (REPEAT (ares_tac [UN_equiv_class] 1));
 qed "UN_equiv_class_inject";
 
 
@@ -211,24 +199,21 @@
 by (Fast_tac 1);
 qed "congruent2_implies_congruent";
 
-val equivA::prems = goalw Equiv.thy [congruent_def]
-    "[| equiv A r;  congruent2 r b;  a: A |] ==> \
+goalw Equiv.thy [congruent_def]
+    "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> \
 \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
-by (cut_facts_tac (equivA::prems) 1);
-by (safe_tac (!claset));
-by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
+by (Step_tac 1);
+by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
+by (asm_simp_tac (!simpset addsimps [UN_equiv_class,
                                      congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
 by (Fast_tac 1);
 qed "congruent2_implies_congruent_UN";
 
-val prems as equivA::_ = goal Equiv.thy
-    "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
+goal Equiv.thy
+    "!!A r. [| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
 \    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
-by (cut_facts_tac prems 1);
-by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
+by (asm_simp_tac (!simpset addsimps [UN_equiv_class,
                                      congruent2_implies_congruent,
                                      congruent2_implies_congruent_UN]) 1);
 qed "UN_equiv_class2";
@@ -240,7 +225,7 @@
 \       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
 \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
 by (cut_facts_tac prems 1);
-by (safe_tac (!claset));
+by (Step_tac 1);
 by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
                              congruent2_implies_congruent_UN,
                              congruent2_implies_congruent, quotientI]) 1));
@@ -255,7 +240,7 @@
 \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
 \    |] ==> congruent2 r b";
 by (cut_facts_tac prems 1);
-by (safe_tac (!claset));
+by (Step_tac 1);
 by (rtac trans 1);
 by (REPEAT (ares_tac prems 1
      ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
diff -r f869dc885841 -r ebf910e7ec87 src/HOL/Integ/Equiv.thy
--- a/src/HOL/Integ/Equiv.thy	Thu Nov 21 15:19:09 1996 +0100
+++ b/src/HOL/Integ/Equiv.thy	Thu Nov 21 15:28:25 1996 +0100
@@ -1,9 +1,7 @@
 (*  Title:      Equiv.thy
     ID:         $Id$
-    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
-                Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994 Universita' di Firenze
-    Copyright   1993  University of Cambridge
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
 
 Equivalence relations in Higher-Order Set Theory 
 *)
diff -r f869dc885841 -r ebf910e7ec87 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Thu Nov 21 15:19:09 1996 +0100
+++ b/src/HOL/Integ/Integ.ML	Thu Nov 21 15:28:25 1996 +0100
@@ -1,8 +1,6 @@
 (*  Title:      Integ.ML
     ID:         $Id$
-    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
-                Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994 Universita' di Firenze
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 The integers as equivalence classes over nat*nat.
diff -r f869dc885841 -r ebf910e7ec87 src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Thu Nov 21 15:19:09 1996 +0100
+++ b/src/HOL/Integ/Integ.thy	Thu Nov 21 15:28:25 1996 +0100
@@ -1,9 +1,7 @@
 (*  Title:      Integ.thy
     ID:         $Id$
-    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
-                Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994 Universita' di Firenze
-    Copyright   1993  University of Cambridge
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
 
 The integers as equivalence classes over nat*nat.
 *)