author paulson Thu Nov 21 15:28:25 1996 +0100 (1996-11-21) changeset 2215 ebf910e7ec87 parent 2214 f869dc885841 child 2216 9b080867c7b1
Tidied up some proofs, ...
 src/HOL/Integ/Equiv.ML file | annotate | diff | revisions src/HOL/Integ/Equiv.thy file | annotate | diff | revisions src/HOL/Integ/Integ.ML file | annotate | diff | revisions src/HOL/Integ/Integ.thy file | annotate | diff | revisions
```     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.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  *)
```