Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
1.1 --- a/src/ZF/Arith.ML Fri Sep 17 12:53:53 1993 +0200
1.2 +++ b/src/ZF/Arith.ML Fri Sep 17 16:16:38 1993 +0200
1.3 @@ -29,10 +29,9 @@
1.4
1.5 goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
1.6 val rec_ss = ZF_ss
1.7 - addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
1.8 - addrews [nat_case_succ, nat_succI];
1.9 + addsimps [nat_case_succ, nat_succI];
1.10 by (rtac rec_trans 1);
1.11 -by (SIMP_TAC rec_ss 1);
1.12 +by (simp_tac rec_ss 1);
1.13 val rec_succ = result();
1.14
1.15 val major::prems = goal Arith.thy
1.16 @@ -42,20 +41,12 @@
1.17 \ |] ==> rec(n,a,b) : C(n)";
1.18 by (rtac (major RS nat_induct) 1);
1.19 by (ALLGOALS
1.20 - (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
1.21 + (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
1.22 val rec_type = result();
1.23
1.24 -val prems = goalw Arith.thy [rec_def]
1.25 - "[| n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \
1.26 -\ |] ==> rec(n,a,b)=rec(n',a',b')";
1.27 -by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]
1.28 - addrews (prems RL [sym])) 1);
1.29 -val rec_cong = result();
1.30 -
1.31 val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
1.32
1.33 -val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
1.34 - addrews ([rec_0,rec_succ] @ nat_typechecks);
1.35 +val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
1.36
1.37
1.38 (** Addition **)
1.39 @@ -101,16 +92,16 @@
1.40 "n:nat ==> 0 #- n = 0"
1.41 (fn [prem]=>
1.42 [ (rtac (prem RS nat_induct) 1),
1.43 - (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
1.44 + (ALLGOALS (asm_simp_tac nat_ss)) ]);
1.45
1.46 (*Must simplify BEFORE the induction!! (Else we get a critical pair)
1.47 succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *)
1.48 val diff_succ_succ = prove_goalw Arith.thy [diff_def]
1.49 "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"
1.50 (fn prems=>
1.51 - [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
1.52 + [ (asm_simp_tac (nat_ss addsimps prems) 1),
1.53 (nat_ind_tac "n" prems 1),
1.54 - (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
1.55 + (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
1.56
1.57 val prems = goal Arith.thy
1.58 "[| m:nat; n:nat |] ==> m #- n : succ(m)";
1.59 @@ -119,8 +110,8 @@
1.60 by (resolve_tac prems 1);
1.61 by (etac succE 3);
1.62 by (ALLGOALS
1.63 - (ASM_SIMP_TAC
1.64 - (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
1.65 + (asm_simp_tac
1.66 + (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
1.67 val diff_leq = result();
1.68
1.69 (*** Simplification over add, mult, diff ***)
1.70 @@ -130,10 +121,7 @@
1.71 mult_0, mult_succ,
1.72 diff_0, diff_0_eq_0, diff_succ_succ];
1.73
1.74 -val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
1.75 -
1.76 -val arith_ss = nat_ss addcongs arith_congs
1.77 - addrews (arith_rews@arith_typechecks);
1.78 +val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
1.79
1.80 (*** Addition ***)
1.81
1.82 @@ -142,7 +130,7 @@
1.83 "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
1.84 (fn prems=>
1.85 [ (nat_ind_tac "m" prems 1),
1.86 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
1.87 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
1.88
1.89 (*The following two lemmas are used for add_commute and sometimes
1.90 elsewhere, since they are safe for rewriting.*)
1.91 @@ -150,13 +138,13 @@
1.92 "m:nat ==> m #+ 0 = m"
1.93 (fn prems=>
1.94 [ (nat_ind_tac "m" prems 1),
1.95 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
1.96 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
1.97
1.98 val add_succ_right = prove_goal Arith.thy
1.99 "m:nat ==> m #+ succ(n) = succ(m #+ n)"
1.100 (fn prems=>
1.101 [ (nat_ind_tac "m" prems 1),
1.102 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
1.103 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
1.104
1.105 (*Commutative law for addition*)
1.106 val add_commute = prove_goal Arith.thy
1.107 @@ -164,15 +152,15 @@
1.108 (fn prems=>
1.109 [ (nat_ind_tac "n" prems 1),
1.110 (ALLGOALS
1.111 - (ASM_SIMP_TAC
1.112 - (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
1.113 + (asm_simp_tac
1.114 + (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
1.115
1.116 (*Cancellation law on the left*)
1.117 val [knat,eqn] = goal Arith.thy
1.118 "[| k:nat; k #+ m = k #+ n |] ==> m=n";
1.119 by (rtac (eqn RS rev_mp) 1);
1.120 by (nat_ind_tac "k" [knat] 1);
1.121 -by (ALLGOALS (SIMP_TAC arith_ss));
1.122 +by (ALLGOALS (simp_tac arith_ss));
1.123 by (fast_tac ZF_cs 1);
1.124 val add_left_cancel = result();
1.125
1.126 @@ -183,39 +171,40 @@
1.127 "m:nat ==> m #* 0 = 0"
1.128 (fn prems=>
1.129 [ (nat_ind_tac "m" prems 1),
1.130 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
1.131 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
1.132
1.133 (*right successor law for multiplication*)
1.134 val mult_succ_right = prove_goal Arith.thy
1.135 - "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
1.136 - (fn prems=>
1.137 - [ (nat_ind_tac "m" prems 1),
1.138 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
1.139 + "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
1.140 + (fn _=>
1.141 + [ (nat_ind_tac "m" [] 1),
1.142 + (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
1.143 (*The final goal requires the commutative law for addition*)
1.144 - (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]);
1.145 + (rtac (add_commute RS subst_context) 1),
1.146 + (REPEAT (assume_tac 1)) ]);
1.147
1.148 (*Commutative law for multiplication*)
1.149 val mult_commute = prove_goal Arith.thy
1.150 "[| m:nat; n:nat |] ==> m #* n = n #* m"
1.151 (fn prems=>
1.152 [ (nat_ind_tac "m" prems 1),
1.153 - (ALLGOALS (ASM_SIMP_TAC
1.154 - (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
1.155 + (ALLGOALS (asm_simp_tac
1.156 + (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
1.157
1.158 (*addition distributes over multiplication*)
1.159 val add_mult_distrib = prove_goal Arith.thy
1.160 "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
1.161 (fn prems=>
1.162 [ (nat_ind_tac "m" prems 1),
1.163 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
1.164 + (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
1.165
1.166 (*Distributive law on the left; requires an extra typing premise*)
1.167 val add_mult_distrib_left = prove_goal Arith.thy
1.168 "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
1.169 (fn prems=>
1.170 let val mult_commute' = read_instantiate [("m","k")] mult_commute
1.171 - val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
1.172 - in [ (SIMP_TAC ss 1) ]
1.173 + val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
1.174 + in [ (simp_tac ss 1) ]
1.175 end);
1.176
1.177 (*Associative law for multiplication*)
1.178 @@ -223,7 +212,7 @@
1.179 "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
1.180 (fn prems=>
1.181 [ (nat_ind_tac "m" prems 1),
1.182 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
1.183 + (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
1.184
1.185
1.186 (*** Difference ***)
1.187 @@ -232,7 +221,7 @@
1.188 "m:nat ==> m #- m = 0"
1.189 (fn prems=>
1.190 [ (nat_ind_tac "m" prems 1),
1.191 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
1.192 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
1.193
1.194 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
1.195 val notless::prems = goal Arith.thy
1.196 @@ -241,8 +230,8 @@
1.197 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.198 by (resolve_tac prems 1);
1.199 by (resolve_tac prems 1);
1.200 -by (ALLGOALS (ASM_SIMP_TAC
1.201 - (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
1.202 +by (ALLGOALS (asm_simp_tac
1.203 + (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
1.204 naturals_are_ordinals]))));
1.205 val add_diff_inverse = result();
1.206
1.207 @@ -251,29 +240,24 @@
1.208 val [mnat,nnat] = goal Arith.thy
1.209 "[| m:nat; n:nat |] ==> (n#+m) #-n = m";
1.210 by (rtac (nnat RS nat_induct) 1);
1.211 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
1.212 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
1.213 val diff_add_inverse = result();
1.214
1.215 val [mnat,nnat] = goal Arith.thy
1.216 "[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
1.217 by (rtac (nnat RS nat_induct) 1);
1.218 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
1.219 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
1.220 val diff_add_0 = result();
1.221
1.222
1.223 (*** Remainder ***)
1.224
1.225 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
1.226 -val prems = goal Arith.thy
1.227 - "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
1.228 -by (cut_facts_tac prems 1);
1.229 +goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
1.230 by (etac rev_mp 1);
1.231 by (etac rev_mp 1);
1.232 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.233 -by (resolve_tac prems 1);
1.234 -by (resolve_tac prems 1);
1.235 -by (ALLGOALS (ASM_SIMP_TAC
1.236 - (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
1.237 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
1.238 val div_termination = result();
1.239
1.240 val div_rls =
1.241 @@ -286,17 +270,17 @@
1.242 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
1.243 val mod_type = result();
1.244
1.245 -val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
1.246 +val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
1.247
1.248 val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m";
1.249 by (rtac (mod_def RS def_transrec RS trans) 1);
1.250 -by (SIMP_TAC (div_ss addrews prems) 1);
1.251 +by (simp_tac (div_ss addsimps prems) 1);
1.252 val mod_less = result();
1.253
1.254 val prems = goal Arith.thy
1.255 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n";
1.256 by (rtac (mod_def RS def_transrec RS trans) 1);
1.257 -by (SIMP_TAC (div_ss addrews prems) 1);
1.258 +by (simp_tac (div_ss addsimps prems) 1);
1.259 val mod_geq = result();
1.260
1.261 (*** Quotient ***)
1.262 @@ -310,13 +294,13 @@
1.263 val prems = goal Arith.thy
1.264 "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0";
1.265 by (rtac (div_def RS def_transrec RS trans) 1);
1.266 -by (SIMP_TAC (div_ss addrews prems) 1);
1.267 +by (simp_tac (div_ss addsimps prems) 1);
1.268 val div_less = result();
1.269
1.270 val prems = goal Arith.thy
1.271 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)";
1.272 by (rtac (div_def RS def_transrec RS trans) 1);
1.273 -by (SIMP_TAC (div_ss addrews prems) 1);
1.274 +by (simp_tac (div_ss addsimps prems) 1);
1.275 val div_geq = result();
1.276
1.277 (*Main Result.*)
1.278 @@ -326,8 +310,8 @@
1.279 by (resolve_tac prems 1);
1.280 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
1.281 by (ALLGOALS
1.282 - (ASM_SIMP_TAC
1.283 - (arith_ss addrews ([mod_type,div_type] @ prems @
1.284 + (asm_simp_tac
1.285 + (arith_ss addsimps ([mod_type,div_type] @ prems @
1.286 [mod_less,mod_geq, div_less, div_geq,
1.287 add_assoc, add_diff_inverse, div_termination]))));
1.288 val mod_div_equality = result();
1.289 @@ -338,7 +322,7 @@
1.290 val [mnat,nnat] = goal Arith.thy
1.291 "[| m:nat; n:nat |] ==> ~ (m #+ n) : n";
1.292 by (rtac (mnat RS nat_induct) 1);
1.293 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
1.294 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
1.295 by (rtac notI 1);
1.296 by (etac notE 1);
1.297 by (etac (succI1 RS Ord_trans) 1);
2.1 --- a/src/ZF/Arith.thy Fri Sep 17 12:53:53 1993 +0200
2.2 +++ b/src/ZF/Arith.thy Fri Sep 17 16:16:38 1993 +0200
2.3 @@ -16,7 +16,7 @@
2.4 "#-" :: "[i,i]=>i" (infixl 65)
2.5
2.6 rules
2.7 - rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
2.8 + rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
2.9
2.10 add_def "m#+n == rec(m, n, %u v.succ(v))"
2.11 diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
3.1 --- a/src/ZF/Bool.ML Fri Sep 17 12:53:53 1993 +0200
3.2 +++ b/src/ZF/Bool.ML Fri Sep 17 16:16:38 1993 +0200
3.3 @@ -53,9 +53,6 @@
3.4 by (resolve_tac prems 1);
3.5 val cond_type = result();
3.6
3.7 -val [cond_cong] = mk_congs Bool.thy ["cond"];
3.8 -val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
3.9 -
3.10 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
3.11 by (rewtac rew);
3.12 by (rtac cond_1 1);
4.1 --- a/src/ZF/Epsilon.ML Fri Sep 17 12:53:53 1993 +0200
4.2 +++ b/src/ZF/Epsilon.ML Fri Sep 17 16:16:38 1993 +0200
4.3 @@ -64,8 +64,8 @@
4.4 "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \
4.5 \ nat_rec(n, A, %m r. Union(r)) <= X";
4.6 by (etac nat_induct 1);
4.7 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
4.8 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
4.9 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
4.10 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
4.11 by (fast_tac ZF_cs 1);
4.12 val eclose_least_lemma = result();
4.13
4.14 @@ -126,8 +126,8 @@
4.15 by (rtac (kmemj RS eclose_induct) 1);
4.16 by (rtac wfrec_ssubst 1);
4.17 by (rtac wfrec_ssubst 1);
4.18 -by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
4.19 - jmemi RSN (2,mem_eclose_sing_trans)]) 1);
4.20 +by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
4.21 + jmemi RSN (2,mem_eclose_sing_trans)]) 1);
4.22 val wfrec_eclose_eq = result();
4.23
4.24 val [prem] = goal Epsilon.thy
4.25 @@ -139,8 +139,8 @@
4.26 goalw Epsilon.thy [transrec_def]
4.27 "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
4.28 by (rtac wfrec_ssubst 1);
4.29 -by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
4.30 - arg_in_eclose_sing, under_Memrel_eclose]) 1);
4.31 +by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
4.32 + under_Memrel_eclose]) 1);
4.33 val transrec = result();
4.34
4.35 (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
4.36 @@ -173,23 +173,12 @@
4.37 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
4.38 val Ord_transrec_type = result();
4.39
4.40 -(*Congruence*)
4.41 -val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
4.42 - "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> transrec(a,H)=transrec(a',H')";
4.43 -val transrec_ss =
4.44 - ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
4.45 - addrews (prems RL [sym]);
4.46 -by (SIMP_TAC transrec_ss 1);
4.47 -val transrec_cong = result();
4.48 -
4.49 (*** Rank ***)
4.50
4.51 -val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
4.52 -
4.53 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
4.54 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
4.55 by (rtac (rank_def RS def_transrec RS ssubst) 1);
4.56 -by (SIMP_TAC ZF_ss 1);
4.57 +by (simp_tac ZF_ss 1);
4.58 val rank = result();
4.59
4.60 goal Epsilon.thy "Ord(rank(a))";
4.61 @@ -203,7 +192,7 @@
4.62 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
4.63 by (rtac (major RS trans_induct) 1);
4.64 by (rtac (rank RS ssubst) 1);
4.65 -by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
4.66 +by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
4.67 val rank_of_Ord = result();
4.68
4.69 val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
5.1 --- a/src/ZF/List.ML Fri Sep 17 12:53:53 1993 +0200
5.2 +++ b/src/ZF/List.ML Fri Sep 17 16:16:38 1993 +0200
5.3 @@ -62,7 +62,7 @@
5.4 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(<x,y>) \
5.5 \ |] ==> list_case(l,c,h) : C(l)";
5.6 by (rtac (major RS list_induct) 1);
5.7 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
5.8 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
5.9 ([list_case_0,list_case_Pair]@prems))));
5.10 val list_case_type = result();
5.11 ****)
5.12 @@ -71,10 +71,10 @@
5.13 (** For recursion **)
5.14
5.15 goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
5.16 -by (SIMP_TAC rank_ss 1);
5.17 +by (simp_tac rank_ss 1);
5.18 val rank_Cons1 = result();
5.19
5.20 goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
5.21 -by (SIMP_TAC rank_ss 1);
5.22 +by (simp_tac rank_ss 1);
5.23 val rank_Cons2 = result();
5.24
6.1 --- a/src/ZF/ListFn.ML Fri Sep 17 12:53:53 1993 +0200
6.2 +++ b/src/ZF/ListFn.ML Fri Sep 17 16:16:38 1993 +0200
6.3 @@ -11,19 +11,14 @@
6.4
6.5 (** list_rec -- by Vset recursion **)
6.6
6.7 -(*Used to verify list_rec*)
6.8 -val list_rec_ss = ZF_ss
6.9 - addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
6.10 - addrews List.case_eqns;
6.11 -
6.12 goal ListFn.thy "list_rec(Nil,c,h) = c";
6.13 by (rtac (list_rec_def RS def_Vrec RS trans) 1);
6.14 -by (SIMP_TAC list_rec_ss 1);
6.15 +by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
6.16 val list_rec_Nil = result();
6.17
6.18 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
6.19 by (rtac (list_rec_def RS def_Vrec RS trans) 1);
6.20 -by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
6.21 +by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
6.22 val list_rec_Cons = result();
6.23
6.24 (*Type checking -- proved by induction, as usual*)
6.25 @@ -33,8 +28,8 @@
6.26 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
6.27 \ |] ==> list_rec(l,c,h) : C(l)";
6.28 by (list_ind_tac "l" prems 1);
6.29 -by (ALLGOALS (ASM_SIMP_TAC
6.30 - (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
6.31 +by (ALLGOALS (asm_simp_tac
6.32 + (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
6.33 val list_rec_type = result();
6.34
6.35 (** Versions for use with definitions **)
6.36 @@ -122,47 +117,42 @@
6.37 map_type, map_type2, app_type, length_type, rev_type, flat_type,
6.38 list_add_type];
6.39
6.40 -val list_congs =
6.41 - List.congs @
6.42 - mk_congs ListFn.thy
6.43 - ["list_rec","map","op @","length","rev","flat","list_add"];
6.44 -
6.45 val list_ss = arith_ss
6.46 - addcongs list_congs
6.47 - addrews List.case_eqns
6.48 - addrews list_typechecks
6.49 - addrews [list_rec_Nil, list_rec_Cons,
6.50 + addsimps List.case_eqns
6.51 + addsimps [list_rec_Nil, list_rec_Cons,
6.52 map_Nil, map_Cons,
6.53 app_Nil, app_Cons,
6.54 length_Nil, length_Cons,
6.55 rev_Nil, rev_Cons,
6.56 flat_Nil, flat_Cons,
6.57 - list_add_Nil, list_add_Cons];
6.58 + list_add_Nil, list_add_Cons]
6.59 + setsolver (type_auto_tac list_typechecks);
6.60 +(*Could also rewrite using the list_typechecks...*)
6.61
6.62 (*** theorems about map ***)
6.63
6.64 val prems = goal ListFn.thy
6.65 "l: list(A) ==> map(%u.u, l) = l";
6.66 by (list_ind_tac "l" prems 1);
6.67 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.68 +by (ALLGOALS (asm_simp_tac list_ss));
6.69 val map_ident = result();
6.70
6.71 val prems = goal ListFn.thy
6.72 "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
6.73 by (list_ind_tac "l" prems 1);
6.74 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.75 +by (ALLGOALS (asm_simp_tac list_ss));
6.76 val map_compose = result();
6.77
6.78 val prems = goal ListFn.thy
6.79 "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
6.80 by (list_ind_tac "xs" prems 1);
6.81 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.82 +by (ALLGOALS (asm_simp_tac list_ss));
6.83 val map_app_distrib = result();
6.84
6.85 val prems = goal ListFn.thy
6.86 "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
6.87 by (list_ind_tac "ls" prems 1);
6.88 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
6.89 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
6.90 val map_flat = result();
6.91
6.92 val prems = goal ListFn.thy
6.93 @@ -170,9 +160,7 @@
6.94 \ list_rec(map(h,l), c, d) = \
6.95 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
6.96 by (list_ind_tac "l" prems 1);
6.97 -by (ALLGOALS
6.98 - (ASM_SIMP_TAC
6.99 - (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
6.100 +by (ALLGOALS (asm_simp_tac list_ss));
6.101 val list_rec_map = result();
6.102
6.103 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
6.104 @@ -183,7 +171,7 @@
6.105 val prems = goal ListFn.thy
6.106 "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
6.107 by (list_ind_tac "l" prems 1);
6.108 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.109 +by (ALLGOALS (asm_simp_tac list_ss));
6.110 val map_list_Collect = result();
6.111
6.112 (*** theorems about length ***)
6.113 @@ -191,13 +179,13 @@
6.114 val prems = goal ListFn.thy
6.115 "xs: list(A) ==> length(map(h,xs)) = length(xs)";
6.116 by (list_ind_tac "xs" prems 1);
6.117 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.118 +by (ALLGOALS (asm_simp_tac list_ss));
6.119 val length_map = result();
6.120
6.121 val prems = goal ListFn.thy
6.122 "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
6.123 by (list_ind_tac "xs" prems 1);
6.124 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.125 +by (ALLGOALS (asm_simp_tac list_ss));
6.126 val length_app = result();
6.127
6.128 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
6.129 @@ -207,60 +195,59 @@
6.130 val prems = goal ListFn.thy
6.131 "xs: list(A) ==> length(rev(xs)) = length(xs)";
6.132 by (list_ind_tac "xs" prems 1);
6.133 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
6.134 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
6.135 val length_rev = result();
6.136
6.137 val prems = goal ListFn.thy
6.138 "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
6.139 by (list_ind_tac "ls" prems 1);
6.140 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
6.141 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
6.142 val length_flat = result();
6.143
6.144 (*** theorems about app ***)
6.145
6.146 val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
6.147 by (rtac (major RS List.induct) 1);
6.148 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.149 +by (ALLGOALS (asm_simp_tac list_ss));
6.150 val app_right_Nil = result();
6.151
6.152 val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
6.153 by (list_ind_tac "xs" prems 1);
6.154 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
6.155 +by (ALLGOALS (asm_simp_tac list_ss));
6.156 val app_assoc = result();
6.157
6.158 val prems = goal ListFn.thy
6.159 "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
6.160 by (list_ind_tac "ls" prems 1);
6.161 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
6.162 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
6.163 val flat_app_distrib = result();
6.164
6.165 (*** theorems about rev ***)
6.166
6.167 val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
6.168 by (list_ind_tac "l" prems 1);
6.169 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
6.170 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
6.171 val rev_map_distrib = result();
6.172
6.173 (*Simplifier needs the premises as assumptions because rewriting will not
6.174 instantiate the variable ?A in the rules' typing conditions; note that
6.175 rev_type does not instantiate ?A. Only the premises do.
6.176 *)
6.177 -val prems = goal ListFn.thy
6.178 - "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
6.179 -by (cut_facts_tac prems 1);
6.180 +goal ListFn.thy
6.181 + "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
6.182 by (etac List.induct 1);
6.183 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
6.184 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
6.185 val rev_app_distrib = result();
6.186
6.187 val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
6.188 by (list_ind_tac "l" prems 1);
6.189 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
6.190 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
6.191 val rev_rev_ident = result();
6.192
6.193 val prems = goal ListFn.thy
6.194 "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
6.195 by (list_ind_tac "ls" prems 1);
6.196 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews
6.197 +by (ALLGOALS (asm_simp_tac (list_ss addsimps
6.198 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
6.199 val rev_flat = result();
6.200
6.201 @@ -273,22 +260,22 @@
6.202 by (cut_facts_tac prems 1);
6.203 by (list_ind_tac "xs" prems 1);
6.204 by (ALLGOALS
6.205 - (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
6.206 -by (resolve_tac arith_congs 1);
6.207 -by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
6.208 + (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
6.209 +by (rtac (add_commute RS subst_context) 1);
6.210 +by (REPEAT (ares_tac [refl, list_add_type] 1));
6.211 val list_add_app = result();
6.212
6.213 val prems = goal ListFn.thy
6.214 "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
6.215 by (list_ind_tac "l" prems 1);
6.216 by (ALLGOALS
6.217 - (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
6.218 + (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
6.219 val list_add_rev = result();
6.220
6.221 val prems = goal ListFn.thy
6.222 "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
6.223 by (list_ind_tac "ls" prems 1);
6.224 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
6.225 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
6.226 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
6.227 val list_add_flat = result();
6.228
6.229 @@ -301,6 +288,6 @@
6.230 \ |] ==> P(l)";
6.231 by (rtac (major RS rev_rev_ident RS subst) 1);
6.232 by (rtac (major RS rev_type RS List.induct) 1);
6.233 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
6.234 +by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
6.235 val list_append_induct = result();
6.236
7.1 --- a/src/ZF/Nat.ML Fri Sep 17 12:53:53 1993 +0200
7.2 +++ b/src/ZF/Nat.ML Fri Sep 17 16:16:38 1993 +0200
7.3 @@ -95,8 +95,8 @@
7.4 \ |] ==> m <= n --> P(m) --> P(n)";
7.5 by (nat_ind_tac "n" prems 1);
7.6 by (ALLGOALS
7.7 - (ASM_SIMP_TAC
7.8 - (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
7.9 + (asm_simp_tac
7.10 + (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
7.11 Ord_nat RS Ord_in_Ord]))));
7.12 val nat_induct_from_lemma = result();
7.13
7.14 @@ -127,17 +127,17 @@
7.15
7.16 (** nat_case **)
7.17
7.18 -goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
7.19 +goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
7.20 by (fast_tac (ZF_cs addIs [the_equality]) 1);
7.21 val nat_case_0 = result();
7.22
7.23 -goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
7.24 +goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
7.25 by (fast_tac (ZF_cs addIs [the_equality]) 1);
7.26 val nat_case_succ = result();
7.27
7.28 val major::prems = goal Nat.thy
7.29 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \
7.30 -\ |] ==> nat_case(n,a,b) : C(n)";
7.31 +\ |] ==> nat_case(a,b,n) : C(n)";
7.32 by (rtac (major RS nat_induct) 1);
7.33 by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
7.34 nat_case_succ RS ssubst] 1
7.35 @@ -145,13 +145,6 @@
7.36 by (assume_tac 1);
7.37 val nat_case_type = result();
7.38
7.39 -val prems = goalw Nat.thy [nat_case_def]
7.40 - "[| n=n'; a=a'; !!m z. b(m)=b'(m) \
7.41 -\ |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
7.42 -by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
7.43 - ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
7.44 -val nat_case_cong = result();
7.45 -
7.46
7.47 (** nat_rec -- used to define eclose and transrec, then obsolete **)
7.48
7.49 @@ -165,11 +158,10 @@
7.50 val [prem] = goal Nat.thy
7.51 "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
7.52 val nat_rec_ss = ZF_ss
7.53 - addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
7.54 - addrews [prem, nat_case_succ, nat_succI, Memrel_iff,
7.55 - vimage_singleton_iff];
7.56 + addsimps [prem, nat_case_succ, nat_succI, Memrel_iff,
7.57 + vimage_singleton_iff];
7.58 by (rtac nat_rec_trans 1);
7.59 -by (SIMP_TAC nat_rec_ss 1);
7.60 +by (simp_tac nat_rec_ss 1);
7.61 val nat_rec_succ = result();
7.62
7.63 (** The union of two natural numbers is a natural number -- their maximum **)
8.1 --- a/src/ZF/Nat.thy Fri Sep 17 12:53:53 1993 +0200
8.2 +++ b/src/ZF/Nat.thy Fri Sep 17 16:16:38 1993 +0200
8.3 @@ -9,7 +9,7 @@
8.4 Nat = Ord + Bool +
8.5 consts
8.6 nat :: "i"
8.7 - nat_case :: "[i, i, i=>i]=>i"
8.8 + nat_case :: "[i, i=>i, i]=>i"
8.9 nat_rec :: "[i, i, [i,i]=>i]=>i"
8.10
8.11 rules
8.12 @@ -17,10 +17,10 @@
8.13 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
8.14
8.15 nat_case_def
8.16 - "nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
8.17 + "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
8.18
8.19 nat_rec_def
8.20 "nat_rec(k,a,b) == \
8.21 -\ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"
8.22 +\ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
8.23
8.24 end
9.1 --- a/src/ZF/Ord.ML Fri Sep 17 12:53:53 1993 +0200
9.2 +++ b/src/ZF/Ord.ML Fri Sep 17 16:16:38 1993 +0200
9.3 @@ -318,7 +318,7 @@
9.4
9.5 goal Ord.thy
9.6 "!!i j. [| Ord(i); Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
9.7 -by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
9.8 +by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
9.9 by (fast_tac ZF_cs 1);
9.10 val subset_succ_iff = result();
9.11
9.12 @@ -356,17 +356,17 @@
9.13 goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k";
9.14 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
9.15 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
9.16 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
9.17 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
9.18 by (rtac (Un_commute RS ssubst) 1);
9.19 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
9.20 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
9.21 val Ord_member_UnI = result();
9.22
9.23 goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Int j : k";
9.24 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
9.25 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
9.26 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
9.27 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
9.28 by (rtac (Int_commute RS ssubst) 1);
9.29 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
9.30 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
9.31 val Ord_member_IntI = result();
9.32
9.33
10.1 --- a/src/ZF/Pair.ML Fri Sep 17 12:53:53 1993 +0200
10.2 +++ b/src/ZF/Pair.ML Fri Sep 17 16:16:38 1993 +0200
10.3 @@ -15,7 +15,7 @@
10.4
10.5 val Pair_iff = prove_goalw ZF.thy [Pair_def]
10.6 "<a,b> = <c,d> <-> a=c & b=d"
10.7 - (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
10.8 + (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
10.9 (fast_tac FOL_cs 1) ]);
10.10
10.11 val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
10.12 @@ -89,7 +89,7 @@
10.13 val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
10.14 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
10.15 \ Sigma(A,B) = Sigma(A',B')"
10.16 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
10.17 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
10.18
10.19 val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
10.20 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
10.21 @@ -114,13 +114,6 @@
10.22 (etac ssubst 1),
10.23 (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
10.24
10.25 -(*This congruence rule uses NO typing information...*)
10.26 -val split_cong = prove_goalw ZF.thy [split_def]
10.27 - "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
10.28 -\ split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
10.29 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
10.30 -
10.31 -
10.32 (*** conversions for fst and snd ***)
10.33
10.34 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
11.1 --- a/src/ZF/Perm.ML Fri Sep 17 12:53:53 1993 +0200
11.2 +++ b/src/ZF/Perm.ML Fri Sep 17 16:16:38 1993 +0200
11.3 @@ -52,6 +52,7 @@
11.4 (* f: bij(A,B) ==> f: A->B *)
11.5 val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
11.6
11.7 +
11.8 (** Identity function **)
11.9
11.10 val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";
11.11 @@ -76,7 +77,7 @@
11.12
11.13 goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
11.14 by (REPEAT (ares_tac [CollectI,lam_type] 1));
11.15 -by (SIMP_TAC ZF_ss 1);
11.16 +by (simp_tac ZF_ss 1);
11.17 val id_inj = result();
11.18
11.19 goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
11.20 @@ -262,7 +263,7 @@
11.21 "!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
11.22 by (safe_tac comp_cs);
11.23 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
11.24 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
11.25 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
11.26 val comp_mem_injD1 = result();
11.27
11.28 goalw Perm.thy [inj_def,surj_def]
11.29 @@ -271,9 +272,10 @@
11.30 by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
11.31 by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
11.32 by (REPEAT (assume_tac 1));
11.33 -by (safe_tac (comp_cs addSIs ZF_congs));
11.34 +by (safe_tac comp_cs);
11.35 +by (res_inst_tac [("t", "op `(g)")] subst_context 1);
11.36 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
11.37 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
11.38 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
11.39 val comp_mem_injD2 = result();
11.40
11.41 goalw Perm.thy [surj_def]
11.42 @@ -427,7 +429,9 @@
11.43 by (etac fun_extend 1);
11.44 by (REPEAT (ares_tac [ballI] 1));
11.45 by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
11.46 -(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
11.47 -by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
11.48 +(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
11.49 + using ZF_ss! But FOL_ss ignores the assumption...*)
11.50 +by (ALLGOALS (asm_simp_tac
11.51 + (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
11.52 by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
11.53 val inj_extend = result();
12.1 --- a/src/ZF/QPair.ML Fri Sep 17 12:53:53 1993 +0200
12.2 +++ b/src/ZF/QPair.ML Fri Sep 17 16:16:38 1993 +0200
12.3 @@ -74,7 +74,7 @@
12.4 val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
12.5 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
12.6 \ QSigma(A,B) = QSigma(A',B')"
12.7 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
12.8 + (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
12.9
12.10 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
12.11 (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
12.12 @@ -98,12 +98,6 @@
12.13 (etac ssubst 1),
12.14 (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
12.15
12.16 -(*This congruence rule uses NO typing information...*)
12.17 -val qsplit_cong = prove_goalw QPair.thy [qsplit_def]
12.18 - "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
12.19 -\ qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
12.20 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
12.21 -
12.22
12.23 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
12.24
12.25 @@ -243,7 +237,7 @@
12.26 val qsum_subset_iff = result();
12.27
12.28 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
12.29 -by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
12.30 +by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
12.31 by (fast_tac ZF_cs 1);
12.32 val qsum_equal_iff = result();
12.33
12.34 @@ -259,12 +253,6 @@
12.35 by (rtac cond_1 1);
12.36 val qcase_QInr = result();
12.37
12.38 -val prems = goalw QPair.thy [qcase_def]
12.39 - "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
12.40 -\ qcase(c,d,u)=qcase(c',d',u')";
12.41 -by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
12.42 -val qcase_cong = result();
12.43 -
12.44 val major::prems = goal QPair.thy
12.45 "[| u: A <+> B; \
12.46 \ !!x. x: A ==> c(x): C(QInl(x)); \
12.47 @@ -272,7 +260,7 @@
12.48 \ |] ==> qcase(c,d,u) : C(u)";
12.49 by (rtac (major RS qsumE) 1);
12.50 by (ALLGOALS (etac ssubst));
12.51 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
12.52 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
12.53 (prems@[qcase_QInl,qcase_QInr]))));
12.54 val qcase_type = result();
12.55
13.1 --- a/src/ZF/QUniv.ML Fri Sep 17 12:53:53 1993 +0200
13.2 +++ b/src/ZF/QUniv.ML Fri Sep 17 16:16:38 1993 +0200
13.3 @@ -205,7 +205,7 @@
13.4
13.5 goalw QUniv.thy [QPair_def,sum_def]
13.6 "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
13.7 -by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
13.8 +by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
13.9 val QPair_Int_quniv_eq = result();
13.10
13.11 (**** "Take-lemma" rules for proving c: quniv(A) ****)
14.1 --- a/src/ZF/ROOT.ML Fri Sep 17 12:53:53 1993 +0200
14.2 +++ b/src/ZF/ROOT.ML Fri Sep 17 16:16:38 1993 +0200
14.3 @@ -1,4 +1,5 @@
14.4 (* Title: ZF/ROOT
14.5 + ID: $Id$
14.6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
14.7 Copyright 1993 University of Cambridge
14.8
15.1 --- a/src/ZF/Sum.ML Fri Sep 17 12:53:53 1993 +0200
15.2 +++ b/src/ZF/Sum.ML Fri Sep 17 16:16:38 1993 +0200
15.3 @@ -83,7 +83,7 @@
15.4 val sum_subset_iff = result();
15.5
15.6 goal Sum.thy "A+B = C+D <-> A=C & B=D";
15.7 -by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
15.8 +by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
15.9 by (fast_tac ZF_cs 1);
15.10 val sum_equal_iff = result();
15.11
15.12 @@ -99,12 +99,6 @@
15.13 by (rtac cond_1 1);
15.14 val case_Inr = result();
15.15
15.16 -val prems = goalw Sum.thy [case_def]
15.17 - "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
15.18 -\ case(c,d,u)=case(c',d',u')";
15.19 -by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
15.20 -val case_cong = result();
15.21 -
15.22 val major::prems = goal Sum.thy
15.23 "[| u: A+B; \
15.24 \ !!x. x: A ==> c(x): C(Inl(x)); \
15.25 @@ -112,7 +106,7 @@
15.26 \ |] ==> case(c,d,u) : C(u)";
15.27 by (rtac (major RS sumE) 1);
15.28 by (ALLGOALS (etac ssubst));
15.29 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
15.30 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
15.31 (prems@[case_Inl,case_Inr]))));
15.32 val case_type = result();
15.33
16.1 --- a/src/ZF/Univ.ML Fri Sep 17 12:53:53 1993 +0200
16.2 +++ b/src/ZF/Univ.ML Fri Sep 17 16:16:38 1993 +0200
16.3 @@ -11,7 +11,7 @@
16.4 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
16.5 goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
16.6 by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
16.7 -by (SIMP_TAC ZF_ss 1);
16.8 +by (simp_tac ZF_ss 1);
16.9 val Vfrom = result();
16.10
16.11 (** Monotonicity **)
16.12 @@ -122,9 +122,8 @@
16.13
16.14 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
16.15 by (rtac (Vfrom RS trans) 1);
16.16 -brs ([refl] RL ZF_congs) 1;
16.17 -by (rtac equalityI 1);
16.18 -by (rtac (succI1 RS RepFunI RS Union_upper) 2);
16.19 +by (rtac (succI1 RS RepFunI RS Union_upper RSN
16.20 + (2, equalityI RS subst_context)) 1);
16.21 by (rtac UN_least 1);
16.22 by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
16.23 by (etac member_succD 1);
16.24 @@ -473,16 +472,16 @@
16.25 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
16.26
16.27 val rank_ss = ZF_ss
16.28 - addrews [split, case_Inl, case_Inr, Vset_rankI]
16.29 - addrews rank_trans_rls;
16.30 + addsimps [case_Inl, case_Inr, Vset_rankI]
16.31 + addsimps rank_trans_rls;
16.32
16.33 (** Recursion over Vset levels! **)
16.34
16.35 (*NOT SUITABLE FOR REWRITING: recursive!*)
16.36 goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
16.37 by (rtac (transrec RS ssubst) 1);
16.38 -by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta,
16.39 - VsetI RS beta]) 1);
16.40 +by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta,
16.41 + VsetI RS beta]) 1);
16.42 val Vrec = result();
16.43
16.44 (*This form avoids giant explosions in proofs. NOTE USE OF == *)
16.45 @@ -493,13 +492,6 @@
16.46 by (rtac Vrec 1);
16.47 val def_Vrec = result();
16.48
16.49 -val prems = goalw Univ.thy [Vrec_def]
16.50 - "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> Vrec(a,H)=Vrec(a',H')";
16.51 -val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
16.52 - addrews (prems RL [sym]);
16.53 -by (SIMP_TAC Vrec_ss 1);
16.54 -val Vrec_cong = result();
16.55 -
16.56
16.57 (*** univ(A) ***)
16.58
17.1 --- a/src/ZF/WF.ML Fri Sep 17 12:53:53 1993 +0200
17.2 +++ b/src/ZF/WF.ML Fri Sep 17 16:16:38 1993 +0200
17.3 @@ -19,10 +19,6 @@
17.4
17.5 open WF;
17.6
17.7 -val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
17.8 -
17.9 -val wf_ss = ZF_ss addcongs [H_cong];
17.10 -
17.11
17.12 (*** Well-founded relations ***)
17.13
17.14 @@ -138,13 +134,13 @@
17.15 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
17.16 spec RS mp instantiates induction hypotheses*)
17.17 fun indhyp_tac hyps =
17.18 - ares_tac (TrueI::hyps) ORELSE'
17.19 + resolve_tac (TrueI::refl::hyps) ORELSE'
17.20 (cut_facts_tac hyps THEN'
17.21 DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
17.22 eresolve_tac [underD, transD, spec RS mp]));
17.23
17.24 -(*** NOTE! some simplifications need a different auto_tac!! ***)
17.25 -val wf_super_ss = wf_ss setauto indhyp_tac;
17.26 +(*** NOTE! some simplifications need a different solver!! ***)
17.27 +val wf_super_ss = ZF_ss setsolver indhyp_tac;
17.28
17.29 val prems = goalw WF.thy [is_recfun_def]
17.30 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
17.31 @@ -153,7 +149,7 @@
17.32 by (wf_ind_tac "x" prems 1);
17.33 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
17.34 by (rewtac restrict_def);
17.35 -by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
17.36 +by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
17.37 val is_recfun_equal_lemma = result();
17.38 val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
17.39
17.40 @@ -165,7 +161,7 @@
17.41 by (rtac (consI1 RS restrict_type RS fun_extension) 1);
17.42 by (etac is_recfun_type 1);
17.43 by (ALLGOALS
17.44 - (ASM_SIMP_TAC (wf_super_ss addrews
17.45 + (asm_simp_tac (wf_super_ss addsimps
17.46 [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
17.47 val is_recfun_cut = result();
17.48
17.49 @@ -195,13 +191,13 @@
17.50 by (REPEAT (assume_tac 2));
17.51 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
17.52 (*Applying the substitution: must keep the quantified assumption!!*)
17.53 -by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
17.54 +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
17.55 by (fold_tac [is_recfun_def]);
17.56 -by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
17.57 +by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
17.58 by (rtac is_recfun_type 1);
17.59 by (ALLGOALS
17.60 - (ASM_SIMP_TAC
17.61 - (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
17.62 + (asm_simp_tac
17.63 + (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
17.64 val unfold_the_recfun = result();
17.65
17.66
17.67 @@ -214,13 +210,12 @@
17.68 val the_recfun_cut = result();
17.69
17.70 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
17.71 -val prems = goalw WF.thy [wftrec_def]
17.72 - "[| wf(r); trans(r) |] ==> \
17.73 -\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
17.74 +goalw WF.thy [wftrec_def]
17.75 + "!!r. [| wf(r); trans(r) |] ==> \
17.76 +\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
17.77 by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
17.78 -by (ALLGOALS (ASM_SIMP_TAC
17.79 - (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym,
17.80 - the_recfun_cut]))));
17.81 +by (ALLGOALS (asm_simp_tac
17.82 + (ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
17.83 val wftrec = result();
17.84
17.85 (** Removal of the premise trans(r) **)
17.86 @@ -230,8 +225,7 @@
17.87 "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
17.88 by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
17.89 by (rtac trans_trancl 1);
17.90 -by (rtac (refl RS H_cong) 1);
17.91 -by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
17.92 +by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
17.93 by (etac r_into_trancl 1);
17.94 by (rtac subset_refl 1);
17.95 val wfrec = result();
17.96 @@ -253,10 +247,3 @@
17.97 by (REPEAT (ares_tac (prems@[lam_type]) 1
17.98 ORELSE eresolve_tac [spec RS mp, underD] 1));
17.99 val wfrec_type = result();
17.100 -
17.101 -val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
17.102 - "[| r=r'; !!x u. H(x,u)=H'(x,u); a=a' |] \
17.103 -\ ==> wfrec(r,a,H)=wfrec(r',a',H')";
17.104 -by (EVERY1 (map rtac (prems RL [subst])));
17.105 -by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
17.106 -val wfrec_cong = result();
18.1 --- a/src/ZF/ZF.ML Fri Sep 17 12:53:53 1993 +0200
18.2 +++ b/src/ZF/ZF.ML Fri Sep 17 16:16:38 1993 +0200
18.3 @@ -13,9 +13,8 @@
18.4 val ballE : thm
18.5 val ballI : thm
18.6 val ball_cong : thm
18.7 - val ball_rew : thm
18.8 + val ball_simp : thm
18.9 val ball_tac : int -> tactic
18.10 - val basic_ZF_congs : thm list
18.11 val bexCI : thm
18.12 val bexE : thm
18.13 val bexI : thm
18.14 @@ -45,7 +44,6 @@
18.15 val lemmas_cs : claset
18.16 val PowD : thm
18.17 val PowI : thm
18.18 - val prove_cong_tac : thm list -> int -> tactic
18.19 val RepFunE : thm
18.20 val RepFunI : thm
18.21 val RepFun_eqI : thm
18.22 @@ -75,14 +73,6 @@
18.23 structure ZF_Lemmas : ZF_LEMMAS =
18.24 struct
18.25
18.26 -val basic_ZF_congs = mk_congs ZF.thy
18.27 - ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :",
18.28 - "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
18.29 - "domain", "range", "restrict"];
18.30 -
18.31 -fun prove_cong_tac prems i =
18.32 - REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
18.33 -
18.34 (*** Bounded universal quantifier ***)
18.35
18.36 val ballI = prove_goalw ZF.thy [Ball_def]
18.37 @@ -118,14 +108,13 @@
18.38 val ball_tac = dtac bspec THEN' assume_tac;
18.39
18.40 (*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
18.41 -val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
18.42 - (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
18.43 +val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
18.44 + (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
18.45
18.46 (*Congruence rule for rewriting*)
18.47 val ball_cong = prove_goalw ZF.thy [Ball_def]
18.48 - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
18.49 -\ |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
18.50 - (fn prems=> [ (prove_cong_tac prems 1) ]);
18.51 + "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
18.52 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
18.53
18.54 (*** Bounded existential quantifier ***)
18.55
18.56 @@ -151,8 +140,8 @@
18.57
18.58 val bex_cong = prove_goalw ZF.thy [Bex_def]
18.59 "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
18.60 -\ |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
18.61 - (fn prems=> [ (prove_cong_tac prems 1) ]);
18.62 +\ |] ==> Bex(A,P) <-> Bex(A',P')"
18.63 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
18.64
18.65 (*** Rules for subsets ***)
18.66
18.67 @@ -265,7 +254,7 @@
18.68
18.69 val Replace_cong = prove_goal ZF.thy
18.70 "[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
18.71 -\ {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
18.72 +\ Replace(A,P) = Replace(B,Q)"
18.73 (fn prems=>
18.74 let val substprems = prems RL [subst, ssubst]
18.75 and iffprems = prems RL [iffD1,iffD2]
18.76 @@ -275,7 +264,6 @@
18.77 ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
18.78 end);
18.79
18.80 -
18.81 (*** Rules for RepFun ***)
18.82
18.83 val RepFunI = prove_goalw ZF.thy [RepFun_def]
18.84 @@ -296,9 +284,8 @@
18.85 (REPEAT (ares_tac prems 1)) ]);
18.86
18.87 val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
18.88 - "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> \
18.89 -\ {f(x). x:A} = {g(x). x:B}"
18.90 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
18.91 + "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
18.92 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
18.93
18.94
18.95 (*** Rules for Collect -- forming a subset by separation ***)
18.96 @@ -332,9 +319,8 @@
18.97 (assume_tac 1) ]);
18.98
18.99 val Collect_cong = prove_goalw ZF.thy [Collect_def]
18.100 - "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> \
18.101 -\ {x:A. P(x)} = {x:B. Q(x)}"
18.102 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
18.103 + "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
18.104 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
18.105
18.106 (*** Rules for Unions ***)
18.107
19.1 --- a/src/ZF/arith.ML Fri Sep 17 12:53:53 1993 +0200
19.2 +++ b/src/ZF/arith.ML Fri Sep 17 16:16:38 1993 +0200
19.3 @@ -29,10 +29,9 @@
19.4
19.5 goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
19.6 val rec_ss = ZF_ss
19.7 - addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
19.8 - addrews [nat_case_succ, nat_succI];
19.9 + addsimps [nat_case_succ, nat_succI];
19.10 by (rtac rec_trans 1);
19.11 -by (SIMP_TAC rec_ss 1);
19.12 +by (simp_tac rec_ss 1);
19.13 val rec_succ = result();
19.14
19.15 val major::prems = goal Arith.thy
19.16 @@ -42,20 +41,12 @@
19.17 \ |] ==> rec(n,a,b) : C(n)";
19.18 by (rtac (major RS nat_induct) 1);
19.19 by (ALLGOALS
19.20 - (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
19.21 + (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
19.22 val rec_type = result();
19.23
19.24 -val prems = goalw Arith.thy [rec_def]
19.25 - "[| n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \
19.26 -\ |] ==> rec(n,a,b)=rec(n',a',b')";
19.27 -by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]
19.28 - addrews (prems RL [sym])) 1);
19.29 -val rec_cong = result();
19.30 -
19.31 val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
19.32
19.33 -val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
19.34 - addrews ([rec_0,rec_succ] @ nat_typechecks);
19.35 +val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
19.36
19.37
19.38 (** Addition **)
19.39 @@ -101,16 +92,16 @@
19.40 "n:nat ==> 0 #- n = 0"
19.41 (fn [prem]=>
19.42 [ (rtac (prem RS nat_induct) 1),
19.43 - (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
19.44 + (ALLGOALS (asm_simp_tac nat_ss)) ]);
19.45
19.46 (*Must simplify BEFORE the induction!! (Else we get a critical pair)
19.47 succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *)
19.48 val diff_succ_succ = prove_goalw Arith.thy [diff_def]
19.49 "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"
19.50 (fn prems=>
19.51 - [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
19.52 + [ (asm_simp_tac (nat_ss addsimps prems) 1),
19.53 (nat_ind_tac "n" prems 1),
19.54 - (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
19.55 + (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
19.56
19.57 val prems = goal Arith.thy
19.58 "[| m:nat; n:nat |] ==> m #- n : succ(m)";
19.59 @@ -119,8 +110,8 @@
19.60 by (resolve_tac prems 1);
19.61 by (etac succE 3);
19.62 by (ALLGOALS
19.63 - (ASM_SIMP_TAC
19.64 - (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
19.65 + (asm_simp_tac
19.66 + (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
19.67 val diff_leq = result();
19.68
19.69 (*** Simplification over add, mult, diff ***)
19.70 @@ -130,10 +121,7 @@
19.71 mult_0, mult_succ,
19.72 diff_0, diff_0_eq_0, diff_succ_succ];
19.73
19.74 -val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
19.75 -
19.76 -val arith_ss = nat_ss addcongs arith_congs
19.77 - addrews (arith_rews@arith_typechecks);
19.78 +val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
19.79
19.80 (*** Addition ***)
19.81
19.82 @@ -142,7 +130,7 @@
19.83 "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
19.84 (fn prems=>
19.85 [ (nat_ind_tac "m" prems 1),
19.86 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
19.87 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
19.88
19.89 (*The following two lemmas are used for add_commute and sometimes
19.90 elsewhere, since they are safe for rewriting.*)
19.91 @@ -150,13 +138,13 @@
19.92 "m:nat ==> m #+ 0 = m"
19.93 (fn prems=>
19.94 [ (nat_ind_tac "m" prems 1),
19.95 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
19.96 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
19.97
19.98 val add_succ_right = prove_goal Arith.thy
19.99 "m:nat ==> m #+ succ(n) = succ(m #+ n)"
19.100 (fn prems=>
19.101 [ (nat_ind_tac "m" prems 1),
19.102 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
19.103 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
19.104
19.105 (*Commutative law for addition*)
19.106 val add_commute = prove_goal Arith.thy
19.107 @@ -164,15 +152,15 @@
19.108 (fn prems=>
19.109 [ (nat_ind_tac "n" prems 1),
19.110 (ALLGOALS
19.111 - (ASM_SIMP_TAC
19.112 - (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
19.113 + (asm_simp_tac
19.114 + (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
19.115
19.116 (*Cancellation law on the left*)
19.117 val [knat,eqn] = goal Arith.thy
19.118 "[| k:nat; k #+ m = k #+ n |] ==> m=n";
19.119 by (rtac (eqn RS rev_mp) 1);
19.120 by (nat_ind_tac "k" [knat] 1);
19.121 -by (ALLGOALS (SIMP_TAC arith_ss));
19.122 +by (ALLGOALS (simp_tac arith_ss));
19.123 by (fast_tac ZF_cs 1);
19.124 val add_left_cancel = result();
19.125
19.126 @@ -183,39 +171,40 @@
19.127 "m:nat ==> m #* 0 = 0"
19.128 (fn prems=>
19.129 [ (nat_ind_tac "m" prems 1),
19.130 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
19.131 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
19.132
19.133 (*right successor law for multiplication*)
19.134 val mult_succ_right = prove_goal Arith.thy
19.135 - "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
19.136 - (fn prems=>
19.137 - [ (nat_ind_tac "m" prems 1),
19.138 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
19.139 + "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
19.140 + (fn _=>
19.141 + [ (nat_ind_tac "m" [] 1),
19.142 + (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
19.143 (*The final goal requires the commutative law for addition*)
19.144 - (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]);
19.145 + (rtac (add_commute RS subst_context) 1),
19.146 + (REPEAT (assume_tac 1)) ]);
19.147
19.148 (*Commutative law for multiplication*)
19.149 val mult_commute = prove_goal Arith.thy
19.150 "[| m:nat; n:nat |] ==> m #* n = n #* m"
19.151 (fn prems=>
19.152 [ (nat_ind_tac "m" prems 1),
19.153 - (ALLGOALS (ASM_SIMP_TAC
19.154 - (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
19.155 + (ALLGOALS (asm_simp_tac
19.156 + (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
19.157
19.158 (*addition distributes over multiplication*)
19.159 val add_mult_distrib = prove_goal Arith.thy
19.160 "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
19.161 (fn prems=>
19.162 [ (nat_ind_tac "m" prems 1),
19.163 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
19.164 + (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
19.165
19.166 (*Distributive law on the left; requires an extra typing premise*)
19.167 val add_mult_distrib_left = prove_goal Arith.thy
19.168 "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
19.169 (fn prems=>
19.170 let val mult_commute' = read_instantiate [("m","k")] mult_commute
19.171 - val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
19.172 - in [ (SIMP_TAC ss 1) ]
19.173 + val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
19.174 + in [ (simp_tac ss 1) ]
19.175 end);
19.176
19.177 (*Associative law for multiplication*)
19.178 @@ -223,7 +212,7 @@
19.179 "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
19.180 (fn prems=>
19.181 [ (nat_ind_tac "m" prems 1),
19.182 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
19.183 + (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
19.184
19.185
19.186 (*** Difference ***)
19.187 @@ -232,7 +221,7 @@
19.188 "m:nat ==> m #- m = 0"
19.189 (fn prems=>
19.190 [ (nat_ind_tac "m" prems 1),
19.191 - (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
19.192 + (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
19.193
19.194 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
19.195 val notless::prems = goal Arith.thy
19.196 @@ -241,8 +230,8 @@
19.197 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
19.198 by (resolve_tac prems 1);
19.199 by (resolve_tac prems 1);
19.200 -by (ALLGOALS (ASM_SIMP_TAC
19.201 - (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
19.202 +by (ALLGOALS (asm_simp_tac
19.203 + (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
19.204 naturals_are_ordinals]))));
19.205 val add_diff_inverse = result();
19.206
19.207 @@ -251,29 +240,24 @@
19.208 val [mnat,nnat] = goal Arith.thy
19.209 "[| m:nat; n:nat |] ==> (n#+m) #-n = m";
19.210 by (rtac (nnat RS nat_induct) 1);
19.211 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
19.212 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
19.213 val diff_add_inverse = result();
19.214
19.215 val [mnat,nnat] = goal Arith.thy
19.216 "[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
19.217 by (rtac (nnat RS nat_induct) 1);
19.218 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
19.219 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
19.220 val diff_add_0 = result();
19.221
19.222
19.223 (*** Remainder ***)
19.224
19.225 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
19.226 -val prems = goal Arith.thy
19.227 - "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
19.228 -by (cut_facts_tac prems 1);
19.229 +goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
19.230 by (etac rev_mp 1);
19.231 by (etac rev_mp 1);
19.232 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
19.233 -by (resolve_tac prems 1);
19.234 -by (resolve_tac prems 1);
19.235 -by (ALLGOALS (ASM_SIMP_TAC
19.236 - (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
19.237 +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
19.238 val div_termination = result();
19.239
19.240 val div_rls =
19.241 @@ -286,17 +270,17 @@
19.242 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
19.243 val mod_type = result();
19.244
19.245 -val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
19.246 +val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
19.247
19.248 val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m";
19.249 by (rtac (mod_def RS def_transrec RS trans) 1);
19.250 -by (SIMP_TAC (div_ss addrews prems) 1);
19.251 +by (simp_tac (div_ss addsimps prems) 1);
19.252 val mod_less = result();
19.253
19.254 val prems = goal Arith.thy
19.255 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n";
19.256 by (rtac (mod_def RS def_transrec RS trans) 1);
19.257 -by (SIMP_TAC (div_ss addrews prems) 1);
19.258 +by (simp_tac (div_ss addsimps prems) 1);
19.259 val mod_geq = result();
19.260
19.261 (*** Quotient ***)
19.262 @@ -310,13 +294,13 @@
19.263 val prems = goal Arith.thy
19.264 "[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0";
19.265 by (rtac (div_def RS def_transrec RS trans) 1);
19.266 -by (SIMP_TAC (div_ss addrews prems) 1);
19.267 +by (simp_tac (div_ss addsimps prems) 1);
19.268 val div_less = result();
19.269
19.270 val prems = goal Arith.thy
19.271 "[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)";
19.272 by (rtac (div_def RS def_transrec RS trans) 1);
19.273 -by (SIMP_TAC (div_ss addrews prems) 1);
19.274 +by (simp_tac (div_ss addsimps prems) 1);
19.275 val div_geq = result();
19.276
19.277 (*Main Result.*)
19.278 @@ -326,8 +310,8 @@
19.279 by (resolve_tac prems 1);
19.280 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
19.281 by (ALLGOALS
19.282 - (ASM_SIMP_TAC
19.283 - (arith_ss addrews ([mod_type,div_type] @ prems @
19.284 + (asm_simp_tac
19.285 + (arith_ss addsimps ([mod_type,div_type] @ prems @
19.286 [mod_less,mod_geq, div_less, div_geq,
19.287 add_assoc, add_diff_inverse, div_termination]))));
19.288 val mod_div_equality = result();
19.289 @@ -338,7 +322,7 @@
19.290 val [mnat,nnat] = goal Arith.thy
19.291 "[| m:nat; n:nat |] ==> ~ (m #+ n) : n";
19.292 by (rtac (mnat RS nat_induct) 1);
19.293 -by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
19.294 +by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
19.295 by (rtac notI 1);
19.296 by (etac notE 1);
19.297 by (etac (succI1 RS Ord_trans) 1);
20.1 --- a/src/ZF/arith.thy Fri Sep 17 12:53:53 1993 +0200
20.2 +++ b/src/ZF/arith.thy Fri Sep 17 16:16:38 1993 +0200
20.3 @@ -16,7 +16,7 @@
20.4 "#-" :: "[i,i]=>i" (infixl 65)
20.5
20.6 rules
20.7 - rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
20.8 + rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
20.9
20.10 add_def "m#+n == rec(m, n, %u v.succ(v))"
20.11 diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
21.1 --- a/src/ZF/bool.ML Fri Sep 17 12:53:53 1993 +0200
21.2 +++ b/src/ZF/bool.ML Fri Sep 17 16:16:38 1993 +0200
21.3 @@ -53,9 +53,6 @@
21.4 by (resolve_tac prems 1);
21.5 val cond_type = result();
21.6
21.7 -val [cond_cong] = mk_congs Bool.thy ["cond"];
21.8 -val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
21.9 -
21.10 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
21.11 by (rewtac rew);
21.12 by (rtac cond_1 1);
22.1 --- a/src/ZF/constructor.ML Fri Sep 17 12:53:53 1993 +0200
22.2 +++ b/src/ZF/constructor.ML Fri Sep 17 16:16:38 1993 +0200
22.3 @@ -40,7 +40,6 @@
22.4 val free_iffs : thm list (*freeness rewrite rules*)
22.5 val free_SEs : thm list (*freeness destruct rules*)
22.6 val mk_free : string -> thm (*makes freeness theorems*)
22.7 - val congs : thm list (*congruence rules for simplifier*)
22.8 end;
22.9
22.10
22.11 @@ -194,7 +193,6 @@
22.12 val case_eqns = map prove_case_equation
22.13 (flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
22.14
22.15 -val congs = mk_congs con_thy (flat (map #1 (const_decs @ ext_constants ext)));
22.16 end;
22.17
22.18
23.1 --- a/src/ZF/epsilon.ML Fri Sep 17 12:53:53 1993 +0200
23.2 +++ b/src/ZF/epsilon.ML Fri Sep 17 16:16:38 1993 +0200
23.3 @@ -64,8 +64,8 @@
23.4 "!!X A n. [| Transset(X); A<=X; n: nat |] ==> \
23.5 \ nat_rec(n, A, %m r. Union(r)) <= X";
23.6 by (etac nat_induct 1);
23.7 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
23.8 -by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
23.9 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
23.10 +by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
23.11 by (fast_tac ZF_cs 1);
23.12 val eclose_least_lemma = result();
23.13
23.14 @@ -126,8 +126,8 @@
23.15 by (rtac (kmemj RS eclose_induct) 1);
23.16 by (rtac wfrec_ssubst 1);
23.17 by (rtac wfrec_ssubst 1);
23.18 -by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
23.19 - jmemi RSN (2,mem_eclose_sing_trans)]) 1);
23.20 +by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
23.21 + jmemi RSN (2,mem_eclose_sing_trans)]) 1);
23.22 val wfrec_eclose_eq = result();
23.23
23.24 val [prem] = goal Epsilon.thy
23.25 @@ -139,8 +139,8 @@
23.26 goalw Epsilon.thy [transrec_def]
23.27 "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
23.28 by (rtac wfrec_ssubst 1);
23.29 -by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
23.30 - arg_in_eclose_sing, under_Memrel_eclose]) 1);
23.31 +by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
23.32 + under_Memrel_eclose]) 1);
23.33 val transrec = result();
23.34
23.35 (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
23.36 @@ -173,23 +173,12 @@
23.37 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
23.38 val Ord_transrec_type = result();
23.39
23.40 -(*Congruence*)
23.41 -val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
23.42 - "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> transrec(a,H)=transrec(a',H')";
23.43 -val transrec_ss =
23.44 - ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
23.45 - addrews (prems RL [sym]);
23.46 -by (SIMP_TAC transrec_ss 1);
23.47 -val transrec_cong = result();
23.48 -
23.49 (*** Rank ***)
23.50
23.51 -val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
23.52 -
23.53 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
23.54 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
23.55 by (rtac (rank_def RS def_transrec RS ssubst) 1);
23.56 -by (SIMP_TAC ZF_ss 1);
23.57 +by (simp_tac ZF_ss 1);
23.58 val rank = result();
23.59
23.60 goal Epsilon.thy "Ord(rank(a))";
23.61 @@ -203,7 +192,7 @@
23.62 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
23.63 by (rtac (major RS trans_induct) 1);
23.64 by (rtac (rank RS ssubst) 1);
23.65 -by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
23.66 +by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
23.67 val rank_of_Ord = result();
23.68
23.69 val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
24.1 --- a/src/ZF/fin.ML Fri Sep 17 12:53:53 1993 +0200
24.2 +++ b/src/ZF/fin.ML Fri Sep 17 16:16:38 1993 +0200
24.3 @@ -55,19 +55,19 @@
24.4 val Fin_induct = result();
24.5
24.6 (** Simplification for Fin **)
24.7 -val Fin_ss = arith_ss addcongs mk_congs Fin.thy ["Fin"] addrews Fin.intrs;
24.8 +val Fin_ss = arith_ss addsimps Fin.intrs;
24.9
24.10 (*The union of two finite sets is fin*)
24.11 val major::prems = goal Fin.thy
24.12 "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
24.13 by (rtac (major RS Fin_induct) 1);
24.14 -by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Un_0, Un_cons]))));
24.15 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
24.16 val Fin_UnI = result();
24.17
24.18 (*The union of a set of finite sets is fin*)
24.19 val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
24.20 by (rtac (major RS Fin_induct) 1);
24.21 -by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews [Union_0, Union_cons, Fin_UnI])));
24.22 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
24.23 val Fin_UnionI = result();
24.24
24.25 (*Every subset of a finite set is fin*)
24.26 @@ -76,10 +76,10 @@
24.27 etac (spec RS mp),
24.28 rtac subs]);
24.29 by (rtac (fin RS Fin_induct) 1);
24.30 -by (SIMP_TAC (Fin_ss addrews [subset_empty_iff]) 1);
24.31 +by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
24.32 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
24.33 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
24.34 -by (ALLGOALS (ASM_SIMP_TAC Fin_ss));
24.35 +by (ALLGOALS (asm_simp_tac Fin_ss));
24.36 val Fin_subset = result();
24.37
24.38 val major::prems = goal Fin.thy
24.39 @@ -89,7 +89,7 @@
24.40 \ |] ==> c<=b --> P(b-c)";
24.41 by (rtac (major RS Fin_induct) 1);
24.42 by (rtac (Diff_cons RS ssubst) 2);
24.43 -by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Diff_0, cons_subset_iff,
24.44 +by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,
24.45 Diff_subset RS Fin_subset]))));
24.46 val Fin_0_induct_lemma = result();
24.47
25.1 --- a/src/ZF/func.ML Fri Sep 17 12:53:53 1993 +0200
25.2 +++ b/src/ZF/func.ML Fri Sep 17 16:16:38 1993 +0200
25.3 @@ -37,7 +37,7 @@
25.4
25.5 val prems = goalw ZF.thy [Pi_def]
25.6 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
25.7 -by (prove_cong_tac (prems@[Collect_cong,Sigma_cong,ball_cong]) 1);
25.8 +by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
25.9 val Pi_cong = result();
25.10
25.11 (*Weaking one function type to another*)
25.12 @@ -84,8 +84,7 @@
25.13 by (rtac refl 1);
25.14 val memberPiE = result();
25.15
25.16 -(*Conclusion is flexible -- use res_inst_tac or else RS with a theorem
25.17 - of the form f:A->B *)
25.18 +(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
25.19 goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)";
25.20 by (rtac (fun_unique_Pair RS ex1E) 1);
25.21 by (REPEAT (assume_tac 1));
25.22 @@ -94,6 +93,11 @@
25.23 by (REPEAT (assume_tac 1));
25.24 val apply_type = result();
25.25
25.26 +(*This version is acceptable to the simplifier*)
25.27 +goal ZF.thy "!!f. [| f: A->B; a:A |] ==> f`a : B";
25.28 +by (REPEAT (ares_tac [apply_type] 1));
25.29 +val apply_funtype = result();
25.30 +
25.31 goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
25.32 by (rtac (fun_unique_Pair RS ex1E) 1);
25.33 by (resolve_tac [apply_equality RS ssubst] 3);
25.34 @@ -169,11 +173,8 @@
25.35
25.36 (*congruence rule for lambda abstraction*)
25.37 val prems = goalw ZF.thy [lam_def]
25.38 - "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> \
25.39 -\ (lam x:A.b(x)) = (lam x:A'.b'(x))";
25.40 -by (rtac RepFun_cong 1);
25.41 -by (res_inst_tac [("t","Pair")] subst_context2 2);
25.42 -by (REPEAT (ares_tac (prems@[refl]) 1));
25.43 + "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
25.44 +by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
25.45 val lam_cong = result();
25.46
25.47 val [major] = goal ZF.thy
25.48 @@ -259,7 +260,7 @@
25.49 val [prem] = goalw ZF.thy [restrict_def]
25.50 "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
25.51 by (rtac (refl RS lam_cong) 1);
25.52 -be (prem RS subsetD RS beta) 1; (*easier than calling SIMP_TAC*)
25.53 +be (prem RS subsetD RS beta) 1; (*easier than calling simp_tac*)
25.54 val restrict_lam_eq = result();
25.55
25.56
26.1 --- a/src/ZF/ind-syntax.ML Fri Sep 17 12:53:53 1993 +0200
26.2 +++ b/src/ZF/ind-syntax.ML Fri Sep 17 16:16:38 1993 +0200
26.3 @@ -37,7 +37,6 @@
26.4 flatten_term sign (Logic.mk_equals (lhs,rhs)))
26.5 end;
26.6
26.7 -(*export to Pure/sign? Used in Provers/simp.ML...*)
26.8 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
26.9
26.10 (*export to Pure/library? *)
27.1 --- a/src/ZF/ind_syntax.ML Fri Sep 17 12:53:53 1993 +0200
27.2 +++ b/src/ZF/ind_syntax.ML Fri Sep 17 16:16:38 1993 +0200
27.3 @@ -37,7 +37,6 @@
27.4 flatten_term sign (Logic.mk_equals (lhs,rhs)))
27.5 end;
27.6
27.7 -(*export to Pure/sign? Used in Provers/simp.ML...*)
27.8 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
27.9
27.10 (*export to Pure/library? *)
28.1 --- a/src/ZF/list.ML Fri Sep 17 12:53:53 1993 +0200
28.2 +++ b/src/ZF/list.ML Fri Sep 17 16:16:38 1993 +0200
28.3 @@ -62,7 +62,7 @@
28.4 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(<x,y>) \
28.5 \ |] ==> list_case(l,c,h) : C(l)";
28.6 by (rtac (major RS list_induct) 1);
28.7 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
28.8 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
28.9 ([list_case_0,list_case_Pair]@prems))));
28.10 val list_case_type = result();
28.11 ****)
28.12 @@ -71,10 +71,10 @@
28.13 (** For recursion **)
28.14
28.15 goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
28.16 -by (SIMP_TAC rank_ss 1);
28.17 +by (simp_tac rank_ss 1);
28.18 val rank_Cons1 = result();
28.19
28.20 goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
28.21 -by (SIMP_TAC rank_ss 1);
28.22 +by (simp_tac rank_ss 1);
28.23 val rank_Cons2 = result();
28.24
29.1 --- a/src/ZF/listfn.ML Fri Sep 17 12:53:53 1993 +0200
29.2 +++ b/src/ZF/listfn.ML Fri Sep 17 16:16:38 1993 +0200
29.3 @@ -11,19 +11,14 @@
29.4
29.5 (** list_rec -- by Vset recursion **)
29.6
29.7 -(*Used to verify list_rec*)
29.8 -val list_rec_ss = ZF_ss
29.9 - addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
29.10 - addrews List.case_eqns;
29.11 -
29.12 goal ListFn.thy "list_rec(Nil,c,h) = c";
29.13 by (rtac (list_rec_def RS def_Vrec RS trans) 1);
29.14 -by (SIMP_TAC list_rec_ss 1);
29.15 +by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
29.16 val list_rec_Nil = result();
29.17
29.18 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
29.19 by (rtac (list_rec_def RS def_Vrec RS trans) 1);
29.20 -by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
29.21 +by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
29.22 val list_rec_Cons = result();
29.23
29.24 (*Type checking -- proved by induction, as usual*)
29.25 @@ -33,8 +28,8 @@
29.26 \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
29.27 \ |] ==> list_rec(l,c,h) : C(l)";
29.28 by (list_ind_tac "l" prems 1);
29.29 -by (ALLGOALS (ASM_SIMP_TAC
29.30 - (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
29.31 +by (ALLGOALS (asm_simp_tac
29.32 + (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
29.33 val list_rec_type = result();
29.34
29.35 (** Versions for use with definitions **)
29.36 @@ -122,47 +117,42 @@
29.37 map_type, map_type2, app_type, length_type, rev_type, flat_type,
29.38 list_add_type];
29.39
29.40 -val list_congs =
29.41 - List.congs @
29.42 - mk_congs ListFn.thy
29.43 - ["list_rec","map","op @","length","rev","flat","list_add"];
29.44 -
29.45 val list_ss = arith_ss
29.46 - addcongs list_congs
29.47 - addrews List.case_eqns
29.48 - addrews list_typechecks
29.49 - addrews [list_rec_Nil, list_rec_Cons,
29.50 + addsimps List.case_eqns
29.51 + addsimps [list_rec_Nil, list_rec_Cons,
29.52 map_Nil, map_Cons,
29.53 app_Nil, app_Cons,
29.54 length_Nil, length_Cons,
29.55 rev_Nil, rev_Cons,
29.56 flat_Nil, flat_Cons,
29.57 - list_add_Nil, list_add_Cons];
29.58 + list_add_Nil, list_add_Cons]
29.59 + setsolver (type_auto_tac list_typechecks);
29.60 +(*Could also rewrite using the list_typechecks...*)
29.61
29.62 (*** theorems about map ***)
29.63
29.64 val prems = goal ListFn.thy
29.65 "l: list(A) ==> map(%u.u, l) = l";
29.66 by (list_ind_tac "l" prems 1);
29.67 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.68 +by (ALLGOALS (asm_simp_tac list_ss));
29.69 val map_ident = result();
29.70
29.71 val prems = goal ListFn.thy
29.72 "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
29.73 by (list_ind_tac "l" prems 1);
29.74 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.75 +by (ALLGOALS (asm_simp_tac list_ss));
29.76 val map_compose = result();
29.77
29.78 val prems = goal ListFn.thy
29.79 "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
29.80 by (list_ind_tac "xs" prems 1);
29.81 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.82 +by (ALLGOALS (asm_simp_tac list_ss));
29.83 val map_app_distrib = result();
29.84
29.85 val prems = goal ListFn.thy
29.86 "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
29.87 by (list_ind_tac "ls" prems 1);
29.88 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
29.89 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
29.90 val map_flat = result();
29.91
29.92 val prems = goal ListFn.thy
29.93 @@ -170,9 +160,7 @@
29.94 \ list_rec(map(h,l), c, d) = \
29.95 \ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
29.96 by (list_ind_tac "l" prems 1);
29.97 -by (ALLGOALS
29.98 - (ASM_SIMP_TAC
29.99 - (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
29.100 +by (ALLGOALS (asm_simp_tac list_ss));
29.101 val list_rec_map = result();
29.102
29.103 (** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
29.104 @@ -183,7 +171,7 @@
29.105 val prems = goal ListFn.thy
29.106 "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
29.107 by (list_ind_tac "l" prems 1);
29.108 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.109 +by (ALLGOALS (asm_simp_tac list_ss));
29.110 val map_list_Collect = result();
29.111
29.112 (*** theorems about length ***)
29.113 @@ -191,13 +179,13 @@
29.114 val prems = goal ListFn.thy
29.115 "xs: list(A) ==> length(map(h,xs)) = length(xs)";
29.116 by (list_ind_tac "xs" prems 1);
29.117 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.118 +by (ALLGOALS (asm_simp_tac list_ss));
29.119 val length_map = result();
29.120
29.121 val prems = goal ListFn.thy
29.122 "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
29.123 by (list_ind_tac "xs" prems 1);
29.124 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.125 +by (ALLGOALS (asm_simp_tac list_ss));
29.126 val length_app = result();
29.127
29.128 (* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
29.129 @@ -207,60 +195,59 @@
29.130 val prems = goal ListFn.thy
29.131 "xs: list(A) ==> length(rev(xs)) = length(xs)";
29.132 by (list_ind_tac "xs" prems 1);
29.133 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
29.134 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
29.135 val length_rev = result();
29.136
29.137 val prems = goal ListFn.thy
29.138 "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
29.139 by (list_ind_tac "ls" prems 1);
29.140 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
29.141 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
29.142 val length_flat = result();
29.143
29.144 (*** theorems about app ***)
29.145
29.146 val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
29.147 by (rtac (major RS List.induct) 1);
29.148 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.149 +by (ALLGOALS (asm_simp_tac list_ss));
29.150 val app_right_Nil = result();
29.151
29.152 val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
29.153 by (list_ind_tac "xs" prems 1);
29.154 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
29.155 +by (ALLGOALS (asm_simp_tac list_ss));
29.156 val app_assoc = result();
29.157
29.158 val prems = goal ListFn.thy
29.159 "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
29.160 by (list_ind_tac "ls" prems 1);
29.161 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
29.162 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
29.163 val flat_app_distrib = result();
29.164
29.165 (*** theorems about rev ***)
29.166
29.167 val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
29.168 by (list_ind_tac "l" prems 1);
29.169 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
29.170 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
29.171 val rev_map_distrib = result();
29.172
29.173 (*Simplifier needs the premises as assumptions because rewriting will not
29.174 instantiate the variable ?A in the rules' typing conditions; note that
29.175 rev_type does not instantiate ?A. Only the premises do.
29.176 *)
29.177 -val prems = goal ListFn.thy
29.178 - "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
29.179 -by (cut_facts_tac prems 1);
29.180 +goal ListFn.thy
29.181 + "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
29.182 by (etac List.induct 1);
29.183 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
29.184 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
29.185 val rev_app_distrib = result();
29.186
29.187 val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
29.188 by (list_ind_tac "l" prems 1);
29.189 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
29.190 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
29.191 val rev_rev_ident = result();
29.192
29.193 val prems = goal ListFn.thy
29.194 "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
29.195 by (list_ind_tac "ls" prems 1);
29.196 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews
29.197 +by (ALLGOALS (asm_simp_tac (list_ss addsimps
29.198 [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
29.199 val rev_flat = result();
29.200
29.201 @@ -273,22 +260,22 @@
29.202 by (cut_facts_tac prems 1);
29.203 by (list_ind_tac "xs" prems 1);
29.204 by (ALLGOALS
29.205 - (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
29.206 -by (resolve_tac arith_congs 1);
29.207 -by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
29.208 + (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
29.209 +by (rtac (add_commute RS subst_context) 1);
29.210 +by (REPEAT (ares_tac [refl, list_add_type] 1));
29.211 val list_add_app = result();
29.212
29.213 val prems = goal ListFn.thy
29.214 "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
29.215 by (list_ind_tac "l" prems 1);
29.216 by (ALLGOALS
29.217 - (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
29.218 + (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
29.219 val list_add_rev = result();
29.220
29.221 val prems = goal ListFn.thy
29.222 "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
29.223 by (list_ind_tac "ls" prems 1);
29.224 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
29.225 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
29.226 by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
29.227 val list_add_flat = result();
29.228
29.229 @@ -301,6 +288,6 @@
29.230 \ |] ==> P(l)";
29.231 by (rtac (major RS rev_rev_ident RS subst) 1);
29.232 by (rtac (major RS rev_type RS List.induct) 1);
29.233 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
29.234 +by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
29.235 val list_append_induct = result();
29.236
30.1 --- a/src/ZF/nat.ML Fri Sep 17 12:53:53 1993 +0200
30.2 +++ b/src/ZF/nat.ML Fri Sep 17 16:16:38 1993 +0200
30.3 @@ -95,8 +95,8 @@
30.4 \ |] ==> m <= n --> P(m) --> P(n)";
30.5 by (nat_ind_tac "n" prems 1);
30.6 by (ALLGOALS
30.7 - (ASM_SIMP_TAC
30.8 - (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
30.9 + (asm_simp_tac
30.10 + (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
30.11 Ord_nat RS Ord_in_Ord]))));
30.12 val nat_induct_from_lemma = result();
30.13
30.14 @@ -127,17 +127,17 @@
30.15
30.16 (** nat_case **)
30.17
30.18 -goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
30.19 +goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
30.20 by (fast_tac (ZF_cs addIs [the_equality]) 1);
30.21 val nat_case_0 = result();
30.22
30.23 -goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
30.24 +goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
30.25 by (fast_tac (ZF_cs addIs [the_equality]) 1);
30.26 val nat_case_succ = result();
30.27
30.28 val major::prems = goal Nat.thy
30.29 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \
30.30 -\ |] ==> nat_case(n,a,b) : C(n)";
30.31 +\ |] ==> nat_case(a,b,n) : C(n)";
30.32 by (rtac (major RS nat_induct) 1);
30.33 by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
30.34 nat_case_succ RS ssubst] 1
30.35 @@ -145,13 +145,6 @@
30.36 by (assume_tac 1);
30.37 val nat_case_type = result();
30.38
30.39 -val prems = goalw Nat.thy [nat_case_def]
30.40 - "[| n=n'; a=a'; !!m z. b(m)=b'(m) \
30.41 -\ |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
30.42 -by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
30.43 - ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
30.44 -val nat_case_cong = result();
30.45 -
30.46
30.47 (** nat_rec -- used to define eclose and transrec, then obsolete **)
30.48
30.49 @@ -165,11 +158,10 @@
30.50 val [prem] = goal Nat.thy
30.51 "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
30.52 val nat_rec_ss = ZF_ss
30.53 - addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
30.54 - addrews [prem, nat_case_succ, nat_succI, Memrel_iff,
30.55 - vimage_singleton_iff];
30.56 + addsimps [prem, nat_case_succ, nat_succI, Memrel_iff,
30.57 + vimage_singleton_iff];
30.58 by (rtac nat_rec_trans 1);
30.59 -by (SIMP_TAC nat_rec_ss 1);
30.60 +by (simp_tac nat_rec_ss 1);
30.61 val nat_rec_succ = result();
30.62
30.63 (** The union of two natural numbers is a natural number -- their maximum **)
31.1 --- a/src/ZF/nat.thy Fri Sep 17 12:53:53 1993 +0200
31.2 +++ b/src/ZF/nat.thy Fri Sep 17 16:16:38 1993 +0200
31.3 @@ -9,7 +9,7 @@
31.4 Nat = Ord + Bool +
31.5 consts
31.6 nat :: "i"
31.7 - nat_case :: "[i, i, i=>i]=>i"
31.8 + nat_case :: "[i, i=>i, i]=>i"
31.9 nat_rec :: "[i, i, [i,i]=>i]=>i"
31.10
31.11 rules
31.12 @@ -17,10 +17,10 @@
31.13 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
31.14
31.15 nat_case_def
31.16 - "nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
31.17 + "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
31.18
31.19 nat_rec_def
31.20 "nat_rec(k,a,b) == \
31.21 -\ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"
31.22 +\ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
31.23
31.24 end
32.1 --- a/src/ZF/ord.ML Fri Sep 17 12:53:53 1993 +0200
32.2 +++ b/src/ZF/ord.ML Fri Sep 17 16:16:38 1993 +0200
32.3 @@ -318,7 +318,7 @@
32.4
32.5 goal Ord.thy
32.6 "!!i j. [| Ord(i); Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
32.7 -by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
32.8 +by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
32.9 by (fast_tac ZF_cs 1);
32.10 val subset_succ_iff = result();
32.11
32.12 @@ -356,17 +356,17 @@
32.13 goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k";
32.14 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
32.15 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
32.16 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
32.17 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
32.18 by (rtac (Un_commute RS ssubst) 1);
32.19 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
32.20 +by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
32.21 val Ord_member_UnI = result();
32.22
32.23 goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Int j : k";
32.24 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
32.25 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
32.26 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
32.27 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
32.28 by (rtac (Int_commute RS ssubst) 1);
32.29 -by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
32.30 +by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
32.31 val Ord_member_IntI = result();
32.32
32.33
33.1 --- a/src/ZF/pair.ML Fri Sep 17 12:53:53 1993 +0200
33.2 +++ b/src/ZF/pair.ML Fri Sep 17 16:16:38 1993 +0200
33.3 @@ -15,7 +15,7 @@
33.4
33.5 val Pair_iff = prove_goalw ZF.thy [Pair_def]
33.6 "<a,b> = <c,d> <-> a=c & b=d"
33.7 - (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
33.8 + (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
33.9 (fast_tac FOL_cs 1) ]);
33.10
33.11 val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
33.12 @@ -89,7 +89,7 @@
33.13 val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
33.14 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
33.15 \ Sigma(A,B) = Sigma(A',B')"
33.16 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
33.17 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
33.18
33.19 val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
33.20 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
33.21 @@ -114,13 +114,6 @@
33.22 (etac ssubst 1),
33.23 (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
33.24
33.25 -(*This congruence rule uses NO typing information...*)
33.26 -val split_cong = prove_goalw ZF.thy [split_def]
33.27 - "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
33.28 -\ split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
33.29 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
33.30 -
33.31 -
33.32 (*** conversions for fst and snd ***)
33.33
33.34 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
34.1 --- a/src/ZF/perm.ML Fri Sep 17 12:53:53 1993 +0200
34.2 +++ b/src/ZF/perm.ML Fri Sep 17 16:16:38 1993 +0200
34.3 @@ -52,6 +52,7 @@
34.4 (* f: bij(A,B) ==> f: A->B *)
34.5 val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
34.6
34.7 +
34.8 (** Identity function **)
34.9
34.10 val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";
34.11 @@ -76,7 +77,7 @@
34.12
34.13 goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
34.14 by (REPEAT (ares_tac [CollectI,lam_type] 1));
34.15 -by (SIMP_TAC ZF_ss 1);
34.16 +by (simp_tac ZF_ss 1);
34.17 val id_inj = result();
34.18
34.19 goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
34.20 @@ -262,7 +263,7 @@
34.21 "!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
34.22 by (safe_tac comp_cs);
34.23 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
34.24 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
34.25 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
34.26 val comp_mem_injD1 = result();
34.27
34.28 goalw Perm.thy [inj_def,surj_def]
34.29 @@ -271,9 +272,10 @@
34.30 by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
34.31 by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
34.32 by (REPEAT (assume_tac 1));
34.33 -by (safe_tac (comp_cs addSIs ZF_congs));
34.34 +by (safe_tac comp_cs);
34.35 +by (res_inst_tac [("t", "op `(g)")] subst_context 1);
34.36 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
34.37 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
34.38 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
34.39 val comp_mem_injD2 = result();
34.40
34.41 goalw Perm.thy [surj_def]
34.42 @@ -427,7 +429,9 @@
34.43 by (etac fun_extend 1);
34.44 by (REPEAT (ares_tac [ballI] 1));
34.45 by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
34.46 -(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
34.47 -by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
34.48 +(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
34.49 + using ZF_ss! But FOL_ss ignores the assumption...*)
34.50 +by (ALLGOALS (asm_simp_tac
34.51 + (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
34.52 by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
34.53 val inj_extend = result();
35.1 --- a/src/ZF/qpair.ML Fri Sep 17 12:53:53 1993 +0200
35.2 +++ b/src/ZF/qpair.ML Fri Sep 17 16:16:38 1993 +0200
35.3 @@ -74,7 +74,7 @@
35.4 val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
35.5 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
35.6 \ QSigma(A,B) = QSigma(A',B')"
35.7 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
35.8 + (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
35.9
35.10 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
35.11 (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
35.12 @@ -98,12 +98,6 @@
35.13 (etac ssubst 1),
35.14 (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
35.15
35.16 -(*This congruence rule uses NO typing information...*)
35.17 -val qsplit_cong = prove_goalw QPair.thy [qsplit_def]
35.18 - "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
35.19 -\ qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
35.20 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
35.21 -
35.22
35.23 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
35.24
35.25 @@ -243,7 +237,7 @@
35.26 val qsum_subset_iff = result();
35.27
35.28 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
35.29 -by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
35.30 +by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
35.31 by (fast_tac ZF_cs 1);
35.32 val qsum_equal_iff = result();
35.33
35.34 @@ -259,12 +253,6 @@
35.35 by (rtac cond_1 1);
35.36 val qcase_QInr = result();
35.37
35.38 -val prems = goalw QPair.thy [qcase_def]
35.39 - "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
35.40 -\ qcase(c,d,u)=qcase(c',d',u')";
35.41 -by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
35.42 -val qcase_cong = result();
35.43 -
35.44 val major::prems = goal QPair.thy
35.45 "[| u: A <+> B; \
35.46 \ !!x. x: A ==> c(x): C(QInl(x)); \
35.47 @@ -272,7 +260,7 @@
35.48 \ |] ==> qcase(c,d,u) : C(u)";
35.49 by (rtac (major RS qsumE) 1);
35.50 by (ALLGOALS (etac ssubst));
35.51 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
35.52 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
35.53 (prems@[qcase_QInl,qcase_QInr]))));
35.54 val qcase_type = result();
35.55
36.1 --- a/src/ZF/quniv.ML Fri Sep 17 12:53:53 1993 +0200
36.2 +++ b/src/ZF/quniv.ML Fri Sep 17 16:16:38 1993 +0200
36.3 @@ -205,7 +205,7 @@
36.4
36.5 goalw QUniv.thy [QPair_def,sum_def]
36.6 "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
36.7 -by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
36.8 +by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
36.9 val QPair_Int_quniv_eq = result();
36.10
36.11 (**** "Take-lemma" rules for proving c: quniv(A) ****)
37.1 --- a/src/ZF/simpdata.ML Fri Sep 17 12:53:53 1993 +0200
37.2 +++ b/src/ZF/simpdata.ML Fri Sep 17 16:16:38 1993 +0200
37.3 @@ -10,7 +10,7 @@
37.4 (writeln s; prove_goal ZF.thy s
37.5 (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
37.6
37.7 -val mem_rews = map prove_fun
37.8 +val mem_simps = map prove_fun
37.9 [ "a:0 <-> False",
37.10 "a : A Un B <-> a:A | a:B",
37.11 "a : A Int B <-> a:A & a:B",
37.12 @@ -45,7 +45,7 @@
37.13 NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
37.14 fun type_auto_tac tyrls hyps = SELECT_GOAL
37.15 (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
37.16 - ORELSE ares_tac [TrueI,ballI,allI,conjI,impI] 1));
37.17 + ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
37.18
37.19 (** New version of mk_rew_rules **)
37.20
37.21 @@ -80,41 +80,19 @@
37.22 | _ $ A => tryrules atomize_pairs A
37.23 end;
37.24
37.25 -fun ZF_mk_rew_rules th = map mk_eq (atomize th);
37.26 +fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
37.27
37.28
37.29 -fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
37.30 +val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false,
37.31 + beta, eta, restrict, fst_conv, snd_conv, split];
37.32
37.33 -structure ZF_SimpData : SIMP_DATA =
37.34 - struct
37.35 - val refl_thms = FOL_SimpData.refl_thms
37.36 - val trans_thms = FOL_SimpData.trans_thms
37.37 - val red1 = FOL_SimpData.red1
37.38 - val red2 = FOL_SimpData.red2
37.39 - val mk_rew_rules = ZF_mk_rew_rules
37.40 - val norm_thms = FOL_SimpData.norm_thms
37.41 - val subst_thms = FOL_SimpData.subst_thms
37.42 - val dest_red = FOL_SimpData.dest_red
37.43 - end;
37.44 +(*Sigma_cong, Pi_cong NOT included by default since they cause
37.45 + flex-flex pairs and the "Check your prover" error -- because most
37.46 + Sigma's and Pi's are abbreviated as * or -> *)
37.47 +val ZF_congs =
37.48 + [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
37.49
37.50 -structure ZF_Simp = SimpFun(ZF_SimpData);
37.51 -
37.52 -open ZF_Simp;
37.53 -
37.54 -(*Redeclared because the previous FOL_ss belongs to a different instance
37.55 - of type simpset*)
37.56 -val FOL_ss = empty_ss addcongs FOL_congs addrews FOL_rews
37.57 - setauto auto_tac[TrueI,ballI];
37.58 -
37.59 -(** Basic congruence and rewrite rules for ZF set theory **)
37.60 -
37.61 -val ZF_congs =
37.62 - [ball_cong,bex_cong,Replace_cong,RepFun_cong,Collect_cong,the_cong,
37.63 - if_cong,Sigma_cong,split_cong,Pi_cong,lam_cong] @ basic_ZF_congs;
37.64 -
37.65 -val ZF_rews = [empty_subsetI, ball_rew, if_true, if_false,
37.66 - beta, eta, restrict,
37.67 - fst_conv, snd_conv, split];
37.68 -
37.69 -val ZF_ss = FOL_ss addcongs ZF_congs addrews (ZF_rews@mem_rews);
37.70 -
37.71 +val ZF_ss = FOL_ss
37.72 + setmksimps ZF_mk_rew_rules
37.73 + addsimps (ZF_simps@mem_simps)
37.74 + addcongs ZF_congs;
38.1 --- a/src/ZF/sum.ML Fri Sep 17 12:53:53 1993 +0200
38.2 +++ b/src/ZF/sum.ML Fri Sep 17 16:16:38 1993 +0200
38.3 @@ -83,7 +83,7 @@
38.4 val sum_subset_iff = result();
38.5
38.6 goal Sum.thy "A+B = C+D <-> A=C & B=D";
38.7 -by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
38.8 +by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
38.9 by (fast_tac ZF_cs 1);
38.10 val sum_equal_iff = result();
38.11
38.12 @@ -99,12 +99,6 @@
38.13 by (rtac cond_1 1);
38.14 val case_Inr = result();
38.15
38.16 -val prems = goalw Sum.thy [case_def]
38.17 - "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
38.18 -\ case(c,d,u)=case(c',d',u')";
38.19 -by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
38.20 -val case_cong = result();
38.21 -
38.22 val major::prems = goal Sum.thy
38.23 "[| u: A+B; \
38.24 \ !!x. x: A ==> c(x): C(Inl(x)); \
38.25 @@ -112,7 +106,7 @@
38.26 \ |] ==> case(c,d,u) : C(u)";
38.27 by (rtac (major RS sumE) 1);
38.28 by (ALLGOALS (etac ssubst));
38.29 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
38.30 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
38.31 (prems@[case_Inl,case_Inr]))));
38.32 val case_type = result();
38.33
39.1 --- a/src/ZF/univ.ML Fri Sep 17 12:53:53 1993 +0200
39.2 +++ b/src/ZF/univ.ML Fri Sep 17 16:16:38 1993 +0200
39.3 @@ -11,7 +11,7 @@
39.4 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
39.5 goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
39.6 by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
39.7 -by (SIMP_TAC ZF_ss 1);
39.8 +by (simp_tac ZF_ss 1);
39.9 val Vfrom = result();
39.10
39.11 (** Monotonicity **)
39.12 @@ -122,9 +122,8 @@
39.13
39.14 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
39.15 by (rtac (Vfrom RS trans) 1);
39.16 -brs ([refl] RL ZF_congs) 1;
39.17 -by (rtac equalityI 1);
39.18 -by (rtac (succI1 RS RepFunI RS Union_upper) 2);
39.19 +by (rtac (succI1 RS RepFunI RS Union_upper RSN
39.20 + (2, equalityI RS subst_context)) 1);
39.21 by (rtac UN_least 1);
39.22 by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
39.23 by (etac member_succD 1);
39.24 @@ -473,16 +472,16 @@
39.25 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
39.26
39.27 val rank_ss = ZF_ss
39.28 - addrews [split, case_Inl, case_Inr, Vset_rankI]
39.29 - addrews rank_trans_rls;
39.30 + addsimps [case_Inl, case_Inr, Vset_rankI]
39.31 + addsimps rank_trans_rls;
39.32
39.33 (** Recursion over Vset levels! **)
39.34
39.35 (*NOT SUITABLE FOR REWRITING: recursive!*)
39.36 goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
39.37 by (rtac (transrec RS ssubst) 1);
39.38 -by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta,
39.39 - VsetI RS beta]) 1);
39.40 +by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta,
39.41 + VsetI RS beta]) 1);
39.42 val Vrec = result();
39.43
39.44 (*This form avoids giant explosions in proofs. NOTE USE OF == *)
39.45 @@ -493,13 +492,6 @@
39.46 by (rtac Vrec 1);
39.47 val def_Vrec = result();
39.48
39.49 -val prems = goalw Univ.thy [Vrec_def]
39.50 - "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> Vrec(a,H)=Vrec(a',H')";
39.51 -val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
39.52 - addrews (prems RL [sym]);
39.53 -by (SIMP_TAC Vrec_ss 1);
39.54 -val Vrec_cong = result();
39.55 -
39.56
39.57 (*** univ(A) ***)
39.58
40.1 --- a/src/ZF/upair.ML Fri Sep 17 12:53:53 1993 +0200
40.2 +++ b/src/ZF/upair.ML Fri Sep 17 16:16:38 1993 +0200
40.3 @@ -167,10 +167,6 @@
40.4 (resolve_tac [major RS the_equality2 RS ssubst] 1),
40.5 (REPEAT (assume_tac 1)) ]);
40.6
40.7 -val the_cong = prove_goalw ZF.thy [the_def]
40.8 - "[| !!y. P(y) <-> Q(y) |] ==> (THE x. P(x)) = (THE x. Q(x))"
40.9 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
40.10 -
40.11
40.12 (*** if -- a conditional expression for formulae ***)
40.13
40.14 @@ -182,38 +178,34 @@
40.15 by (fast_tac (lemmas_cs addIs [the_equality]) 1);
40.16 val if_false = result();
40.17
40.18 +(*Never use with case splitting, or if P is known to be true or false*)
40.19 val prems = goalw ZF.thy [if_def]
40.20 - "[| P<->Q; a=c; b=d |] ==> if(P,a,b) = if(Q,c,d)";
40.21 -by (REPEAT (resolve_tac (prems@[refl,the_cong]@FOL_congs) 1));
40.22 + "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
40.23 +by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1);
40.24 val if_cong = result();
40.25
40.26 (*Not needed for rewriting, since P would rewrite to True anyway*)
40.27 -val prems = goalw ZF.thy [if_def] "P ==> if(P,a,b) = a";
40.28 -by (cut_facts_tac prems 1);
40.29 +goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
40.30 by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
40.31 val if_P = result();
40.32
40.33 (*Not needed for rewriting, since P would rewrite to False anyway*)
40.34 -val prems = goalw ZF.thy [if_def] "~P ==> if(P,a,b) = b";
40.35 -by (cut_facts_tac prems 1);
40.36 +goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
40.37 by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
40.38 val if_not_P = result();
40.39
40.40 -val if_ss =
40.41 - FOL_ss addcongs (if_cong :: mk_typed_congs ZF.thy [("P", "i=>o")]
40.42 - @ basic_ZF_congs)
40.43 - addrews [if_true,if_false];
40.44 +val if_ss = FOL_ss addsimps [if_true,if_false];
40.45
40.46 val expand_if = prove_goal ZF.thy
40.47 "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
40.48 (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
40.49 - (ASM_SIMP_TAC if_ss 1),
40.50 - (ASM_SIMP_TAC if_ss 1) ]);
40.51 + (asm_simp_tac if_ss 1),
40.52 + (asm_simp_tac if_ss 1) ]);
40.53
40.54 val prems = goal ZF.thy
40.55 "[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A";
40.56 by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);
40.57 -by (ALLGOALS (ASM_SIMP_TAC (if_ss addrews prems)));
40.58 +by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
40.59 val if_type = result();
40.60
40.61
41.1 --- a/src/ZF/wf.ML Fri Sep 17 12:53:53 1993 +0200
41.2 +++ b/src/ZF/wf.ML Fri Sep 17 16:16:38 1993 +0200
41.3 @@ -19,10 +19,6 @@
41.4
41.5 open WF;
41.6
41.7 -val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
41.8 -
41.9 -val wf_ss = ZF_ss addcongs [H_cong];
41.10 -
41.11
41.12 (*** Well-founded relations ***)
41.13
41.14 @@ -138,13 +134,13 @@
41.15 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
41.16 spec RS mp instantiates induction hypotheses*)
41.17 fun indhyp_tac hyps =
41.18 - ares_tac (TrueI::hyps) ORELSE'
41.19 + resolve_tac (TrueI::refl::hyps) ORELSE'
41.20 (cut_facts_tac hyps THEN'
41.21 DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
41.22 eresolve_tac [underD, transD, spec RS mp]));
41.23
41.24 -(*** NOTE! some simplifications need a different auto_tac!! ***)
41.25 -val wf_super_ss = wf_ss setauto indhyp_tac;
41.26 +(*** NOTE! some simplifications need a different solver!! ***)
41.27 +val wf_super_ss = ZF_ss setsolver indhyp_tac;
41.28
41.29 val prems = goalw WF.thy [is_recfun_def]
41.30 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
41.31 @@ -153,7 +149,7 @@
41.32 by (wf_ind_tac "x" prems 1);
41.33 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
41.34 by (rewtac restrict_def);
41.35 -by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
41.36 +by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
41.37 val is_recfun_equal_lemma = result();
41.38 val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
41.39
41.40 @@ -165,7 +161,7 @@
41.41 by (rtac (consI1 RS restrict_type RS fun_extension) 1);
41.42 by (etac is_recfun_type 1);
41.43 by (ALLGOALS
41.44 - (ASM_SIMP_TAC (wf_super_ss addrews
41.45 + (asm_simp_tac (wf_super_ss addsimps
41.46 [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
41.47 val is_recfun_cut = result();
41.48
41.49 @@ -195,13 +191,13 @@
41.50 by (REPEAT (assume_tac 2));
41.51 by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
41.52 (*Applying the substitution: must keep the quantified assumption!!*)
41.53 -by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
41.54 +by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
41.55 by (fold_tac [is_recfun_def]);
41.56 -by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
41.57 +by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
41.58 by (rtac is_recfun_type 1);
41.59 by (ALLGOALS
41.60 - (ASM_SIMP_TAC
41.61 - (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
41.62 + (asm_simp_tac
41.63 + (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
41.64 val unfold_the_recfun = result();
41.65
41.66
41.67 @@ -214,13 +210,12 @@
41.68 val the_recfun_cut = result();
41.69
41.70 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
41.71 -val prems = goalw WF.thy [wftrec_def]
41.72 - "[| wf(r); trans(r) |] ==> \
41.73 -\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
41.74 +goalw WF.thy [wftrec_def]
41.75 + "!!r. [| wf(r); trans(r) |] ==> \
41.76 +\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
41.77 by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
41.78 -by (ALLGOALS (ASM_SIMP_TAC
41.79 - (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym,
41.80 - the_recfun_cut]))));
41.81 +by (ALLGOALS (asm_simp_tac
41.82 + (ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
41.83 val wftrec = result();
41.84
41.85 (** Removal of the premise trans(r) **)
41.86 @@ -230,8 +225,7 @@
41.87 "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
41.88 by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
41.89 by (rtac trans_trancl 1);
41.90 -by (rtac (refl RS H_cong) 1);
41.91 -by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
41.92 +by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
41.93 by (etac r_into_trancl 1);
41.94 by (rtac subset_refl 1);
41.95 val wfrec = result();
41.96 @@ -253,10 +247,3 @@
41.97 by (REPEAT (ares_tac (prems@[lam_type]) 1
41.98 ORELSE eresolve_tac [spec RS mp, underD] 1));
41.99 val wfrec_type = result();
41.100 -
41.101 -val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
41.102 - "[| r=r'; !!x u. H(x,u)=H'(x,u); a=a' |] \
41.103 -\ ==> wfrec(r,a,H)=wfrec(r',a',H')";
41.104 -by (EVERY1 (map rtac (prems RL [subst])));
41.105 -by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
41.106 -val wfrec_cong = result();
42.1 --- a/src/ZF/zf.ML Fri Sep 17 12:53:53 1993 +0200
42.2 +++ b/src/ZF/zf.ML Fri Sep 17 16:16:38 1993 +0200
42.3 @@ -13,9 +13,8 @@
42.4 val ballE : thm
42.5 val ballI : thm
42.6 val ball_cong : thm
42.7 - val ball_rew : thm
42.8 + val ball_simp : thm
42.9 val ball_tac : int -> tactic
42.10 - val basic_ZF_congs : thm list
42.11 val bexCI : thm
42.12 val bexE : thm
42.13 val bexI : thm
42.14 @@ -45,7 +44,6 @@
42.15 val lemmas_cs : claset
42.16 val PowD : thm
42.17 val PowI : thm
42.18 - val prove_cong_tac : thm list -> int -> tactic
42.19 val RepFunE : thm
42.20 val RepFunI : thm
42.21 val RepFun_eqI : thm
42.22 @@ -75,14 +73,6 @@
42.23 structure ZF_Lemmas : ZF_LEMMAS =
42.24 struct
42.25
42.26 -val basic_ZF_congs = mk_congs ZF.thy
42.27 - ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :",
42.28 - "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
42.29 - "domain", "range", "restrict"];
42.30 -
42.31 -fun prove_cong_tac prems i =
42.32 - REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
42.33 -
42.34 (*** Bounded universal quantifier ***)
42.35
42.36 val ballI = prove_goalw ZF.thy [Ball_def]
42.37 @@ -118,14 +108,13 @@
42.38 val ball_tac = dtac bspec THEN' assume_tac;
42.39
42.40 (*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
42.41 -val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
42.42 - (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
42.43 +val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
42.44 + (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
42.45
42.46 (*Congruence rule for rewriting*)
42.47 val ball_cong = prove_goalw ZF.thy [Ball_def]
42.48 - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
42.49 -\ |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
42.50 - (fn prems=> [ (prove_cong_tac prems 1) ]);
42.51 + "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
42.52 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
42.53
42.54 (*** Bounded existential quantifier ***)
42.55
42.56 @@ -151,8 +140,8 @@
42.57
42.58 val bex_cong = prove_goalw ZF.thy [Bex_def]
42.59 "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
42.60 -\ |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
42.61 - (fn prems=> [ (prove_cong_tac prems 1) ]);
42.62 +\ |] ==> Bex(A,P) <-> Bex(A',P')"
42.63 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
42.64
42.65 (*** Rules for subsets ***)
42.66
42.67 @@ -265,7 +254,7 @@
42.68
42.69 val Replace_cong = prove_goal ZF.thy
42.70 "[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
42.71 -\ {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
42.72 +\ Replace(A,P) = Replace(B,Q)"
42.73 (fn prems=>
42.74 let val substprems = prems RL [subst, ssubst]
42.75 and iffprems = prems RL [iffD1,iffD2]
42.76 @@ -275,7 +264,6 @@
42.77 ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
42.78 end);
42.79
42.80 -
42.81 (*** Rules for RepFun ***)
42.82
42.83 val RepFunI = prove_goalw ZF.thy [RepFun_def]
42.84 @@ -296,9 +284,8 @@
42.85 (REPEAT (ares_tac prems 1)) ]);
42.86
42.87 val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
42.88 - "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> \
42.89 -\ {f(x). x:A} = {g(x). x:B}"
42.90 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
42.91 + "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
42.92 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
42.93
42.94
42.95 (*** Rules for Collect -- forming a subset by separation ***)
42.96 @@ -332,9 +319,8 @@
42.97 (assume_tac 1) ]);
42.98
42.99 val Collect_cong = prove_goalw ZF.thy [Collect_def]
42.100 - "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> \
42.101 -\ {x:A. P(x)} = {x:B. Q(x)}"
42.102 - (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
42.103 + "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
42.104 + (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
42.105
42.106 (*** Rules for Unions ***)
42.107