Tidied up some proofs, ...
authorpaulson
Thu Nov 21 15:28:25 1996 +0100 (1996-11-21)
changeset 2215ebf910e7ec87
parent 2214 f869dc885841
child 2216 9b080867c7b1
Tidied up some proofs, ...
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Integ/Integ.ML
src/HOL/Integ/Integ.thy
     1.1 --- a/src/HOL/Integ/Equiv.ML	Thu Nov 21 15:19:09 1996 +0100
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Nov 21 15:28:25 1996 +0100
     1.3 @@ -1,9 +1,7 @@
     1.4  (*  Title:      Equiv.ML
     1.5      ID:         $Id$
     1.6 -    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
     1.7 -                Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 -    Copyright   1994 Universita' di Firenze
     1.9 -    Copyright   1993  University of Cambridge
    1.10 +    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
    1.11 +    Copyright   1996  University of Cambridge
    1.12  
    1.13  Equivalence relations in HOL Set Theory 
    1.14  *)
    1.15 @@ -40,7 +38,7 @@
    1.16      "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
    1.17  by (etac equalityE 1);
    1.18  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
    1.19 -by (safe_tac (!claset));
    1.20 +by (Step_tac 1);
    1.21  by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3);
    1.22  by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE])));
    1.23  qed "comp_equivI";
    1.24 @@ -50,7 +48,7 @@
    1.25  (*Lemma for the next result*)
    1.26  goalw Equiv.thy [equiv_def,trans_def,sym_def]
    1.27      "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
    1.28 -by (safe_tac (!claset));
    1.29 +by (Step_tac 1);
    1.30  by (rtac ImageI 1);
    1.31  by (Fast_tac 2);
    1.32  by (Fast_tac 1);
    1.33 @@ -62,9 +60,8 @@
    1.34  by (Fast_tac 1);
    1.35  qed "equiv_class_eq";
    1.36  
    1.37 -val prems = goalw Equiv.thy [equiv_def,refl_def]
    1.38 -    "[| equiv A r;  a: A |] ==> a: r^^{a}";
    1.39 -by (cut_facts_tac prems 1);
    1.40 +goalw Equiv.thy [equiv_def,refl_def]
    1.41 +    "!!A r. [| equiv A r;  a: A |] ==> a: r^^{a}";
    1.42  by (Fast_tac 1);
    1.43  qed "equiv_class_self";
    1.44  
    1.45 @@ -74,9 +71,9 @@
    1.46  by (Fast_tac 1);
    1.47  qed "subset_equiv_class";
    1.48  
    1.49 -val prems = goal Equiv.thy
    1.50 -    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
    1.51 -by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
    1.52 +goal Equiv.thy
    1.53 +    "!!A r. [| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
    1.54 +by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
    1.55  qed "eq_equiv_class";
    1.56  
    1.57  (*thus r^^{a} = r^^{b} as well*)
    1.58 @@ -92,7 +89,7 @@
    1.59  
    1.60  goal Equiv.thy
    1.61      "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
    1.62 -by (safe_tac (!claset));
    1.63 +by (Step_tac 1);
    1.64  by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
    1.65  by ((rtac eq_equiv_class 3) THEN 
    1.66      (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
    1.67 @@ -104,7 +101,7 @@
    1.68  
    1.69  goal Equiv.thy
    1.70      "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
    1.71 -by (safe_tac (!claset));
    1.72 +by (Step_tac 1);
    1.73  by ((rtac eq_equiv_class 1) THEN 
    1.74      (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
    1.75  by ((rtac equiv_class_eq 1) THEN 
    1.76 @@ -115,10 +112,8 @@
    1.77  
    1.78  (** Introduction/elimination rules -- needed? **)
    1.79  
    1.80 -val prems = goalw Equiv.thy [quotient_def] "x:A ==> r^^{x}: A/r";
    1.81 -by (rtac UN_I 1);
    1.82 -by (resolve_tac prems 1);
    1.83 -by (rtac singletonI 1);
    1.84 +goalw Equiv.thy [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
    1.85 +by (Fast_tac 1);
    1.86  qed "quotientI";
    1.87  
    1.88  val [major,minor] = goalw Equiv.thy [quotient_def]
    1.89 @@ -156,50 +151,43 @@
    1.90  val UN_singleton = ballI RSN (2,UN_singleton_lemma);
    1.91  
    1.92  
    1.93 -(** These proofs really require as local premises
    1.94 +(** These proofs really require the local premises
    1.95       equiv A r;  congruent r b
    1.96  **)
    1.97  
    1.98  (*Conversion rule*)
    1.99 -val prems as [equivA,bcong,_] = goal Equiv.thy
   1.100 -    "[| equiv A r;  congruent r b;  a: A |] ==> (UN x:r^^{a}. b(x)) = b(a)";
   1.101 -by (cut_facts_tac prems 1);
   1.102 -by (rtac UN_singleton 1);
   1.103 -by (rtac equiv_class_self 1);
   1.104 -by (assume_tac 1);
   1.105 -by (assume_tac 1);
   1.106 +goal Equiv.thy "!!A r. [| equiv A r;  congruent r b;  a: A |] \
   1.107 +\                      ==> (UN x:r^^{a}. b(x)) = b(a)";
   1.108 +by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
   1.109  by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
   1.110  by (Fast_tac 1);
   1.111  qed "UN_equiv_class";
   1.112  
   1.113 -(*Resolve th against the "local" premises*)
   1.114 -val localize = RSLIST [equivA,bcong];
   1.115 -
   1.116  (*type checking of  UN x:r``{a}. b(x) *)
   1.117 -val _::_::prems = goalw Equiv.thy [quotient_def]
   1.118 +val prems = goalw Equiv.thy [quotient_def]
   1.119      "[| equiv A r;  congruent r b;  X: A/r;     \
   1.120 -\       !!x.  x : A ==> b(x) : B |]     \
   1.121 +\       !!x.  x : A ==> b(x) : B |]             \
   1.122  \    ==> (UN x:X. b(x)) : B";
   1.123  by (cut_facts_tac prems 1);
   1.124 -by (safe_tac (!claset));
   1.125 -by (stac (localize UN_equiv_class) 1);
   1.126 +by (Step_tac 1);
   1.127 +by (stac UN_equiv_class 1);
   1.128  by (REPEAT (ares_tac prems 1));
   1.129  qed "UN_equiv_class_type";
   1.130  
   1.131  (*Sufficient conditions for injectiveness.  Could weaken premises!
   1.132    major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   1.133  *)
   1.134 -val _::_::prems = goalw Equiv.thy [quotient_def]
   1.135 +val prems = goalw Equiv.thy [quotient_def]
   1.136      "[| equiv A r;   congruent r b;  \
   1.137 -\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
   1.138 +\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;        \
   1.139  \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
   1.140  \    ==> X=Y";
   1.141  by (cut_facts_tac prems 1);
   1.142 -by (safe_tac ((!claset) delrules [equalityI]));
   1.143 -by (rtac (equivA RS equiv_class_eq) 1);
   1.144 +by (Step_tac 1);
   1.145 +by (rtac equiv_class_eq 1);
   1.146  by (REPEAT (ares_tac prems 1));
   1.147  by (etac box_equals 1);
   1.148 -by (REPEAT (ares_tac [localize UN_equiv_class] 1));
   1.149 +by (REPEAT (ares_tac [UN_equiv_class] 1));
   1.150  qed "UN_equiv_class_inject";
   1.151  
   1.152  
   1.153 @@ -211,24 +199,21 @@
   1.154  by (Fast_tac 1);
   1.155  qed "congruent2_implies_congruent";
   1.156  
   1.157 -val equivA::prems = goalw Equiv.thy [congruent_def]
   1.158 -    "[| equiv A r;  congruent2 r b;  a: A |] ==> \
   1.159 +goalw Equiv.thy [congruent_def]
   1.160 +    "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> \
   1.161  \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
   1.162 -by (cut_facts_tac (equivA::prems) 1);
   1.163 -by (safe_tac (!claset));
   1.164 -by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   1.165 -by (assume_tac 1);
   1.166 -by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
   1.167 +by (Step_tac 1);
   1.168 +by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
   1.169 +by (asm_simp_tac (!simpset addsimps [UN_equiv_class,
   1.170                                       congruent2_implies_congruent]) 1);
   1.171  by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
   1.172  by (Fast_tac 1);
   1.173  qed "congruent2_implies_congruent_UN";
   1.174  
   1.175 -val prems as equivA::_ = goal Equiv.thy
   1.176 -    "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
   1.177 +goal Equiv.thy
   1.178 +    "!!A r. [| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
   1.179  \    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
   1.180 -by (cut_facts_tac prems 1);
   1.181 -by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
   1.182 +by (asm_simp_tac (!simpset addsimps [UN_equiv_class,
   1.183                                       congruent2_implies_congruent,
   1.184                                       congruent2_implies_congruent_UN]) 1);
   1.185  qed "UN_equiv_class2";
   1.186 @@ -240,7 +225,7 @@
   1.187  \       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
   1.188  \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
   1.189  by (cut_facts_tac prems 1);
   1.190 -by (safe_tac (!claset));
   1.191 +by (Step_tac 1);
   1.192  by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
   1.193                               congruent2_implies_congruent_UN,
   1.194                               congruent2_implies_congruent, quotientI]) 1));
   1.195 @@ -255,7 +240,7 @@
   1.196  \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
   1.197  \    |] ==> congruent2 r b";
   1.198  by (cut_facts_tac prems 1);
   1.199 -by (safe_tac (!claset));
   1.200 +by (Step_tac 1);
   1.201  by (rtac trans 1);
   1.202  by (REPEAT (ares_tac prems 1
   1.203       ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
     2.1 --- a/src/HOL/Integ/Equiv.thy	Thu Nov 21 15:19:09 1996 +0100
     2.2 +++ b/src/HOL/Integ/Equiv.thy	Thu Nov 21 15:28:25 1996 +0100
     2.3 @@ -1,9 +1,7 @@
     2.4  (*  Title:      Equiv.thy
     2.5      ID:         $Id$
     2.6 -    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
     2.7 -                Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8 -    Copyright   1994 Universita' di Firenze
     2.9 -    Copyright   1993  University of Cambridge
    2.10 +    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
    2.11 +    Copyright   1996  University of Cambridge
    2.12  
    2.13  Equivalence relations in Higher-Order Set Theory 
    2.14  *)
     3.1 --- a/src/HOL/Integ/Integ.ML	Thu Nov 21 15:19:09 1996 +0100
     3.2 +++ b/src/HOL/Integ/Integ.ML	Thu Nov 21 15:28:25 1996 +0100
     3.3 @@ -1,8 +1,6 @@
     3.4  (*  Title:      Integ.ML
     3.5      ID:         $Id$
     3.6 -    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
     3.7 -                Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 -    Copyright   1994 Universita' di Firenze
     3.9 +    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
    3.10      Copyright   1993  University of Cambridge
    3.11  
    3.12  The integers as equivalence classes over nat*nat.
     4.1 --- a/src/HOL/Integ/Integ.thy	Thu Nov 21 15:19:09 1996 +0100
     4.2 +++ b/src/HOL/Integ/Integ.thy	Thu Nov 21 15:28:25 1996 +0100
     4.3 @@ -1,9 +1,7 @@
     4.4  (*  Title:      Integ.thy
     4.5      ID:         $Id$
     4.6 -    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
     4.7 -                Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8 -    Copyright   1994 Universita' di Firenze
     4.9 -    Copyright   1993  University of Cambridge
    4.10 +    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
    4.11 +    Copyright   1996  University of Cambridge
    4.12  
    4.13  The integers as equivalence classes over nat*nat.
    4.14  *)