Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
particularly delicate. There is a variable renaming problem in
ramsey.ML/pigeon2_lemma. In some cases, rewriting by typechecking rules
had to be replaced by setsolver type_auto_tac... because only the solver
can instantiate variables.
1.1 --- a/src/ZF/ex/BT_Fn.ML Fri Sep 17 16:16:38 1993 +0200
1.2 +++ b/src/ZF/ex/BT_Fn.ML Fri Sep 17 16:52:10 1993 +0200
1.3 @@ -12,28 +12,24 @@
1.4
1.5 (** bt_rec -- by Vset recursion **)
1.6
1.7 -(*Used to verify bt_rec*)
1.8 -val bt_rec_ss = ZF_ss
1.9 - addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")])
1.10 - addrews BT.case_eqns;
1.11 -
1.12 goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))";
1.13 -by (SIMP_TAC rank_ss 1);
1.14 +by (simp_tac rank_ss 1);
1.15 val rank_Br1 = result();
1.16
1.17 goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))";
1.18 -by (SIMP_TAC rank_ss 1);
1.19 +by (simp_tac rank_ss 1);
1.20 val rank_Br2 = result();
1.21
1.22 goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
1.23 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
1.24 -by (SIMP_TAC bt_rec_ss 1);
1.25 +by (simp_tac (ZF_ss addsimps BT.case_eqns) 1);
1.26 val bt_rec_Lf = result();
1.27
1.28 goal BT_Fn.thy
1.29 "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
1.30 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
1.31 -by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1);
1.32 +by (simp_tac (ZF_ss addsimps
1.33 + (BT.case_eqns @ [Vset_rankI, rank_Br1, rank_Br2])) 1);
1.34 val bt_rec_Br = result();
1.35
1.36 (*Type checking -- proved by induction, as usual*)
1.37 @@ -44,7 +40,7 @@
1.38 \ h(x,y,z,r,s): C(Br(x,y,z)) \
1.39 \ |] ==> bt_rec(t,c,h) : C(t)";
1.40 by (bt_ind_tac "t" prems 1);
1.41 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
1.42 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
1.43 (prems@[bt_rec_Lf,bt_rec_Br]))));
1.44 val bt_rec_type = result();
1.45
1.46 @@ -98,15 +94,10 @@
1.47 val bt_typechecks =
1.48 [LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
1.49
1.50 -val bt_congs =
1.51 - BT.congs @
1.52 - mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"];
1.53 -
1.54 val bt_ss = arith_ss
1.55 - addcongs bt_congs
1.56 - addrews BT.case_eqns
1.57 - addrews bt_typechecks
1.58 - addrews [bt_rec_Lf, bt_rec_Br,
1.59 + addsimps BT.case_eqns
1.60 + addsimps bt_typechecks
1.61 + addsimps [bt_rec_Lf, bt_rec_Br,
1.62 n_nodes_Lf, n_nodes_Br,
1.63 n_leaves_Lf, n_leaves_Br,
1.64 bt_reflect_Lf, bt_reflect_Br];
1.65 @@ -117,14 +108,14 @@
1.66 val prems = goal BT_Fn.thy
1.67 "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
1.68 by (bt_ind_tac "t" prems 1);
1.69 -by (ALLGOALS (ASM_SIMP_TAC bt_ss));
1.70 +by (ALLGOALS (asm_simp_tac bt_ss));
1.71 by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
1.72 val n_leaves_reflect = result();
1.73
1.74 val prems = goal BT_Fn.thy
1.75 "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
1.76 by (bt_ind_tac "t" prems 1);
1.77 -by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right])));
1.78 +by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
1.79 val n_leaves_nodes = result();
1.80
1.81 (*** theorems about bt_reflect ***)
1.82 @@ -132,7 +123,7 @@
1.83 val prems = goal BT_Fn.thy
1.84 "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
1.85 by (bt_ind_tac "t" prems 1);
1.86 -by (ALLGOALS (ASM_SIMP_TAC bt_ss));
1.87 +by (ALLGOALS (asm_simp_tac bt_ss));
1.88 val bt_reflect_bt_reflect_ident = result();
1.89
1.90
2.1 --- a/src/ZF/ex/BinFn.ML Fri Sep 17 16:16:38 1993 +0200
2.2 +++ b/src/ZF/ex/BinFn.ML Fri Sep 17 16:52:10 1993 +0200
2.3 @@ -14,20 +14,19 @@
2.4 goal BinFn.thy "bin_rec(Plus,a,b,h) = a";
2.5 by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
2.6 by (rewrite_goals_tac Bin.con_defs);
2.7 -by (SIMP_TAC rank_ss 1);
2.8 +by (simp_tac rank_ss 1);
2.9 val bin_rec_Plus = result();
2.10
2.11 goal BinFn.thy "bin_rec(Minus,a,b,h) = b";
2.12 by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
2.13 by (rewrite_goals_tac Bin.con_defs);
2.14 -by (SIMP_TAC rank_ss 1);
2.15 +by (simp_tac rank_ss 1);
2.16 val bin_rec_Minus = result();
2.17
2.18 goal BinFn.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
2.19 by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
2.20 by (rewrite_goals_tac Bin.con_defs);
2.21 -by (SIMP_TAC (rank_ss addcongs
2.22 - (mk_typed_congs BinFn.thy [("h", "[i,i,i]=>i")])) 1);
2.23 +by (simp_tac rank_ss 1);
2.24 val bin_rec_Bcons = result();
2.25
2.26 (*Type checking*)
2.27 @@ -38,7 +37,7 @@
2.28 \ |] ==> bin_rec(w,a,b,h) : C(w)";
2.29 by (bin_ind_tac "w" prems 1);
2.30 by (ALLGOALS
2.31 - (ASM_SIMP_TAC (ZF_ss addrews (prems@[bin_rec_Plus,bin_rec_Minus,
2.32 + (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
2.33 bin_rec_Bcons]))));
2.34 val bin_rec_type = result();
2.35
2.36 @@ -106,13 +105,8 @@
2.37 [integ_of_bin_type, bin_succ_type, bin_pred_type,
2.38 bin_minus_type, bin_add_type, bin_mult_type];
2.39
2.40 -val bin_congs = mk_congs BinFn.thy
2.41 - ["bin_rec","op $$","integ_of_bin","bin_succ","bin_pred",
2.42 - "bin_minus","bin_add","bin_mult"];
2.43 -
2.44 val bin_ss = integ_ss
2.45 - addcongs (bin_congs@bool_congs)
2.46 - addrews([bool_1I, bool_0I,
2.47 + addsimps([bool_1I, bool_0I,
2.48 bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
2.49 bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
2.50
2.51 @@ -127,7 +121,7 @@
2.52 "!!z v. [| z $+ v = z' $+ v'; \
2.53 \ z: integ; z': integ; v: integ; v': integ; w: integ |] \
2.54 \ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
2.55 -by (ASM_SIMP_TAC (integ_ss addrews ([zadd_assoc RS sym])) 1);
2.56 +by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
2.57 val zadd_assoc_cong = result();
2.58
2.59 goal Integ.thy
2.60 @@ -136,7 +130,8 @@
2.61 by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
2.62 val zadd_assoc_swap = result();
2.63
2.64 -val [zadd_cong] = mk_congs Integ.thy ["op $+"];
2.65 +val zadd_cong =
2.66 + read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2;
2.67
2.68 val zadd_kill = (refl RS zadd_cong);
2.69 val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
2.70 @@ -151,28 +146,28 @@
2.71 val zadd_swap_pairs = result();
2.72
2.73
2.74 -val carry_ss = bin_ss addrews
2.75 +val carry_ss = bin_ss addsimps
2.76 (bin_recs bin_succ_def @ bin_recs bin_pred_def);
2.77
2.78 goal BinFn.thy
2.79 "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
2.80 by (etac Bin.induct 1);
2.81 -by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
2.82 -by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
2.83 +by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
2.84 +by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
2.85 by (etac boolE 1);
2.86 -by (ALLGOALS (ASM_SIMP_TAC (carry_ss addrews [zadd_assoc])));
2.87 +by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc])));
2.88 by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
2.89 val integ_of_bin_succ = result();
2.90
2.91 goal BinFn.thy
2.92 "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
2.93 by (etac Bin.induct 1);
2.94 -by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
2.95 -by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
2.96 +by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
2.97 +by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
2.98 by (etac boolE 1);
2.99 by (ALLGOALS
2.100 - (ASM_SIMP_TAC
2.101 - (carry_ss addrews [zadd_assoc RS sym,
2.102 + (asm_simp_tac
2.103 + (carry_ss addsimps [zadd_assoc RS sym,
2.104 zadd_zminus_inverse, zadd_zminus_inverse2])));
2.105 by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
2.106 val integ_of_bin_pred = result();
2.107 @@ -183,68 +178,68 @@
2.108 (*** bin_minus: (unary!) negation of binary integers ***)
2.109
2.110 val bin_minus_ss =
2.111 - bin_ss addrews (bin_recs bin_minus_def @
2.112 + bin_ss addsimps (bin_recs bin_minus_def @
2.113 [integ_of_bin_succ, integ_of_bin_pred]);
2.114
2.115 goal BinFn.thy
2.116 "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
2.117 by (etac Bin.induct 1);
2.118 -by (SIMP_TAC (bin_minus_ss addrews [zminus_0]) 1);
2.119 -by (SIMP_TAC (bin_minus_ss addrews [zadd_0_right]) 1);
2.120 +by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1);
2.121 +by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1);
2.122 by (etac boolE 1);
2.123 by (ALLGOALS
2.124 - (ASM_SIMP_TAC (bin_minus_ss addrews [zminus_zadd_distrib, zadd_assoc])));
2.125 + (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
2.126 val integ_of_bin_minus = result();
2.127
2.128
2.129 (*** bin_add: binary addition ***)
2.130
2.131 goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
2.132 -by (ASM_SIMP_TAC bin_ss 1);
2.133 +by (asm_simp_tac bin_ss 1);
2.134 val bin_add_Plus = result();
2.135
2.136 goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
2.137 -by (ASM_SIMP_TAC bin_ss 1);
2.138 +by (asm_simp_tac bin_ss 1);
2.139 val bin_add_Minus = result();
2.140
2.141 goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
2.142 -by (SIMP_TAC bin_ss 1);
2.143 +by (simp_tac bin_ss 1);
2.144 val bin_add_Bcons_Plus = result();
2.145
2.146 goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
2.147 -by (SIMP_TAC bin_ss 1);
2.148 +by (simp_tac bin_ss 1);
2.149 val bin_add_Bcons_Minus = result();
2.150
2.151 goalw BinFn.thy [bin_add_def]
2.152 "!!w y. [| w: bin; y: bool |] ==> \
2.153 \ bin_add(v$$x, w$$y) = \
2.154 \ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
2.155 -by (ASM_SIMP_TAC bin_ss 1);
2.156 +by (asm_simp_tac bin_ss 1);
2.157 val bin_add_Bcons_Bcons = result();
2.158
2.159 val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
2.160 bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
2.161 integ_of_bin_succ, integ_of_bin_pred];
2.162
2.163 -val bin_add_ss = bin_ss addrews ([bool_subset_nat RS subsetD] @ bin_add_rews);
2.164 +val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews);
2.165
2.166 goal BinFn.thy
2.167 "!!v. v: bin ==> \
2.168 \ ALL w: bin. integ_of_bin(bin_add(v,w)) = \
2.169 \ integ_of_bin(v) $+ integ_of_bin(w)";
2.170 by (etac Bin.induct 1);
2.171 -by (SIMP_TAC bin_add_ss 1);
2.172 -by (SIMP_TAC bin_add_ss 1);
2.173 +by (simp_tac bin_add_ss 1);
2.174 +by (simp_tac bin_add_ss 1);
2.175 by (rtac ballI 1);
2.176 by (bin_ind_tac "wa" [] 1);
2.177 -by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_0_right]) 1);
2.178 -by (ASM_SIMP_TAC bin_add_ss 1);
2.179 +by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1);
2.180 +by (asm_simp_tac bin_add_ss 1);
2.181 by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
2.182 by (etac boolE 1);
2.183 -by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc, zadd_swap_pairs]) 2);
2.184 +by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2);
2.185 by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
2.186 by (etac boolE 1);
2.187 -by (ALLGOALS (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc,zadd_swap_pairs])));
2.188 +by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
2.189 by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
2.190 typechecks) 1));
2.191 val integ_of_bin_add_lemma = result();
2.192 @@ -255,7 +250,7 @@
2.193 (*** bin_add: binary multiplication ***)
2.194
2.195 val bin_mult_ss =
2.196 - bin_ss addrews (bin_recs bin_mult_def @
2.197 + bin_ss addsimps (bin_recs bin_mult_def @
2.198 [integ_of_bin_minus, integ_of_bin_add]);
2.199
2.200
2.201 @@ -265,12 +260,12 @@
2.202 \ integ_of_bin(v) $* integ_of_bin(w)";
2.203 by (cut_facts_tac prems 1);
2.204 by (bin_ind_tac "v" [major] 1);
2.205 -by (SIMP_TAC (bin_mult_ss addrews [zmult_0]) 1);
2.206 -by (SIMP_TAC (bin_mult_ss addrews [zmult_1,zmult_zminus]) 1);
2.207 +by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1);
2.208 +by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1);
2.209 by (etac boolE 1);
2.210 -by (ASM_SIMP_TAC (bin_mult_ss addrews [zadd_zmult_distrib]) 2);
2.211 -by (ASM_SIMP_TAC
2.212 - (bin_mult_ss addrews [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
2.213 +by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2);
2.214 +by (asm_simp_tac
2.215 + (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
2.216 by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
2.217 typechecks) 1));
2.218 val integ_of_bin_mult = result();
2.219 @@ -283,19 +278,19 @@
2.220 val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
2.221
2.222 goal BinFn.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
2.223 -by (SIMP_TAC carry_ss 1);
2.224 +by (simp_tac carry_ss 1);
2.225 val bin_succ_Bcons1 = result();
2.226
2.227 goal BinFn.thy "bin_succ(w$$0) = w$$1";
2.228 -by (SIMP_TAC carry_ss 1);
2.229 +by (simp_tac carry_ss 1);
2.230 val bin_succ_Bcons0 = result();
2.231
2.232 goal BinFn.thy "bin_pred(w$$1) = w$$0";
2.233 -by (SIMP_TAC carry_ss 1);
2.234 +by (simp_tac carry_ss 1);
2.235 val bin_pred_Bcons1 = result();
2.236
2.237 goal BinFn.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
2.238 -by (SIMP_TAC carry_ss 1);
2.239 +by (simp_tac carry_ss 1);
2.240 val bin_pred_Bcons0 = result();
2.241
2.242 (** extra rules for bin_minus **)
2.243 @@ -303,28 +298,28 @@
2.244 val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
2.245
2.246 goal BinFn.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
2.247 -by (SIMP_TAC bin_minus_ss 1);
2.248 +by (simp_tac bin_minus_ss 1);
2.249 val bin_minus_Bcons1 = result();
2.250
2.251 goal BinFn.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
2.252 -by (SIMP_TAC bin_minus_ss 1);
2.253 +by (simp_tac bin_minus_ss 1);
2.254 val bin_minus_Bcons0 = result();
2.255
2.256 (** extra rules for bin_add **)
2.257
2.258 goal BinFn.thy
2.259 "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
2.260 -by (ASM_SIMP_TAC bin_add_ss 1);
2.261 +by (asm_simp_tac bin_add_ss 1);
2.262 val bin_add_Bcons_Bcons11 = result();
2.263
2.264 goal BinFn.thy
2.265 "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
2.266 -by (ASM_SIMP_TAC bin_add_ss 1);
2.267 +by (asm_simp_tac bin_add_ss 1);
2.268 val bin_add_Bcons_Bcons10 = result();
2.269
2.270 goal BinFn.thy
2.271 "!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
2.272 -by (ASM_SIMP_TAC bin_add_ss 1);
2.273 +by (asm_simp_tac bin_add_ss 1);
2.274 val bin_add_Bcons_Bcons0 = result();
2.275
2.276 (** extra rules for bin_mult **)
2.277 @@ -332,24 +327,18 @@
2.278 val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
2.279
2.280 goal BinFn.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
2.281 -by (SIMP_TAC bin_mult_ss 1);
2.282 +by (simp_tac bin_mult_ss 1);
2.283 val bin_mult_Bcons1 = result();
2.284
2.285 goal BinFn.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
2.286 -by (SIMP_TAC bin_mult_ss 1);
2.287 +by (simp_tac bin_mult_ss 1);
2.288 val bin_mult_Bcons0 = result();
2.289
2.290
2.291 (*** The computation simpset ***)
2.292
2.293 -val bin_comp_ss = carry_ss addrews
2.294 - [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, bin_add_Bcons_Minus,
2.295 - bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11]
2.296 - setauto (type_auto_tac bin_typechecks0);
2.297 -
2.298 val bin_comp_ss = integ_ss
2.299 - addcongs bin_congs
2.300 - addrews [bin_succ_Plus, bin_succ_Minus,
2.301 + addsimps [bin_succ_Plus, bin_succ_Minus,
2.302 bin_succ_Bcons1, bin_succ_Bcons0,
2.303 bin_pred_Plus, bin_pred_Minus,
2.304 bin_pred_Bcons1, bin_pred_Bcons0,
2.305 @@ -360,7 +349,7 @@
2.306 bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
2.307 bin_mult_Plus, bin_mult_Minus,
2.308 bin_mult_Bcons1, bin_mult_Bcons0]
2.309 - setauto (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
2.310 + setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
2.311
2.312 (*** Examples of performing binary arithmetic by simplification ***)
2.313
2.314 @@ -370,7 +359,7 @@
2.315 (* 13+19 = 32 *)
2.316 goal BinFn.thy
2.317 "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
2.318 -by (SIMP_TAC bin_comp_ss 1); (*1.9 secs*)
2.319 +by (simp_tac bin_comp_ss 1); (*0.6 secs*)
2.320 result();
2.321
2.322 bin_add(binary_of_int 13, binary_of_int 19);
2.323 @@ -380,7 +369,7 @@
2.324 "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
2.325 \ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
2.326 \ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
2.327 -by (SIMP_TAC bin_comp_ss 1); (*8.9 secs*)
2.328 +by (simp_tac bin_comp_ss 1); (*2.6 secs*)
2.329 result();
2.330
2.331 bin_add(binary_of_int 1234, binary_of_int 5678);
2.332 @@ -390,7 +379,7 @@
2.333 "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
2.334 \ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
2.335 \ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
2.336 -by (SIMP_TAC bin_comp_ss 1); (*7.4 secs*)
2.337 +by (simp_tac bin_comp_ss 1); (*2.3 secs*)
2.338 result();
2.339
2.340 bin_add(binary_of_int 1359, binary_of_int ~2468);
2.341 @@ -400,7 +389,7 @@
2.342 "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
2.343 \ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
2.344 \ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
2.345 -by (SIMP_TAC bin_comp_ss 1); (*13.7 secs*)
2.346 +by (simp_tac bin_comp_ss 1); (*3.9 secs*)
2.347 result();
2.348
2.349 bin_add(binary_of_int 93746, binary_of_int ~46375);
2.350 @@ -409,7 +398,7 @@
2.351 goal BinFn.thy
2.352 "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
2.353 \ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
2.354 -by (SIMP_TAC bin_comp_ss 1); (*2.8 secs*)
2.355 +by (simp_tac bin_comp_ss 1); (*0.6 secs*)
2.356 result();
2.357
2.358 bin_minus(binary_of_int 65745);
2.359 @@ -418,7 +407,7 @@
2.360 goal BinFn.thy
2.361 "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
2.362 \ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
2.363 -by (SIMP_TAC bin_comp_ss 1); (*3.3 secs*)
2.364 +by (simp_tac bin_comp_ss 1); (*0.7 secs*)
2.365 result();
2.366
2.367 bin_minus(binary_of_int ~54321);
2.368 @@ -426,7 +415,7 @@
2.369 (* 13*19 = 247 *)
2.370 goal BinFn.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
2.371 \ Plus$$1$$1$$1$$1$$0$$1$$1$$1";
2.372 -by (SIMP_TAC bin_comp_ss 1); (*4.4 secs*)
2.373 +by (simp_tac bin_comp_ss 1); (*1.5 secs*)
2.374 result();
2.375
2.376 bin_mult(binary_of_int 13, binary_of_int 19);
2.377 @@ -435,7 +424,7 @@
2.378 goal BinFn.thy
2.379 "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
2.380 \ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
2.381 -by (SIMP_TAC bin_comp_ss 1); (*9.2 secs*)
2.382 +by (simp_tac bin_comp_ss 1); (*2.6 secs*)
2.383 result();
2.384
2.385 bin_mult(binary_of_int ~84, binary_of_int 51);
2.386 @@ -445,19 +434,17 @@
2.387 "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
2.388 \ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
2.389 \ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
2.390 -by (SIMP_TAC bin_comp_ss 1); (*38.4 secs*)
2.391 +by (simp_tac bin_comp_ss 1); (*9.8 secs*)
2.392 result();
2.393
2.394 bin_mult(binary_of_int 255, binary_of_int 255);
2.395
2.396 -(***************** TOO SLOW TO INCLUDE IN TEST RUNS
2.397 (* 1359 * ~2468 = ~3354012 *)
2.398 goal BinFn.thy
2.399 "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
2.400 \ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
2.401 \ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
2.402 -by (SIMP_TAC bin_comp_ss 1); (*54.8 secs*)
2.403 +by (simp_tac bin_comp_ss 1); (*13.7 secs*)
2.404 result();
2.405 -****************)
2.406
2.407 bin_mult(binary_of_int 1359, binary_of_int ~2468);
3.1 --- a/src/ZF/ex/Enum.ML Fri Sep 17 16:16:38 1993 +0200
3.2 +++ b/src/ZF/ex/Enum.ML Fri Sep 17 16:52:10 1993 +0200
3.3 @@ -28,6 +28,6 @@
3.4 val type_elims = []);
3.5
3.6 goal Enum.thy "~ con59=con60";
3.7 -by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1); (*2.3 secs*)
3.8 +by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*)
3.9 result();
3.10
4.1 --- a/src/ZF/ex/Equiv.ML Fri Sep 17 16:16:38 1993 +0200
4.2 +++ b/src/ZF/ex/Equiv.ML Fri Sep 17 16:52:10 1993 +0200
4.3 @@ -190,7 +190,7 @@
4.4 by (safe_tac ZF_cs);
4.5 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
4.6 by (assume_tac 1);
4.7 -by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
4.8 +by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
4.9 congruent2_implies_congruent]) 1);
4.10 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
4.11 by (fast_tac ZF_cs 1);
4.12 @@ -200,7 +200,7 @@
4.13 "[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \
4.14 \ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
4.15 by (cut_facts_tac prems 1);
4.16 -by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
4.17 +by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
4.18 congruent2_implies_congruent,
4.19 congruent2_implies_congruent_UN]) 1);
4.20 val UN_equiv_class2 = result();
4.21 @@ -235,7 +235,7 @@
4.22
4.23 val [equivA,commute,congt] = goal Equiv.thy
4.24 "[| equiv(A,r); \
4.25 -\ !! y z w. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
4.26 +\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
4.27 \ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
4.28 \ |] ==> congruent2(r,b)";
4.29 by (resolve_tac [equivA RS congruent2I] 1);
4.30 @@ -259,7 +259,7 @@
4.31 by (safe_tac ZF_cs);
4.32 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
4.33 by (assume_tac 1);
4.34 -by (ASM_SIMP_TAC (ZF_ss addrews [congt RS (equivA RS UN_equiv_class)]) 1);
4.35 +by (asm_simp_tac (ZF_ss addsimps [congt RS (equivA RS UN_equiv_class)]) 1);
4.36 by (rtac (commute RS trans) 1);
4.37 by (rtac (commute RS trans RS sym) 3);
4.38 by (rtac sym 5);
5.1 --- a/src/ZF/ex/Integ.ML Fri Sep 17 16:16:38 1993 +0200
5.2 +++ b/src/ZF/ex/Integ.ML Fri Sep 17 16:52:10 1993 +0200
5.3 @@ -12,16 +12,18 @@
5.4 $+ and $* are monotonic wrt $<
5.5 *)
5.6
5.7 +val add_cong =
5.8 + read_instantiate_sg (sign_of Arith.thy) [("t","op #+")] subst_context2;
5.9 +
5.10 +
5.11 open Integ;
5.12
5.13 -val [add_cong] = mk_congs Arith.thy ["op #+"];
5.14 -
5.15 (*** Proving that intrel is an equivalence relation ***)
5.16
5.17 val prems = goal Arith.thy
5.18 "[| m #+ n = m' #+ n'; m: nat; m': nat |] \
5.19 \ ==> m #+ (n #+ k) = m' #+ (n' #+ k)";
5.20 -by (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym] @ prems)) 1);
5.21 +by (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym] @ prems)) 1);
5.22 val add_assoc_cong = result();
5.23
5.24 val prems = goal Arith.thy
5.25 @@ -31,6 +33,7 @@
5.26 val add_assoc_swap = result();
5.27
5.28 val add_kill = (refl RS add_cong);
5.29 +
5.30 val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans);
5.31
5.32 (*By luck, requires no typing premises for y1, y2,y3*)
5.33 @@ -90,22 +93,17 @@
5.34 val equiv_intrel = result();
5.35
5.36
5.37 -val integ_congs = mk_congs Integ.thy
5.38 - ["znat", "zminus", "znegative", "zmagnitude", "op $+", "op $-", "op $*"];
5.39 +val intrel_ss =
5.40 + arith_ss addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
5.41
5.42 -val intrel_ss0 = arith_ss addcongs integ_congs;
5.43 -
5.44 -val intrel_ss =
5.45 - intrel_ss0 addrews [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
5.46 -
5.47 -(*More than twice as fast as simplifying with intrel_ss*)
5.48 +(*Roughly twice as fast as simplifying with intrel_ss*)
5.49 fun INTEG_SIMP_TAC ths =
5.50 - let val ss = intrel_ss0 addrews ths
5.51 + let val ss = arith_ss addsimps ths
5.52 in fn i =>
5.53 - EVERY [ASM_SIMP_TAC ss i,
5.54 + EVERY [asm_simp_tac ss i,
5.55 rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i,
5.56 typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks),
5.57 - ASM_SIMP_TAC ss i]
5.58 + asm_simp_tac ss i]
5.59 end;
5.60
5.61
5.62 @@ -130,7 +128,7 @@
5.63 goalw Integ.thy [congruent_def]
5.64 "congruent(intrel, split(%x y. intrel``{<y,x>}))";
5.65 by (safe_tac intrel_cs);
5.66 -by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
5.67 +by (ALLGOALS (asm_simp_tac intrel_ss));
5.68 by (etac (box_equals RS sym) 1);
5.69 by (REPEAT (ares_tac [add_commute] 1));
5.70 val zminus_congruent = result();
5.71 @@ -150,7 +148,7 @@
5.72 by (REPEAT (ares_tac prems 1));
5.73 by (REPEAT (etac SigmaE 1));
5.74 by (etac rev_mp 1);
5.75 -by (ASM_SIMP_TAC ZF_ss 1);
5.76 +by (asm_simp_tac ZF_ss 1);
5.77 by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel]
5.78 addSEs [box_equals RS sym, add_commute,
5.79 make_elim eq_equiv_class]) 1);
5.80 @@ -158,17 +156,17 @@
5.81
5.82 val prems = goalw Integ.thy [zminus_def]
5.83 "[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
5.84 -by (ASM_SIMP_TAC
5.85 - (ZF_ss addrews (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
5.86 +by (asm_simp_tac
5.87 + (ZF_ss addsimps (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
5.88 val zminus = result();
5.89
5.90 goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z";
5.91 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.92 -by (ASM_SIMP_TAC (ZF_ss addrews [zminus] addcongs integ_congs) 1);
5.93 +by (asm_simp_tac (ZF_ss addsimps [zminus]) 1);
5.94 val zminus_zminus = result();
5.95
5.96 goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0";
5.97 -by (SIMP_TAC (arith_ss addrews [zminus]) 1);
5.98 +by (simp_tac (arith_ss addsimps [zminus]) 1);
5.99 val zminus_0 = result();
5.100
5.101
5.102 @@ -179,13 +177,13 @@
5.103 by (safe_tac intrel_cs);
5.104 by (rtac (add_not_less_self RS notE) 1);
5.105 by (etac ssubst 3);
5.106 -by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 3);
5.107 +by (asm_simp_tac (arith_ss addsimps [add_0_right]) 3);
5.108 by (REPEAT (assume_tac 1));
5.109 val not_znegative_znat = result();
5.110
5.111 val [nnat] = goalw Integ.thy [znegative_def, znat_def]
5.112 "n: nat ==> znegative($~ $# succ(n))";
5.113 -by (SIMP_TAC (intrel_ss addrews [zminus,nnat]) 1);
5.114 +by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
5.115 by (REPEAT
5.116 (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
5.117 refl RS intrelI RS imageI, consI1, nnat, nat_0I,
5.118 @@ -198,19 +196,19 @@
5.119 goalw Integ.thy [congruent_def]
5.120 "congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))";
5.121 by (safe_tac intrel_cs);
5.122 -by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
5.123 +by (ALLGOALS (asm_simp_tac intrel_ss));
5.124 by (etac rev_mp 1);
5.125 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
5.126 by (REPEAT (assume_tac 1));
5.127 -by (ASM_SIMP_TAC (arith_ss addrews [add_succ_right,succ_inject_iff]) 3);
5.128 -by (ASM_SIMP_TAC
5.129 - (arith_ss addrews [diff_add_inverse,diff_add_0,add_0_right]) 2);
5.130 -by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 1);
5.131 +by (asm_simp_tac (arith_ss addsimps [add_succ_right,succ_inject_iff]) 3);
5.132 +by (asm_simp_tac
5.133 + (arith_ss addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2);
5.134 +by (asm_simp_tac (arith_ss addsimps [add_0_right]) 1);
5.135 by (rtac impI 1);
5.136 by (etac subst 1);
5.137 by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
5.138 by (REPEAT (assume_tac 1));
5.139 -by (ASM_SIMP_TAC (arith_ss addrews [diff_add_inverse,diff_add_0]) 1);
5.140 +by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
5.141 val zmagnitude_congruent = result();
5.142
5.143 (*Resolve th against the corresponding facts for zmagnitude*)
5.144 @@ -225,18 +223,18 @@
5.145 val prems = goalw Integ.thy [zmagnitude_def]
5.146 "[| x: nat; y: nat |] ==> \
5.147 \ zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)";
5.148 -by (ASM_SIMP_TAC
5.149 - (ZF_ss addrews (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
5.150 +by (asm_simp_tac
5.151 + (ZF_ss addsimps (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
5.152 val zmagnitude = result();
5.153
5.154 val [nnat] = goalw Integ.thy [znat_def]
5.155 "n: nat ==> zmagnitude($# n) = n";
5.156 -by (SIMP_TAC (intrel_ss addrews [zmagnitude,nnat]) 1);
5.157 +by (simp_tac (intrel_ss addsimps [zmagnitude,nnat]) 1);
5.158 val zmagnitude_znat = result();
5.159
5.160 val [nnat] = goalw Integ.thy [znat_def]
5.161 "n: nat ==> zmagnitude($~ $# n) = n";
5.162 -by (SIMP_TAC (intrel_ss addrews [zmagnitude,zminus,nnat,add_0_right]) 1);
5.163 +by (simp_tac (intrel_ss addsimps [zmagnitude,zminus,nnat,add_0_right]) 1);
5.164 val zmagnitude_zminus_znat = result();
5.165
5.166
5.167 @@ -254,7 +252,7 @@
5.168 by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1);
5.169 by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3);
5.170 by (typechk_tac [add_type]);
5.171 -by (ASM_SIMP_TAC (arith_ss addrews [add_assoc RS sym]) 1);
5.172 +by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
5.173 val zadd_congruent2 = result();
5.174
5.175 (*Resolve th against the corresponding facts for zadd*)
5.176 @@ -269,19 +267,19 @@
5.177 val prems = goalw Integ.thy [zadd_def]
5.178 "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
5.179 \ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = intrel `` {<x1#+x2, y1#+y2>}";
5.180 -by (ASM_SIMP_TAC (ZF_ss addrews
5.181 +by (asm_simp_tac (ZF_ss addsimps
5.182 (prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1);
5.183 val zadd = result();
5.184
5.185 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";
5.186 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.187 -by (ASM_SIMP_TAC (arith_ss addrews [zadd]) 1);
5.188 +by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
5.189 val zadd_0 = result();
5.190
5.191 goalw Integ.thy [integ_def]
5.192 "!!z w. [| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
5.193 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.194 -by (ASM_SIMP_TAC (arith_ss addrews [zminus,zadd] addcongs integ_congs) 1);
5.195 +by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
5.196 val zminus_zadd_distrib = result();
5.197
5.198 goalw Integ.thy [integ_def]
5.199 @@ -296,17 +294,17 @@
5.200 \ (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
5.201 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.202 (*rewriting is much faster without intrel_iff, etc.*)
5.203 -by (ASM_SIMP_TAC (intrel_ss0 addrews [zadd,add_assoc]) 1);
5.204 +by (asm_simp_tac (arith_ss addsimps [zadd,add_assoc]) 1);
5.205 val zadd_assoc = result();
5.206
5.207 val prems = goalw Integ.thy [znat_def]
5.208 "[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
5.209 -by (ASM_SIMP_TAC (arith_ss addrews (zadd::prems)) 1);
5.210 +by (asm_simp_tac (arith_ss addsimps (zadd::prems)) 1);
5.211 val znat_add = result();
5.212
5.213 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0";
5.214 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.215 -by (ASM_SIMP_TAC (intrel_ss addrews [zminus,zadd,add_0_right]) 1);
5.216 +by (asm_simp_tac (intrel_ss addsimps [zminus,zadd,add_0_right]) 1);
5.217 by (REPEAT (ares_tac [add_commute] 1));
5.218 val zadd_zminus_inverse = result();
5.219
5.220 @@ -334,7 +332,7 @@
5.221 "[| k: nat; l: nat; m: nat; n: nat |] ==> \
5.222 \ (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)";
5.223 val add_commute' = read_instantiate [("m","l")] add_commute;
5.224 -by (SIMP_TAC (arith_ss addrews ([add_commute',add_assoc]@prems)) 1);
5.225 +by (simp_tac (arith_ss addsimps ([add_commute',add_assoc]@prems)) 1);
5.226 val zmult_congruent_lemma = result();
5.227
5.228 goal Integ.thy
5.229 @@ -348,7 +346,7 @@
5.230 by (rtac (zmult_congruent_lemma RS trans) 2);
5.231 by (rtac (zmult_congruent_lemma RS trans RS sym) 6);
5.232 by (typechk_tac [mult_type]);
5.233 -by (ASM_SIMP_TAC (arith_ss addrews [add_mult_distrib_left RS sym]) 2);
5.234 +by (asm_simp_tac (arith_ss addsimps [add_mult_distrib_left RS sym]) 2);
5.235 (*Proof that zmult is commutative on representatives*)
5.236 by (rtac add_cong 1);
5.237 by (rtac (add_commute RS trans) 2);
5.238 @@ -370,19 +368,19 @@
5.239 "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
5.240 \ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
5.241 \ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
5.242 -by (ASM_SIMP_TAC (ZF_ss addrews
5.243 +by (asm_simp_tac (ZF_ss addsimps
5.244 (prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1);
5.245 val zmult = result();
5.246
5.247 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0";
5.248 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.249 -by (ASM_SIMP_TAC (arith_ss addrews [zmult]) 1);
5.250 +by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
5.251 val zmult_0 = result();
5.252
5.253 goalw Integ.thy [integ_def,znat_def,one_def]
5.254 "!!z. z : integ ==> $#1 $* z = z";
5.255 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
5.256 -by (ASM_SIMP_TAC (arith_ss addrews [zmult,add_0_right]) 1);
5.257 +by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
5.258 val zmult_1 = result();
5.259
5.260 goalw Integ.thy [integ_def]
5.261 @@ -432,6 +430,5 @@
5.262 [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
5.263
5.264 val integ_ss =
5.265 - arith_ss addcongs integ_congs
5.266 - addrews ([zminus_zminus,zmagnitude_znat,zmagnitude_zminus_znat,
5.267 - zadd_0] @ integ_typechecks);
5.268 + arith_ss addsimps ([zminus_zminus, zmagnitude_znat,
5.269 + zmagnitude_zminus_znat, zadd_0] @ integ_typechecks);
6.1 --- a/src/ZF/ex/LList.ML Fri Sep 17 16:16:38 1993 +0200
6.2 +++ b/src/ZF/ex/LList.ML Fri Sep 17 16:52:10 1993 +0200
6.3 @@ -11,7 +11,6 @@
6.4
6.5 structure LList = Co_Datatype_Fun
6.6 (val thy = QUniv.thy;
6.7 - val thy = QUniv.thy;
6.8 val rec_specs =
6.9 [("llist", "quniv(A)",
6.10 [(["LNil"], "i"),
7.1 --- a/src/ZF/ex/ListN.ML Fri Sep 17 16:16:38 1993 +0200
7.2 +++ b/src/ZF/ex/ListN.ML Fri Sep 17 16:52:10 1993 +0200
7.3 @@ -20,28 +20,24 @@
7.4 val type_intrs = nat_typechecks@List.intrs@[SigmaI]
7.5 val type_elims = [SigmaE2]);
7.6
7.7 -(*Could be generated automatically; requires use of fsplitD*)
7.8 -val listn_induct = standard
7.9 - (fsplitI RSN
7.10 - (2, fsplitI RSN
7.11 - (3, (read_instantiate [("P", "fsplit(R)")] ListN.induct) RS fsplitD)));
7.12 +val listn_induct = standard
7.13 + (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
7.14
7.15 val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
7.16 by (rtac (major RS List.induct) 1);
7.17 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
7.18 +by (ALLGOALS (asm_simp_tac list_ss));
7.19 by (REPEAT (ares_tac ListN.intrs 1));
7.20 val list_into_listn = result();
7.21
7.22 goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
7.23 by (rtac iffI 1);
7.24 by (etac listn_induct 1);
7.25 -by (dtac fsplitD 2);
7.26 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [Pair_iff])));
7.27 -by (fast_tac (ZF_cs addSIs [list_into_listn]) 1);
7.28 +by (safe_tac (ZF_cs addSIs (list_typechecks @
7.29 + [length_Nil, length_Cons, list_into_listn])));
7.30 val listn_iff = result();
7.31
7.32 goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
7.33 by (rtac equality_iffI 1);
7.34 -by (SIMP_TAC (list_ss addrews [listn_iff,separation,image_singleton_iff]) 1);
7.35 +by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
7.36 val listn_image_eq = result();
7.37
8.1 --- a/src/ZF/ex/PropLog.ML Fri Sep 17 16:16:38 1993 +0200
8.2 +++ b/src/ZF/ex/PropLog.ML Fri Sep 17 16:52:10 1993 +0200
8.3 @@ -13,71 +13,66 @@
8.4
8.5 (*** prop_rec -- by Vset recursion ***)
8.6
8.7 -val prop_congs = mk_typed_congs Prop.thy
8.8 - [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
8.9 -
8.10 (** conversion rules **)
8.11
8.12 goal PropLog.thy "prop_rec(Fls,b,c,d) = b";
8.13 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
8.14 by (rewrite_goals_tac Prop.con_defs);
8.15 -by (SIMP_TAC rank_ss 1);
8.16 +by (simp_tac rank_ss 1);
8.17 val prop_rec_Fls = result();
8.18
8.19 goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
8.20 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
8.21 by (rewrite_goals_tac Prop.con_defs);
8.22 -by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
8.23 +by (simp_tac rank_ss 1);
8.24 val prop_rec_Var = result();
8.25
8.26 goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
8.27 \ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
8.28 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
8.29 by (rewrite_goals_tac Prop.con_defs);
8.30 -by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
8.31 +by (simp_tac rank_ss 1);
8.32 val prop_rec_Imp = result();
8.33
8.34 val prop_rec_ss =
8.35 - arith_ss addrews [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
8.36 + arith_ss addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
8.37
8.38 (*** Semantics of propositional logic ***)
8.39
8.40 (** The function is_true **)
8.41
8.42 goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False";
8.43 -by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]) 1);
8.44 +by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1);
8.45 val is_true_Fls = result();
8.46
8.47 goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t";
8.48 -by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]
8.49 - addsplits [expand_if]) 1);
8.50 +by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]
8.51 + setloop (split_tac [expand_if])) 1);
8.52 val is_true_Var = result();
8.53
8.54 goalw PropLog.thy [is_true_def]
8.55 "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
8.56 -by (SIMP_TAC (prop_rec_ss addsplits [expand_if]) 1);
8.57 +by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1);
8.58 val is_true_Imp = result();
8.59
8.60 (** The function hyps **)
8.61
8.62 goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0";
8.63 -by (SIMP_TAC prop_rec_ss 1);
8.64 +by (simp_tac prop_rec_ss 1);
8.65 val hyps_Fls = result();
8.66
8.67 goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}";
8.68 -by (SIMP_TAC prop_rec_ss 1);
8.69 +by (simp_tac prop_rec_ss 1);
8.70 val hyps_Var = result();
8.71
8.72 goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)";
8.73 -by (SIMP_TAC prop_rec_ss 1);
8.74 +by (simp_tac prop_rec_ss 1);
8.75 val hyps_Imp = result();
8.76
8.77 val prop_ss = prop_rec_ss
8.78 - addcongs Prop.congs
8.79 - addcongs (mk_congs PropLog.thy ["Fin", "thms", "op |=","is_true","hyps"])
8.80 - addrews Prop.intrs
8.81 - addrews [is_true_Fls, is_true_Var, is_true_Imp,
8.82 - hyps_Fls, hyps_Var, hyps_Imp];
8.83 + addsimps Prop.intrs
8.84 + addsimps [is_true_Fls, is_true_Var, is_true_Imp,
8.85 + hyps_Fls, hyps_Var, hyps_Imp];
8.86
8.87 (*** Proof theory of propositional logic ***)
8.88
8.89 @@ -162,10 +157,10 @@
8.90 val thms_notE = standard (thms_MP RS thms_FlsE);
8.91
8.92 (*Soundness of the rules wrt truth-table semantics*)
8.93 -val [major] = goalw PropThms.thy [sat_def] "H |- p ==> H |= p";
8.94 -by (rtac (major RS PropThms.induct) 1);
8.95 +goalw PropThms.thy [sat_def] "!!H. H |- p ==> H |= p";
8.96 +by (etac PropThms.induct 1);
8.97 by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
8.98 -by (ALLGOALS (SIMP_TAC prop_ss));
8.99 +by (ALLGOALS (asm_simp_tac prop_ss));
8.100 val soundness = result();
8.101
8.102 (*** Towards the completeness proof ***)
8.103 @@ -194,7 +189,7 @@
8.104 "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
8.105 by (rtac (expand_if RS iffD2) 1);
8.106 by (rtac (major RS Prop.induct) 1);
8.107 -by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [thms_I, thms_H])));
8.108 +by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
8.109 by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2,
8.110 weaken_right, Imp_Fls]
8.111 addSEs [Fls_Imp]) 1);
8.112 @@ -235,10 +230,10 @@
8.113 val [major] = goal PropThms.thy
8.114 "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
8.115 by (rtac (major RS Prop.induct) 1);
8.116 -by (SIMP_TAC prop_ss 1);
8.117 -by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
8.118 +by (simp_tac prop_ss 1);
8.119 +by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
8.120 by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
8.121 -by (ASM_SIMP_TAC prop_ss 1);
8.122 +by (asm_simp_tac prop_ss 1);
8.123 by (fast_tac ZF_cs 1);
8.124 val hyps_Diff = result();
8.125
8.126 @@ -247,10 +242,10 @@
8.127 val [major] = goal PropThms.thy
8.128 "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
8.129 by (rtac (major RS Prop.induct) 1);
8.130 -by (SIMP_TAC prop_ss 1);
8.131 -by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
8.132 +by (simp_tac prop_ss 1);
8.133 +by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
8.134 by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
8.135 -by (ASM_SIMP_TAC prop_ss 1);
8.136 +by (asm_simp_tac prop_ss 1);
8.137 by (fast_tac ZF_cs 1);
8.138 val hyps_cons = result();
8.139
8.140 @@ -269,9 +264,9 @@
8.141 val [major] = goal PropThms.thy
8.142 "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
8.143 by (rtac (major RS Prop.induct) 1);
8.144 -by (ASM_SIMP_TAC (prop_ss addrews [Fin_0I, Fin_consI, UN_I]
8.145 - addsplits [expand_if]) 2);
8.146 -by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [Un_0, Fin_0I, Fin_UnI])));
8.147 +by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I]
8.148 + setloop (split_tac [expand_if])) 2);
8.149 +by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
8.150 val hyps_finite = result();
8.151
8.152 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
8.153 @@ -281,7 +276,7 @@
8.154 val [premp,sat] = goal PropThms.thy
8.155 "[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
8.156 by (rtac (premp RS hyps_finite RS Fin_induct) 1);
8.157 -by (SIMP_TAC (prop_ss addrews [premp, sat, sat_thms_p, Diff_0]) 1);
8.158 +by (simp_tac (prop_ss addsimps [premp, sat, sat_thms_p, Diff_0]) 1);
8.159 by (safe_tac ZF_cs);
8.160 (*Case hyps(p,t)-cons(#v,Y) |- p *)
8.161 by (rtac thms_excluded_middle_rule 1);
8.162 @@ -309,7 +304,7 @@
8.163
8.164 (*A semantic analogue of the Deduction Theorem*)
8.165 goalw PropThms.thy [sat_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
8.166 -by (SIMP_TAC prop_ss 1);
8.167 +by (simp_tac prop_ss 1);
8.168 by (fast_tac ZF_cs 1);
8.169 val sat_Imp = result();
8.170
9.1 --- a/src/ZF/ex/Ramsey.ML Fri Sep 17 16:16:38 1993 +0200
9.2 +++ b/src/ZF/ex/Ramsey.ML Fri Sep 17 16:52:10 1993 +0200
9.3 @@ -20,9 +20,6 @@
9.4
9.5 open Ramsey;
9.6
9.7 -val ramsey_congs = mk_congs Ramsey.thy ["Atleast"];
9.8 -val ramsey_ss = arith_ss addcongs ramsey_congs;
9.9 -
9.10 (*** Cliques and Independent sets ***)
9.11
9.12 goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
9.13 @@ -95,11 +92,12 @@
9.14 \ Atleast(m,A) | Atleast(n,B)";
9.15 by (nat_ind_tac "m" prems 1);
9.16 by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
9.17 -by (ASM_SIMP_TAC ramsey_ss 1);
9.18 +by (asm_simp_tac arith_ss 1);
9.19 by (rtac ballI 1);
9.20 +by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*)
9.21 by (nat_ind_tac "n" [] 1);
9.22 by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
9.23 -by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
9.24 +by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
9.25 by (safe_tac ZF_cs);
9.26 by (etac (Atleast_succD RS bexE) 1);
9.27 by (etac UnE 1);
9.28 @@ -118,7 +116,7 @@
9.29 (*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
9.30 by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
9.31 (*proving the condition*)
9.32 -by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
9.33 +by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
9.34 by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
9.35 val pigeon2_lemma = result();
9.36
9.37 @@ -147,7 +145,7 @@
9.38 "[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \
9.39 \ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
9.40 by (rtac (nat_succI RS pigeon2) 1);
9.41 -by (SIMP_TAC (ramsey_ss addrews prems) 3);
9.42 +by (simp_tac (arith_ss addsimps prems) 3);
9.43 by (rtac Atleast_superset 3);
9.44 by (REPEAT (resolve_tac prems 1));
9.45 by (fast_tac ZF_cs 1);
10.1 --- a/src/ZF/ex/TF_Fn.ML Fri Sep 17 16:16:38 1993 +0200
10.2 +++ b/src/ZF/ex/TF_Fn.ML Fri Sep 17 16:52:10 1993 +0200
10.3 @@ -16,33 +16,29 @@
10.4
10.5 (*** TF_rec -- by Vset recursion ***)
10.6
10.7 -(*Used only to verify TF_rec*)
10.8 -val TF_congs = mk_typed_congs TF.thy
10.9 - [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
10.10 -
10.11 (** conversion rules **)
10.12
10.13 goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
10.14 by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
10.15 by (rewrite_goals_tac TF.con_defs);
10.16 -by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
10.17 +by (simp_tac rank_ss 1);
10.18 val TF_rec_Tcons = result();
10.19
10.20 goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
10.21 by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
10.22 by (rewrite_goals_tac TF.con_defs);
10.23 -by (SIMP_TAC rank_ss 1);
10.24 +by (simp_tac rank_ss 1);
10.25 val TF_rec_Fnil = result();
10.26
10.27 goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
10.28 \ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
10.29 by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
10.30 by (rewrite_goals_tac TF.con_defs);
10.31 -by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
10.32 +by (simp_tac rank_ss 1);
10.33 val TF_rec_Fcons = result();
10.34
10.35 (*list_ss includes list operations as well as arith_ss*)
10.36 -val TF_rec_ss = list_ss addrews
10.37 +val TF_rec_ss = list_ss addsimps
10.38 [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
10.39
10.40 (** Type checking **)
10.41 @@ -56,7 +52,7 @@
10.42 \ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
10.43 \ |] ==> TF_rec(z,b,c,d) : C(z)";
10.44 by (rtac (major RS TF.induct) 1);
10.45 -by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
10.46 +by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
10.47 val TF_rec_type = result();
10.48
10.49 (*Mutually recursive version*)
10.50 @@ -70,7 +66,7 @@
10.51 \ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
10.52 by (rewtac Ball_def);
10.53 by (rtac TF.mutual_induct 1);
10.54 -by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
10.55 +by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
10.56 val tree_forest_rec_type = result();
10.57
10.58
10.59 @@ -159,10 +155,6 @@
10.60 [TconsI, FnilI, FconsI, treeI, forestI,
10.61 list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
10.62
10.63 -val TF_congs = TF.congs @
10.64 - mk_congs TF_Fn.thy
10.65 - ["TF_rec", "list_of_TF", "TF_of_list", "TF_map", "TF_size", "TF_preorder"];
10.66 -
10.67 val TF_rewrites =
10.68 [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
10.69 list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
10.70 @@ -171,8 +163,8 @@
10.71 TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
10.72 TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
10.73
10.74 -val TF_ss = list_ss addcongs TF_congs
10.75 - addrews (TF_rewrites@TF_typechecks);
10.76 +val TF_ss = list_ss addsimps TF_rewrites
10.77 + setsolver type_auto_tac (list_typechecks@TF_typechecks);
10.78
10.79 (** theorems about list_of_TF and TF_of_list **)
10.80
10.81 @@ -188,26 +180,26 @@
10.82
10.83 goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
10.84 by (etac forest_induct 1);
10.85 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
10.86 +by (ALLGOALS (asm_simp_tac TF_ss));
10.87 val forest_iso = result();
10.88
10.89 goal TF_Fn.thy
10.90 "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
10.91 by (etac List.induct 1);
10.92 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
10.93 +by (ALLGOALS (asm_simp_tac TF_ss));
10.94 val tree_list_iso = result();
10.95
10.96 (** theorems about TF_map **)
10.97
10.98 goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
10.99 by (etac TF.induct 1);
10.100 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
10.101 +by (ALLGOALS (asm_simp_tac TF_ss));
10.102 val TF_map_ident = result();
10.103
10.104 goal TF_Fn.thy
10.105 "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
10.106 by (etac TF.induct 1);
10.107 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
10.108 +by (ALLGOALS (asm_simp_tac TF_ss));
10.109 val TF_map_compose = result();
10.110
10.111 (** theorems about TF_size **)
10.112 @@ -215,13 +207,13 @@
10.113 goal TF_Fn.thy
10.114 "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
10.115 by (etac TF.induct 1);
10.116 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
10.117 +by (ALLGOALS (asm_simp_tac TF_ss));
10.118 val TF_size_TF_map = result();
10.119
10.120 goal TF_Fn.thy
10.121 "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
10.122 by (etac TF.induct 1);
10.123 -by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [length_app])));
10.124 +by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
10.125 val TF_size_length = result();
10.126
10.127 (** theorems about TF_preorder **)
10.128 @@ -229,5 +221,5 @@
10.129 goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
10.130 \ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
10.131 by (etac TF.induct 1);
10.132 -by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [map_app_distrib])));
10.133 +by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
10.134 val TF_preorder_TF_map = result();
11.1 --- a/src/ZF/ex/TermFn.ML Fri Sep 17 16:16:38 1993 +0200
11.2 +++ b/src/ZF/ex/TermFn.ML Fri Sep 17 16:52:10 1993 +0200
11.3 @@ -18,11 +18,11 @@
11.4 "[| l: list(A); Ord(i) |] ==> \
11.5 \ rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
11.6 by (rtac (major RS List.induct) 1);
11.7 -by (SIMP_TAC list_ss 1);
11.8 +by (simp_tac list_ss 1);
11.9 by (rtac impI 1);
11.10 by (forward_tac [rank_Cons1 RS Ord_trans] 1);
11.11 by (dtac (rank_Cons2 RS Ord_trans) 2);
11.12 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [ordi, VsetI])));
11.13 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [ordi, VsetI])));
11.14 val map_lemma = result();
11.15
11.16 (*Typing premise is necessary to invoke map_lemma*)
11.17 @@ -31,10 +31,8 @@
11.18 \ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
11.19 by (rtac (term_rec_def RS def_Vrec RS trans) 1);
11.20 by (rewrite_goals_tac Term.con_defs);
11.21 -val term_rec_ss = ZF_ss
11.22 - addcongs (mk_typed_congs TermFn.thy [("d", "[i,i,i]=>i")])
11.23 - addrews [Ord_rank, rank_pair2, prem RS map_lemma];
11.24 -by (SIMP_TAC term_rec_ss 1);
11.25 +val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
11.26 +by (simp_tac term_rec_ss 1);
11.27 val term_rec = result();
11.28
11.29 (*Slightly odd typing condition on r in the second premise!*)
11.30 @@ -49,7 +47,7 @@
11.31 by (rtac (term_rec RS ssubst) 1);
11.32 by (REPEAT (ares_tac prems 1));
11.33 by (etac List.induct 1);
11.34 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [term_rec])));
11.35 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
11.36 by (etac CollectE 1);
11.37 by (REPEAT (ares_tac [ConsI, UN_I] 1));
11.38 val term_rec_type = result();
11.39 @@ -122,31 +120,27 @@
11.40
11.41 (*map_type2 and term_map_type2 instantiate variables*)
11.42 val term_ss = list_ss
11.43 - addcongs (Term.congs @
11.44 - mk_congs TermFn.thy ["term_rec","term_map","term_size",
11.45 - "reflect","preorder"])
11.46 - addrews [term_rec, term_map, term_size, reflect,
11.47 - preorder]
11.48 - setauto type_auto_tac (list_typechecks@term_typechecks);
11.49 + addsimps [term_rec, term_map, term_size, reflect, preorder]
11.50 + setsolver type_auto_tac (list_typechecks@term_typechecks);
11.51
11.52
11.53 (** theorems about term_map **)
11.54
11.55 goal TermFn.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
11.56 by (etac term_induct_eqn 1);
11.57 -by (ASM_SIMP_TAC (term_ss addrews [map_ident]) 1);
11.58 +by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
11.59 val term_map_ident = result();
11.60
11.61 goal TermFn.thy
11.62 "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
11.63 by (etac term_induct_eqn 1);
11.64 -by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
11.65 +by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
11.66 val term_map_compose = result();
11.67
11.68 goal TermFn.thy
11.69 "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
11.70 by (etac term_induct_eqn 1);
11.71 -by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose]) 1);
11.72 +by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
11.73 val term_map_reflect = result();
11.74
11.75
11.76 @@ -155,18 +149,18 @@
11.77 goal TermFn.thy
11.78 "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
11.79 by (etac term_induct_eqn 1);
11.80 -by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
11.81 +by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
11.82 val term_size_term_map = result();
11.83
11.84 goal TermFn.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
11.85 by (etac term_induct_eqn 1);
11.86 -by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose,
11.87 - list_add_rev]) 1);
11.88 +by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
11.89 + list_add_rev]) 1);
11.90 val term_size_reflect = result();
11.91
11.92 goal TermFn.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
11.93 by (etac term_induct_eqn 1);
11.94 -by (ASM_SIMP_TAC (term_ss addrews [length_flat, map_compose]) 1);
11.95 +by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
11.96 val term_size_length = result();
11.97
11.98
11.99 @@ -174,8 +168,8 @@
11.100
11.101 goal TermFn.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
11.102 by (etac term_induct_eqn 1);
11.103 -by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib, map_compose,
11.104 - map_ident, rev_rev_ident]) 1);
11.105 +by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
11.106 + map_ident, rev_rev_ident]) 1);
11.107 val reflect_reflect_ident = result();
11.108
11.109
11.110 @@ -184,7 +178,7 @@
11.111 goal TermFn.thy
11.112 "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
11.113 by (etac term_induct_eqn 1);
11.114 -by (ASM_SIMP_TAC (term_ss addrews [map_compose, map_flat]) 1);
11.115 +by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
11.116 val preorder_term_map = result();
11.117
11.118 (** preorder(reflect(t)) = rev(postorder(t)) **)
12.1 --- a/src/ZF/ex/binfn.ML Fri Sep 17 16:16:38 1993 +0200
12.2 +++ b/src/ZF/ex/binfn.ML Fri Sep 17 16:52:10 1993 +0200
12.3 @@ -14,20 +14,19 @@
12.4 goal BinFn.thy "bin_rec(Plus,a,b,h) = a";
12.5 by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
12.6 by (rewrite_goals_tac Bin.con_defs);
12.7 -by (SIMP_TAC rank_ss 1);
12.8 +by (simp_tac rank_ss 1);
12.9 val bin_rec_Plus = result();
12.10
12.11 goal BinFn.thy "bin_rec(Minus,a,b,h) = b";
12.12 by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
12.13 by (rewrite_goals_tac Bin.con_defs);
12.14 -by (SIMP_TAC rank_ss 1);
12.15 +by (simp_tac rank_ss 1);
12.16 val bin_rec_Minus = result();
12.17
12.18 goal BinFn.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
12.19 by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
12.20 by (rewrite_goals_tac Bin.con_defs);
12.21 -by (SIMP_TAC (rank_ss addcongs
12.22 - (mk_typed_congs BinFn.thy [("h", "[i,i,i]=>i")])) 1);
12.23 +by (simp_tac rank_ss 1);
12.24 val bin_rec_Bcons = result();
12.25
12.26 (*Type checking*)
12.27 @@ -38,7 +37,7 @@
12.28 \ |] ==> bin_rec(w,a,b,h) : C(w)";
12.29 by (bin_ind_tac "w" prems 1);
12.30 by (ALLGOALS
12.31 - (ASM_SIMP_TAC (ZF_ss addrews (prems@[bin_rec_Plus,bin_rec_Minus,
12.32 + (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
12.33 bin_rec_Bcons]))));
12.34 val bin_rec_type = result();
12.35
12.36 @@ -106,13 +105,8 @@
12.37 [integ_of_bin_type, bin_succ_type, bin_pred_type,
12.38 bin_minus_type, bin_add_type, bin_mult_type];
12.39
12.40 -val bin_congs = mk_congs BinFn.thy
12.41 - ["bin_rec","op $$","integ_of_bin","bin_succ","bin_pred",
12.42 - "bin_minus","bin_add","bin_mult"];
12.43 -
12.44 val bin_ss = integ_ss
12.45 - addcongs (bin_congs@bool_congs)
12.46 - addrews([bool_1I, bool_0I,
12.47 + addsimps([bool_1I, bool_0I,
12.48 bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
12.49 bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
12.50
12.51 @@ -127,7 +121,7 @@
12.52 "!!z v. [| z $+ v = z' $+ v'; \
12.53 \ z: integ; z': integ; v: integ; v': integ; w: integ |] \
12.54 \ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
12.55 -by (ASM_SIMP_TAC (integ_ss addrews ([zadd_assoc RS sym])) 1);
12.56 +by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
12.57 val zadd_assoc_cong = result();
12.58
12.59 goal Integ.thy
12.60 @@ -136,7 +130,8 @@
12.61 by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
12.62 val zadd_assoc_swap = result();
12.63
12.64 -val [zadd_cong] = mk_congs Integ.thy ["op $+"];
12.65 +val zadd_cong =
12.66 + read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2;
12.67
12.68 val zadd_kill = (refl RS zadd_cong);
12.69 val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
12.70 @@ -151,28 +146,28 @@
12.71 val zadd_swap_pairs = result();
12.72
12.73
12.74 -val carry_ss = bin_ss addrews
12.75 +val carry_ss = bin_ss addsimps
12.76 (bin_recs bin_succ_def @ bin_recs bin_pred_def);
12.77
12.78 goal BinFn.thy
12.79 "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
12.80 by (etac Bin.induct 1);
12.81 -by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
12.82 -by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
12.83 +by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
12.84 +by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
12.85 by (etac boolE 1);
12.86 -by (ALLGOALS (ASM_SIMP_TAC (carry_ss addrews [zadd_assoc])));
12.87 +by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc])));
12.88 by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
12.89 val integ_of_bin_succ = result();
12.90
12.91 goal BinFn.thy
12.92 "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
12.93 by (etac Bin.induct 1);
12.94 -by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
12.95 -by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
12.96 +by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
12.97 +by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
12.98 by (etac boolE 1);
12.99 by (ALLGOALS
12.100 - (ASM_SIMP_TAC
12.101 - (carry_ss addrews [zadd_assoc RS sym,
12.102 + (asm_simp_tac
12.103 + (carry_ss addsimps [zadd_assoc RS sym,
12.104 zadd_zminus_inverse, zadd_zminus_inverse2])));
12.105 by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
12.106 val integ_of_bin_pred = result();
12.107 @@ -183,68 +178,68 @@
12.108 (*** bin_minus: (unary!) negation of binary integers ***)
12.109
12.110 val bin_minus_ss =
12.111 - bin_ss addrews (bin_recs bin_minus_def @
12.112 + bin_ss addsimps (bin_recs bin_minus_def @
12.113 [integ_of_bin_succ, integ_of_bin_pred]);
12.114
12.115 goal BinFn.thy
12.116 "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
12.117 by (etac Bin.induct 1);
12.118 -by (SIMP_TAC (bin_minus_ss addrews [zminus_0]) 1);
12.119 -by (SIMP_TAC (bin_minus_ss addrews [zadd_0_right]) 1);
12.120 +by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1);
12.121 +by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1);
12.122 by (etac boolE 1);
12.123 by (ALLGOALS
12.124 - (ASM_SIMP_TAC (bin_minus_ss addrews [zminus_zadd_distrib, zadd_assoc])));
12.125 + (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
12.126 val integ_of_bin_minus = result();
12.127
12.128
12.129 (*** bin_add: binary addition ***)
12.130
12.131 goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
12.132 -by (ASM_SIMP_TAC bin_ss 1);
12.133 +by (asm_simp_tac bin_ss 1);
12.134 val bin_add_Plus = result();
12.135
12.136 goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
12.137 -by (ASM_SIMP_TAC bin_ss 1);
12.138 +by (asm_simp_tac bin_ss 1);
12.139 val bin_add_Minus = result();
12.140
12.141 goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
12.142 -by (SIMP_TAC bin_ss 1);
12.143 +by (simp_tac bin_ss 1);
12.144 val bin_add_Bcons_Plus = result();
12.145
12.146 goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
12.147 -by (SIMP_TAC bin_ss 1);
12.148 +by (simp_tac bin_ss 1);
12.149 val bin_add_Bcons_Minus = result();
12.150
12.151 goalw BinFn.thy [bin_add_def]
12.152 "!!w y. [| w: bin; y: bool |] ==> \
12.153 \ bin_add(v$$x, w$$y) = \
12.154 \ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
12.155 -by (ASM_SIMP_TAC bin_ss 1);
12.156 +by (asm_simp_tac bin_ss 1);
12.157 val bin_add_Bcons_Bcons = result();
12.158
12.159 val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
12.160 bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
12.161 integ_of_bin_succ, integ_of_bin_pred];
12.162
12.163 -val bin_add_ss = bin_ss addrews ([bool_subset_nat RS subsetD] @ bin_add_rews);
12.164 +val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews);
12.165
12.166 goal BinFn.thy
12.167 "!!v. v: bin ==> \
12.168 \ ALL w: bin. integ_of_bin(bin_add(v,w)) = \
12.169 \ integ_of_bin(v) $+ integ_of_bin(w)";
12.170 by (etac Bin.induct 1);
12.171 -by (SIMP_TAC bin_add_ss 1);
12.172 -by (SIMP_TAC bin_add_ss 1);
12.173 +by (simp_tac bin_add_ss 1);
12.174 +by (simp_tac bin_add_ss 1);
12.175 by (rtac ballI 1);
12.176 by (bin_ind_tac "wa" [] 1);
12.177 -by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_0_right]) 1);
12.178 -by (ASM_SIMP_TAC bin_add_ss 1);
12.179 +by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1);
12.180 +by (asm_simp_tac bin_add_ss 1);
12.181 by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
12.182 by (etac boolE 1);
12.183 -by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc, zadd_swap_pairs]) 2);
12.184 +by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2);
12.185 by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
12.186 by (etac boolE 1);
12.187 -by (ALLGOALS (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc,zadd_swap_pairs])));
12.188 +by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
12.189 by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
12.190 typechecks) 1));
12.191 val integ_of_bin_add_lemma = result();
12.192 @@ -255,7 +250,7 @@
12.193 (*** bin_add: binary multiplication ***)
12.194
12.195 val bin_mult_ss =
12.196 - bin_ss addrews (bin_recs bin_mult_def @
12.197 + bin_ss addsimps (bin_recs bin_mult_def @
12.198 [integ_of_bin_minus, integ_of_bin_add]);
12.199
12.200
12.201 @@ -265,12 +260,12 @@
12.202 \ integ_of_bin(v) $* integ_of_bin(w)";
12.203 by (cut_facts_tac prems 1);
12.204 by (bin_ind_tac "v" [major] 1);
12.205 -by (SIMP_TAC (bin_mult_ss addrews [zmult_0]) 1);
12.206 -by (SIMP_TAC (bin_mult_ss addrews [zmult_1,zmult_zminus]) 1);
12.207 +by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1);
12.208 +by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1);
12.209 by (etac boolE 1);
12.210 -by (ASM_SIMP_TAC (bin_mult_ss addrews [zadd_zmult_distrib]) 2);
12.211 -by (ASM_SIMP_TAC
12.212 - (bin_mult_ss addrews [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
12.213 +by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2);
12.214 +by (asm_simp_tac
12.215 + (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
12.216 by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
12.217 typechecks) 1));
12.218 val integ_of_bin_mult = result();
12.219 @@ -283,19 +278,19 @@
12.220 val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
12.221
12.222 goal BinFn.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
12.223 -by (SIMP_TAC carry_ss 1);
12.224 +by (simp_tac carry_ss 1);
12.225 val bin_succ_Bcons1 = result();
12.226
12.227 goal BinFn.thy "bin_succ(w$$0) = w$$1";
12.228 -by (SIMP_TAC carry_ss 1);
12.229 +by (simp_tac carry_ss 1);
12.230 val bin_succ_Bcons0 = result();
12.231
12.232 goal BinFn.thy "bin_pred(w$$1) = w$$0";
12.233 -by (SIMP_TAC carry_ss 1);
12.234 +by (simp_tac carry_ss 1);
12.235 val bin_pred_Bcons1 = result();
12.236
12.237 goal BinFn.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
12.238 -by (SIMP_TAC carry_ss 1);
12.239 +by (simp_tac carry_ss 1);
12.240 val bin_pred_Bcons0 = result();
12.241
12.242 (** extra rules for bin_minus **)
12.243 @@ -303,28 +298,28 @@
12.244 val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
12.245
12.246 goal BinFn.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
12.247 -by (SIMP_TAC bin_minus_ss 1);
12.248 +by (simp_tac bin_minus_ss 1);
12.249 val bin_minus_Bcons1 = result();
12.250
12.251 goal BinFn.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
12.252 -by (SIMP_TAC bin_minus_ss 1);
12.253 +by (simp_tac bin_minus_ss 1);
12.254 val bin_minus_Bcons0 = result();
12.255
12.256 (** extra rules for bin_add **)
12.257
12.258 goal BinFn.thy
12.259 "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
12.260 -by (ASM_SIMP_TAC bin_add_ss 1);
12.261 +by (asm_simp_tac bin_add_ss 1);
12.262 val bin_add_Bcons_Bcons11 = result();
12.263
12.264 goal BinFn.thy
12.265 "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
12.266 -by (ASM_SIMP_TAC bin_add_ss 1);
12.267 +by (asm_simp_tac bin_add_ss 1);
12.268 val bin_add_Bcons_Bcons10 = result();
12.269
12.270 goal BinFn.thy
12.271 "!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
12.272 -by (ASM_SIMP_TAC bin_add_ss 1);
12.273 +by (asm_simp_tac bin_add_ss 1);
12.274 val bin_add_Bcons_Bcons0 = result();
12.275
12.276 (** extra rules for bin_mult **)
12.277 @@ -332,24 +327,18 @@
12.278 val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
12.279
12.280 goal BinFn.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
12.281 -by (SIMP_TAC bin_mult_ss 1);
12.282 +by (simp_tac bin_mult_ss 1);
12.283 val bin_mult_Bcons1 = result();
12.284
12.285 goal BinFn.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
12.286 -by (SIMP_TAC bin_mult_ss 1);
12.287 +by (simp_tac bin_mult_ss 1);
12.288 val bin_mult_Bcons0 = result();
12.289
12.290
12.291 (*** The computation simpset ***)
12.292
12.293 -val bin_comp_ss = carry_ss addrews
12.294 - [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, bin_add_Bcons_Minus,
12.295 - bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11]
12.296 - setauto (type_auto_tac bin_typechecks0);
12.297 -
12.298 val bin_comp_ss = integ_ss
12.299 - addcongs bin_congs
12.300 - addrews [bin_succ_Plus, bin_succ_Minus,
12.301 + addsimps [bin_succ_Plus, bin_succ_Minus,
12.302 bin_succ_Bcons1, bin_succ_Bcons0,
12.303 bin_pred_Plus, bin_pred_Minus,
12.304 bin_pred_Bcons1, bin_pred_Bcons0,
12.305 @@ -360,7 +349,7 @@
12.306 bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
12.307 bin_mult_Plus, bin_mult_Minus,
12.308 bin_mult_Bcons1, bin_mult_Bcons0]
12.309 - setauto (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
12.310 + setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
12.311
12.312 (*** Examples of performing binary arithmetic by simplification ***)
12.313
12.314 @@ -370,7 +359,7 @@
12.315 (* 13+19 = 32 *)
12.316 goal BinFn.thy
12.317 "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
12.318 -by (SIMP_TAC bin_comp_ss 1); (*1.9 secs*)
12.319 +by (simp_tac bin_comp_ss 1); (*0.6 secs*)
12.320 result();
12.321
12.322 bin_add(binary_of_int 13, binary_of_int 19);
12.323 @@ -380,7 +369,7 @@
12.324 "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
12.325 \ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
12.326 \ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
12.327 -by (SIMP_TAC bin_comp_ss 1); (*8.9 secs*)
12.328 +by (simp_tac bin_comp_ss 1); (*2.6 secs*)
12.329 result();
12.330
12.331 bin_add(binary_of_int 1234, binary_of_int 5678);
12.332 @@ -390,7 +379,7 @@
12.333 "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
12.334 \ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
12.335 \ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
12.336 -by (SIMP_TAC bin_comp_ss 1); (*7.4 secs*)
12.337 +by (simp_tac bin_comp_ss 1); (*2.3 secs*)
12.338 result();
12.339
12.340 bin_add(binary_of_int 1359, binary_of_int ~2468);
12.341 @@ -400,7 +389,7 @@
12.342 "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
12.343 \ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
12.344 \ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
12.345 -by (SIMP_TAC bin_comp_ss 1); (*13.7 secs*)
12.346 +by (simp_tac bin_comp_ss 1); (*3.9 secs*)
12.347 result();
12.348
12.349 bin_add(binary_of_int 93746, binary_of_int ~46375);
12.350 @@ -409,7 +398,7 @@
12.351 goal BinFn.thy
12.352 "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
12.353 \ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
12.354 -by (SIMP_TAC bin_comp_ss 1); (*2.8 secs*)
12.355 +by (simp_tac bin_comp_ss 1); (*0.6 secs*)
12.356 result();
12.357
12.358 bin_minus(binary_of_int 65745);
12.359 @@ -418,7 +407,7 @@
12.360 goal BinFn.thy
12.361 "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
12.362 \ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
12.363 -by (SIMP_TAC bin_comp_ss 1); (*3.3 secs*)
12.364 +by (simp_tac bin_comp_ss 1); (*0.7 secs*)
12.365 result();
12.366
12.367 bin_minus(binary_of_int ~54321);
12.368 @@ -426,7 +415,7 @@
12.369 (* 13*19 = 247 *)
12.370 goal BinFn.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
12.371 \ Plus$$1$$1$$1$$1$$0$$1$$1$$1";
12.372 -by (SIMP_TAC bin_comp_ss 1); (*4.4 secs*)
12.373 +by (simp_tac bin_comp_ss 1); (*1.5 secs*)
12.374 result();
12.375
12.376 bin_mult(binary_of_int 13, binary_of_int 19);
12.377 @@ -435,7 +424,7 @@
12.378 goal BinFn.thy
12.379 "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
12.380 \ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
12.381 -by (SIMP_TAC bin_comp_ss 1); (*9.2 secs*)
12.382 +by (simp_tac bin_comp_ss 1); (*2.6 secs*)
12.383 result();
12.384
12.385 bin_mult(binary_of_int ~84, binary_of_int 51);
12.386 @@ -445,19 +434,17 @@
12.387 "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
12.388 \ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
12.389 \ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
12.390 -by (SIMP_TAC bin_comp_ss 1); (*38.4 secs*)
12.391 +by (simp_tac bin_comp_ss 1); (*9.8 secs*)
12.392 result();
12.393
12.394 bin_mult(binary_of_int 255, binary_of_int 255);
12.395
12.396 -(***************** TOO SLOW TO INCLUDE IN TEST RUNS
12.397 (* 1359 * ~2468 = ~3354012 *)
12.398 goal BinFn.thy
12.399 "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
12.400 \ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
12.401 \ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
12.402 -by (SIMP_TAC bin_comp_ss 1); (*54.8 secs*)
12.403 +by (simp_tac bin_comp_ss 1); (*13.7 secs*)
12.404 result();
12.405 -****************)
12.406
12.407 bin_mult(binary_of_int 1359, binary_of_int ~2468);
13.1 --- a/src/ZF/ex/bt_fn.ML Fri Sep 17 16:16:38 1993 +0200
13.2 +++ b/src/ZF/ex/bt_fn.ML Fri Sep 17 16:52:10 1993 +0200
13.3 @@ -12,28 +12,24 @@
13.4
13.5 (** bt_rec -- by Vset recursion **)
13.6
13.7 -(*Used to verify bt_rec*)
13.8 -val bt_rec_ss = ZF_ss
13.9 - addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")])
13.10 - addrews BT.case_eqns;
13.11 -
13.12 goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))";
13.13 -by (SIMP_TAC rank_ss 1);
13.14 +by (simp_tac rank_ss 1);
13.15 val rank_Br1 = result();
13.16
13.17 goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))";
13.18 -by (SIMP_TAC rank_ss 1);
13.19 +by (simp_tac rank_ss 1);
13.20 val rank_Br2 = result();
13.21
13.22 goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
13.23 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
13.24 -by (SIMP_TAC bt_rec_ss 1);
13.25 +by (simp_tac (ZF_ss addsimps BT.case_eqns) 1);
13.26 val bt_rec_Lf = result();
13.27
13.28 goal BT_Fn.thy
13.29 "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
13.30 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
13.31 -by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1);
13.32 +by (simp_tac (ZF_ss addsimps
13.33 + (BT.case_eqns @ [Vset_rankI, rank_Br1, rank_Br2])) 1);
13.34 val bt_rec_Br = result();
13.35
13.36 (*Type checking -- proved by induction, as usual*)
13.37 @@ -44,7 +40,7 @@
13.38 \ h(x,y,z,r,s): C(Br(x,y,z)) \
13.39 \ |] ==> bt_rec(t,c,h) : C(t)";
13.40 by (bt_ind_tac "t" prems 1);
13.41 -by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
13.42 +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
13.43 (prems@[bt_rec_Lf,bt_rec_Br]))));
13.44 val bt_rec_type = result();
13.45
13.46 @@ -98,15 +94,10 @@
13.47 val bt_typechecks =
13.48 [LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
13.49
13.50 -val bt_congs =
13.51 - BT.congs @
13.52 - mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"];
13.53 -
13.54 val bt_ss = arith_ss
13.55 - addcongs bt_congs
13.56 - addrews BT.case_eqns
13.57 - addrews bt_typechecks
13.58 - addrews [bt_rec_Lf, bt_rec_Br,
13.59 + addsimps BT.case_eqns
13.60 + addsimps bt_typechecks
13.61 + addsimps [bt_rec_Lf, bt_rec_Br,
13.62 n_nodes_Lf, n_nodes_Br,
13.63 n_leaves_Lf, n_leaves_Br,
13.64 bt_reflect_Lf, bt_reflect_Br];
13.65 @@ -117,14 +108,14 @@
13.66 val prems = goal BT_Fn.thy
13.67 "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
13.68 by (bt_ind_tac "t" prems 1);
13.69 -by (ALLGOALS (ASM_SIMP_TAC bt_ss));
13.70 +by (ALLGOALS (asm_simp_tac bt_ss));
13.71 by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
13.72 val n_leaves_reflect = result();
13.73
13.74 val prems = goal BT_Fn.thy
13.75 "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
13.76 by (bt_ind_tac "t" prems 1);
13.77 -by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right])));
13.78 +by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
13.79 val n_leaves_nodes = result();
13.80
13.81 (*** theorems about bt_reflect ***)
13.82 @@ -132,7 +123,7 @@
13.83 val prems = goal BT_Fn.thy
13.84 "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
13.85 by (bt_ind_tac "t" prems 1);
13.86 -by (ALLGOALS (ASM_SIMP_TAC bt_ss));
13.87 +by (ALLGOALS (asm_simp_tac bt_ss));
13.88 val bt_reflect_bt_reflect_ident = result();
13.89
13.90
14.1 --- a/src/ZF/ex/enum.ML Fri Sep 17 16:16:38 1993 +0200
14.2 +++ b/src/ZF/ex/enum.ML Fri Sep 17 16:52:10 1993 +0200
14.3 @@ -28,6 +28,6 @@
14.4 val type_elims = []);
14.5
14.6 goal Enum.thy "~ con59=con60";
14.7 -by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1); (*2.3 secs*)
14.8 +by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*)
14.9 result();
14.10
15.1 --- a/src/ZF/ex/equiv.ML Fri Sep 17 16:16:38 1993 +0200
15.2 +++ b/src/ZF/ex/equiv.ML Fri Sep 17 16:52:10 1993 +0200
15.3 @@ -190,7 +190,7 @@
15.4 by (safe_tac ZF_cs);
15.5 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
15.6 by (assume_tac 1);
15.7 -by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
15.8 +by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
15.9 congruent2_implies_congruent]) 1);
15.10 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
15.11 by (fast_tac ZF_cs 1);
15.12 @@ -200,7 +200,7 @@
15.13 "[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \
15.14 \ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
15.15 by (cut_facts_tac prems 1);
15.16 -by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
15.17 +by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
15.18 congruent2_implies_congruent,
15.19 congruent2_implies_congruent_UN]) 1);
15.20 val UN_equiv_class2 = result();
15.21 @@ -235,7 +235,7 @@
15.22
15.23 val [equivA,commute,congt] = goal Equiv.thy
15.24 "[| equiv(A,r); \
15.25 -\ !! y z w. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
15.26 +\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
15.27 \ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
15.28 \ |] ==> congruent2(r,b)";
15.29 by (resolve_tac [equivA RS congruent2I] 1);
15.30 @@ -259,7 +259,7 @@
15.31 by (safe_tac ZF_cs);
15.32 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
15.33 by (assume_tac 1);
15.34 -by (ASM_SIMP_TAC (ZF_ss addrews [congt RS (equivA RS UN_equiv_class)]) 1);
15.35 +by (asm_simp_tac (ZF_ss addsimps [congt RS (equivA RS UN_equiv_class)]) 1);
15.36 by (rtac (commute RS trans) 1);
15.37 by (rtac (commute RS trans RS sym) 3);
15.38 by (rtac sym 5);
16.1 --- a/src/ZF/ex/integ.ML Fri Sep 17 16:16:38 1993 +0200
16.2 +++ b/src/ZF/ex/integ.ML Fri Sep 17 16:52:10 1993 +0200
16.3 @@ -12,16 +12,18 @@
16.4 $+ and $* are monotonic wrt $<
16.5 *)
16.6
16.7 +val add_cong =
16.8 + read_instantiate_sg (sign_of Arith.thy) [("t","op #+")] subst_context2;
16.9 +
16.10 +
16.11 open Integ;
16.12
16.13 -val [add_cong] = mk_congs Arith.thy ["op #+"];
16.14 -
16.15 (*** Proving that intrel is an equivalence relation ***)
16.16
16.17 val prems = goal Arith.thy
16.18 "[| m #+ n = m' #+ n'; m: nat; m': nat |] \
16.19 \ ==> m #+ (n #+ k) = m' #+ (n' #+ k)";
16.20 -by (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym] @ prems)) 1);
16.21 +by (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym] @ prems)) 1);
16.22 val add_assoc_cong = result();
16.23
16.24 val prems = goal Arith.thy
16.25 @@ -31,6 +33,7 @@
16.26 val add_assoc_swap = result();
16.27
16.28 val add_kill = (refl RS add_cong);
16.29 +
16.30 val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans);
16.31
16.32 (*By luck, requires no typing premises for y1, y2,y3*)
16.33 @@ -90,22 +93,17 @@
16.34 val equiv_intrel = result();
16.35
16.36
16.37 -val integ_congs = mk_congs Integ.thy
16.38 - ["znat", "zminus", "znegative", "zmagnitude", "op $+", "op $-", "op $*"];
16.39 +val intrel_ss =
16.40 + arith_ss addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
16.41
16.42 -val intrel_ss0 = arith_ss addcongs integ_congs;
16.43 -
16.44 -val intrel_ss =
16.45 - intrel_ss0 addrews [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
16.46 -
16.47 -(*More than twice as fast as simplifying with intrel_ss*)
16.48 +(*Roughly twice as fast as simplifying with intrel_ss*)
16.49 fun INTEG_SIMP_TAC ths =
16.50 - let val ss = intrel_ss0 addrews ths
16.51 + let val ss = arith_ss addsimps ths
16.52 in fn i =>
16.53 - EVERY [ASM_SIMP_TAC ss i,
16.54 + EVERY [asm_simp_tac ss i,
16.55 rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i,
16.56 typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks),
16.57 - ASM_SIMP_TAC ss i]
16.58 + asm_simp_tac ss i]
16.59 end;
16.60
16.61
16.62 @@ -130,7 +128,7 @@
16.63 goalw Integ.thy [congruent_def]
16.64 "congruent(intrel, split(%x y. intrel``{<y,x>}))";
16.65 by (safe_tac intrel_cs);
16.66 -by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
16.67 +by (ALLGOALS (asm_simp_tac intrel_ss));
16.68 by (etac (box_equals RS sym) 1);
16.69 by (REPEAT (ares_tac [add_commute] 1));
16.70 val zminus_congruent = result();
16.71 @@ -150,7 +148,7 @@
16.72 by (REPEAT (ares_tac prems 1));
16.73 by (REPEAT (etac SigmaE 1));
16.74 by (etac rev_mp 1);
16.75 -by (ASM_SIMP_TAC ZF_ss 1);
16.76 +by (asm_simp_tac ZF_ss 1);
16.77 by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel]
16.78 addSEs [box_equals RS sym, add_commute,
16.79 make_elim eq_equiv_class]) 1);
16.80 @@ -158,17 +156,17 @@
16.81
16.82 val prems = goalw Integ.thy [zminus_def]
16.83 "[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
16.84 -by (ASM_SIMP_TAC
16.85 - (ZF_ss addrews (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
16.86 +by (asm_simp_tac
16.87 + (ZF_ss addsimps (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
16.88 val zminus = result();
16.89
16.90 goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z";
16.91 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.92 -by (ASM_SIMP_TAC (ZF_ss addrews [zminus] addcongs integ_congs) 1);
16.93 +by (asm_simp_tac (ZF_ss addsimps [zminus]) 1);
16.94 val zminus_zminus = result();
16.95
16.96 goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0";
16.97 -by (SIMP_TAC (arith_ss addrews [zminus]) 1);
16.98 +by (simp_tac (arith_ss addsimps [zminus]) 1);
16.99 val zminus_0 = result();
16.100
16.101
16.102 @@ -179,13 +177,13 @@
16.103 by (safe_tac intrel_cs);
16.104 by (rtac (add_not_less_self RS notE) 1);
16.105 by (etac ssubst 3);
16.106 -by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 3);
16.107 +by (asm_simp_tac (arith_ss addsimps [add_0_right]) 3);
16.108 by (REPEAT (assume_tac 1));
16.109 val not_znegative_znat = result();
16.110
16.111 val [nnat] = goalw Integ.thy [znegative_def, znat_def]
16.112 "n: nat ==> znegative($~ $# succ(n))";
16.113 -by (SIMP_TAC (intrel_ss addrews [zminus,nnat]) 1);
16.114 +by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
16.115 by (REPEAT
16.116 (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
16.117 refl RS intrelI RS imageI, consI1, nnat, nat_0I,
16.118 @@ -198,19 +196,19 @@
16.119 goalw Integ.thy [congruent_def]
16.120 "congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))";
16.121 by (safe_tac intrel_cs);
16.122 -by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
16.123 +by (ALLGOALS (asm_simp_tac intrel_ss));
16.124 by (etac rev_mp 1);
16.125 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
16.126 by (REPEAT (assume_tac 1));
16.127 -by (ASM_SIMP_TAC (arith_ss addrews [add_succ_right,succ_inject_iff]) 3);
16.128 -by (ASM_SIMP_TAC
16.129 - (arith_ss addrews [diff_add_inverse,diff_add_0,add_0_right]) 2);
16.130 -by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 1);
16.131 +by (asm_simp_tac (arith_ss addsimps [add_succ_right,succ_inject_iff]) 3);
16.132 +by (asm_simp_tac
16.133 + (arith_ss addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2);
16.134 +by (asm_simp_tac (arith_ss addsimps [add_0_right]) 1);
16.135 by (rtac impI 1);
16.136 by (etac subst 1);
16.137 by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
16.138 by (REPEAT (assume_tac 1));
16.139 -by (ASM_SIMP_TAC (arith_ss addrews [diff_add_inverse,diff_add_0]) 1);
16.140 +by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
16.141 val zmagnitude_congruent = result();
16.142
16.143 (*Resolve th against the corresponding facts for zmagnitude*)
16.144 @@ -225,18 +223,18 @@
16.145 val prems = goalw Integ.thy [zmagnitude_def]
16.146 "[| x: nat; y: nat |] ==> \
16.147 \ zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)";
16.148 -by (ASM_SIMP_TAC
16.149 - (ZF_ss addrews (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
16.150 +by (asm_simp_tac
16.151 + (ZF_ss addsimps (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
16.152 val zmagnitude = result();
16.153
16.154 val [nnat] = goalw Integ.thy [znat_def]
16.155 "n: nat ==> zmagnitude($# n) = n";
16.156 -by (SIMP_TAC (intrel_ss addrews [zmagnitude,nnat]) 1);
16.157 +by (simp_tac (intrel_ss addsimps [zmagnitude,nnat]) 1);
16.158 val zmagnitude_znat = result();
16.159
16.160 val [nnat] = goalw Integ.thy [znat_def]
16.161 "n: nat ==> zmagnitude($~ $# n) = n";
16.162 -by (SIMP_TAC (intrel_ss addrews [zmagnitude,zminus,nnat,add_0_right]) 1);
16.163 +by (simp_tac (intrel_ss addsimps [zmagnitude,zminus,nnat,add_0_right]) 1);
16.164 val zmagnitude_zminus_znat = result();
16.165
16.166
16.167 @@ -254,7 +252,7 @@
16.168 by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1);
16.169 by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3);
16.170 by (typechk_tac [add_type]);
16.171 -by (ASM_SIMP_TAC (arith_ss addrews [add_assoc RS sym]) 1);
16.172 +by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
16.173 val zadd_congruent2 = result();
16.174
16.175 (*Resolve th against the corresponding facts for zadd*)
16.176 @@ -269,19 +267,19 @@
16.177 val prems = goalw Integ.thy [zadd_def]
16.178 "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
16.179 \ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = intrel `` {<x1#+x2, y1#+y2>}";
16.180 -by (ASM_SIMP_TAC (ZF_ss addrews
16.181 +by (asm_simp_tac (ZF_ss addsimps
16.182 (prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1);
16.183 val zadd = result();
16.184
16.185 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";
16.186 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.187 -by (ASM_SIMP_TAC (arith_ss addrews [zadd]) 1);
16.188 +by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
16.189 val zadd_0 = result();
16.190
16.191 goalw Integ.thy [integ_def]
16.192 "!!z w. [| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
16.193 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.194 -by (ASM_SIMP_TAC (arith_ss addrews [zminus,zadd] addcongs integ_congs) 1);
16.195 +by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
16.196 val zminus_zadd_distrib = result();
16.197
16.198 goalw Integ.thy [integ_def]
16.199 @@ -296,17 +294,17 @@
16.200 \ (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
16.201 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.202 (*rewriting is much faster without intrel_iff, etc.*)
16.203 -by (ASM_SIMP_TAC (intrel_ss0 addrews [zadd,add_assoc]) 1);
16.204 +by (asm_simp_tac (arith_ss addsimps [zadd,add_assoc]) 1);
16.205 val zadd_assoc = result();
16.206
16.207 val prems = goalw Integ.thy [znat_def]
16.208 "[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
16.209 -by (ASM_SIMP_TAC (arith_ss addrews (zadd::prems)) 1);
16.210 +by (asm_simp_tac (arith_ss addsimps (zadd::prems)) 1);
16.211 val znat_add = result();
16.212
16.213 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0";
16.214 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.215 -by (ASM_SIMP_TAC (intrel_ss addrews [zminus,zadd,add_0_right]) 1);
16.216 +by (asm_simp_tac (intrel_ss addsimps [zminus,zadd,add_0_right]) 1);
16.217 by (REPEAT (ares_tac [add_commute] 1));
16.218 val zadd_zminus_inverse = result();
16.219
16.220 @@ -334,7 +332,7 @@
16.221 "[| k: nat; l: nat; m: nat; n: nat |] ==> \
16.222 \ (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)";
16.223 val add_commute' = read_instantiate [("m","l")] add_commute;
16.224 -by (SIMP_TAC (arith_ss addrews ([add_commute',add_assoc]@prems)) 1);
16.225 +by (simp_tac (arith_ss addsimps ([add_commute',add_assoc]@prems)) 1);
16.226 val zmult_congruent_lemma = result();
16.227
16.228 goal Integ.thy
16.229 @@ -348,7 +346,7 @@
16.230 by (rtac (zmult_congruent_lemma RS trans) 2);
16.231 by (rtac (zmult_congruent_lemma RS trans RS sym) 6);
16.232 by (typechk_tac [mult_type]);
16.233 -by (ASM_SIMP_TAC (arith_ss addrews [add_mult_distrib_left RS sym]) 2);
16.234 +by (asm_simp_tac (arith_ss addsimps [add_mult_distrib_left RS sym]) 2);
16.235 (*Proof that zmult is commutative on representatives*)
16.236 by (rtac add_cong 1);
16.237 by (rtac (add_commute RS trans) 2);
16.238 @@ -370,19 +368,19 @@
16.239 "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
16.240 \ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
16.241 \ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
16.242 -by (ASM_SIMP_TAC (ZF_ss addrews
16.243 +by (asm_simp_tac (ZF_ss addsimps
16.244 (prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1);
16.245 val zmult = result();
16.246
16.247 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0";
16.248 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.249 -by (ASM_SIMP_TAC (arith_ss addrews [zmult]) 1);
16.250 +by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
16.251 val zmult_0 = result();
16.252
16.253 goalw Integ.thy [integ_def,znat_def,one_def]
16.254 "!!z. z : integ ==> $#1 $* z = z";
16.255 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
16.256 -by (ASM_SIMP_TAC (arith_ss addrews [zmult,add_0_right]) 1);
16.257 +by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
16.258 val zmult_1 = result();
16.259
16.260 goalw Integ.thy [integ_def]
16.261 @@ -432,6 +430,5 @@
16.262 [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
16.263
16.264 val integ_ss =
16.265 - arith_ss addcongs integ_congs
16.266 - addrews ([zminus_zminus,zmagnitude_znat,zmagnitude_zminus_znat,
16.267 - zadd_0] @ integ_typechecks);
16.268 + arith_ss addsimps ([zminus_zminus, zmagnitude_znat,
16.269 + zmagnitude_zminus_znat, zadd_0] @ integ_typechecks);
17.1 --- a/src/ZF/ex/listn.ML Fri Sep 17 16:16:38 1993 +0200
17.2 +++ b/src/ZF/ex/listn.ML Fri Sep 17 16:52:10 1993 +0200
17.3 @@ -20,28 +20,24 @@
17.4 val type_intrs = nat_typechecks@List.intrs@[SigmaI]
17.5 val type_elims = [SigmaE2]);
17.6
17.7 -(*Could be generated automatically; requires use of fsplitD*)
17.8 -val listn_induct = standard
17.9 - (fsplitI RSN
17.10 - (2, fsplitI RSN
17.11 - (3, (read_instantiate [("P", "fsplit(R)")] ListN.induct) RS fsplitD)));
17.12 +val listn_induct = standard
17.13 + (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
17.14
17.15 val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
17.16 by (rtac (major RS List.induct) 1);
17.17 -by (ALLGOALS (ASM_SIMP_TAC list_ss));
17.18 +by (ALLGOALS (asm_simp_tac list_ss));
17.19 by (REPEAT (ares_tac ListN.intrs 1));
17.20 val list_into_listn = result();
17.21
17.22 goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
17.23 by (rtac iffI 1);
17.24 by (etac listn_induct 1);
17.25 -by (dtac fsplitD 2);
17.26 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [Pair_iff])));
17.27 -by (fast_tac (ZF_cs addSIs [list_into_listn]) 1);
17.28 +by (safe_tac (ZF_cs addSIs (list_typechecks @
17.29 + [length_Nil, length_Cons, list_into_listn])));
17.30 val listn_iff = result();
17.31
17.32 goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
17.33 by (rtac equality_iffI 1);
17.34 -by (SIMP_TAC (list_ss addrews [listn_iff,separation,image_singleton_iff]) 1);
17.35 +by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
17.36 val listn_image_eq = result();
17.37
18.1 --- a/src/ZF/ex/llist.ML Fri Sep 17 16:16:38 1993 +0200
18.2 +++ b/src/ZF/ex/llist.ML Fri Sep 17 16:52:10 1993 +0200
18.3 @@ -11,7 +11,6 @@
18.4
18.5 structure LList = Co_Datatype_Fun
18.6 (val thy = QUniv.thy;
18.7 - val thy = QUniv.thy;
18.8 val rec_specs =
18.9 [("llist", "quniv(A)",
18.10 [(["LNil"], "i"),
19.1 --- a/src/ZF/ex/misc.ML Fri Sep 17 16:16:38 1993 +0200
19.2 +++ b/src/ZF/ex/misc.ML Fri Sep 17 16:52:10 1993 +0200
19.3 @@ -62,7 +62,7 @@
19.4 \ X - lfp(X, %W. X - g``(Y - f``W)) ";
19.5 by (res_inst_tac [("P", "%u. ?v = X-u")]
19.6 (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
19.7 -by (SIMP_TAC (ZF_ss addrews [subset_refl, double_complement, Diff_subset,
19.8 +by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, Diff_subset,
19.9 gfun RS fun_is_rel RS image_subset]) 1);
19.10 val Banach_last_equation = result();
19.11
19.12 @@ -97,22 +97,29 @@
19.13 JAR 2 (1986), 287-327
19.14 *)
19.15
19.16 -val hom_ss = (*collecting the relevant lemmas*)
19.17 - ZF_ss addrews [comp_func,comp_func_apply,SigmaI,apply_type]
19.18 - addcongs (mk_congs Perm.thy ["op O"]);
19.19 +(*collecting the relevant lemmas*)
19.20 +val hom_ss = ZF_ss addsimps [comp_func,comp_func_apply,SigmaI,apply_funtype];
19.21
19.22 -(*This version uses a super application of SIMP_TAC; it is SLOW
19.23 - Expressing the goal by --> instead of ==> would make it slower still*)
19.24 -val [hom_eq] = goal Perm.thy
19.25 +(*The problem below is proving conditions of rewrites such as comp_func_apply;
19.26 + rewriting does not instantiate Vars; we must prove the conditions
19.27 + explicitly.*)
19.28 +fun hom_tac hyps =
19.29 + resolve_tac (TrueI::refl::iff_refl::hyps) ORELSE'
19.30 + (cut_facts_tac hyps THEN' fast_tac prop_cs);
19.31 +
19.32 +(*This version uses a super application of simp_tac*)
19.33 +goal Perm.thy
19.34 "(ALL A f B g. hom(A,f,B,g) = \
19.35 \ {H: A->B. f:A*A->A & g:B*B->B & \
19.36 -\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
19.37 +\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
19.38 \ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \
19.39 \ (K O J) : hom(A,f,C,h)";
19.40 -by (SIMP_TAC (hom_ss setauto K(fast_tac prop_cs) addrews [hom_eq]) 1);
19.41 +by (simp_tac (hom_ss setsolver hom_tac) 1);
19.42 +(*Also works but slower:
19.43 + by (asm_simp_tac (hom_ss setloop (K (safe_tac FOL_cs))) 1); *)
19.44 val comp_homs = result();
19.45
19.46 -(*This version uses meta-level rewriting, safe_tac and ASM_SIMP_TAC*)
19.47 +(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
19.48 val [hom_def] = goal Perm.thy
19.49 "(!! A f B g. hom(A,f,B,g) == \
19.50 \ {H: A->B. f:A*A->A & g:B*B->B & \
19.51 @@ -121,8 +128,8 @@
19.52 \ (K O J) : hom(A,f,C,h)";
19.53 by (rewtac hom_def);
19.54 by (safe_tac ZF_cs);
19.55 -by (ASM_SIMP_TAC hom_ss 1);
19.56 -by (ASM_SIMP_TAC hom_ss 1);
19.57 +by (asm_simp_tac hom_ss 1);
19.58 +by (asm_simp_tac hom_ss 1);
19.59 val comp_homs = result();
19.60
19.61
19.62 @@ -210,4 +217,31 @@
19.63 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
19.64 val pastre6 = result();
19.65
19.66 +(** Yet another example... **)
19.67 +
19.68 +goalw (merge_theories(Sum.thy,Perm.thy)) [bij_def,inj_def,surj_def]
19.69 + "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
19.70 +\ : bij(Pow(A+B), Pow(A)*Pow(B))";
19.71 +by (DO_GOAL
19.72 + [rtac IntI,
19.73 + DO_GOAL
19.74 + [rtac CollectI,
19.75 + fast_tac (ZF_cs addSIs [lam_type]),
19.76 + simp_tac ZF_ss,
19.77 + fast_tac (eq_cs addSEs [sumE]
19.78 + addEs [equalityD1 RS subsetD RS CollectD2,
19.79 + equalityD2 RS subsetD RS CollectD2])],
19.80 + DO_GOAL
19.81 + [rtac CollectI,
19.82 + fast_tac (ZF_cs addSIs [lam_type]),
19.83 + simp_tac ZF_ss,
19.84 + K(safe_tac ZF_cs),
19.85 + res_inst_tac [("x", "{Inl(u). u: ?U} Un {Inr(v). v: ?V}")] bexI,
19.86 + DO_GOAL
19.87 + [res_inst_tac [("t", "Pair")] subst_context2,
19.88 + fast_tac (sum_cs addSIs [equalityI]),
19.89 + fast_tac (sum_cs addSIs [equalityI])],
19.90 + DO_GOAL [fast_tac sum_cs]]] 1);
19.91 +val Pow_bij = result();
19.92 +
19.93 writeln"Reached end of file.";
20.1 --- a/src/ZF/ex/proplog.ML Fri Sep 17 16:16:38 1993 +0200
20.2 +++ b/src/ZF/ex/proplog.ML Fri Sep 17 16:52:10 1993 +0200
20.3 @@ -13,71 +13,66 @@
20.4
20.5 (*** prop_rec -- by Vset recursion ***)
20.6
20.7 -val prop_congs = mk_typed_congs Prop.thy
20.8 - [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
20.9 -
20.10 (** conversion rules **)
20.11
20.12 goal PropLog.thy "prop_rec(Fls,b,c,d) = b";
20.13 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
20.14 by (rewrite_goals_tac Prop.con_defs);
20.15 -by (SIMP_TAC rank_ss 1);
20.16 +by (simp_tac rank_ss 1);
20.17 val prop_rec_Fls = result();
20.18
20.19 goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
20.20 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
20.21 by (rewrite_goals_tac Prop.con_defs);
20.22 -by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
20.23 +by (simp_tac rank_ss 1);
20.24 val prop_rec_Var = result();
20.25
20.26 goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
20.27 \ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
20.28 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
20.29 by (rewrite_goals_tac Prop.con_defs);
20.30 -by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
20.31 +by (simp_tac rank_ss 1);
20.32 val prop_rec_Imp = result();
20.33
20.34 val prop_rec_ss =
20.35 - arith_ss addrews [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
20.36 + arith_ss addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
20.37
20.38 (*** Semantics of propositional logic ***)
20.39
20.40 (** The function is_true **)
20.41
20.42 goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False";
20.43 -by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]) 1);
20.44 +by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1);
20.45 val is_true_Fls = result();
20.46
20.47 goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t";
20.48 -by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]
20.49 - addsplits [expand_if]) 1);
20.50 +by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]
20.51 + setloop (split_tac [expand_if])) 1);
20.52 val is_true_Var = result();
20.53
20.54 goalw PropLog.thy [is_true_def]
20.55 "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
20.56 -by (SIMP_TAC (prop_rec_ss addsplits [expand_if]) 1);
20.57 +by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1);
20.58 val is_true_Imp = result();
20.59
20.60 (** The function hyps **)
20.61
20.62 goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0";
20.63 -by (SIMP_TAC prop_rec_ss 1);
20.64 +by (simp_tac prop_rec_ss 1);
20.65 val hyps_Fls = result();
20.66
20.67 goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}";
20.68 -by (SIMP_TAC prop_rec_ss 1);
20.69 +by (simp_tac prop_rec_ss 1);
20.70 val hyps_Var = result();
20.71
20.72 goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)";
20.73 -by (SIMP_TAC prop_rec_ss 1);
20.74 +by (simp_tac prop_rec_ss 1);
20.75 val hyps_Imp = result();
20.76
20.77 val prop_ss = prop_rec_ss
20.78 - addcongs Prop.congs
20.79 - addcongs (mk_congs PropLog.thy ["Fin", "thms", "op |=","is_true","hyps"])
20.80 - addrews Prop.intrs
20.81 - addrews [is_true_Fls, is_true_Var, is_true_Imp,
20.82 - hyps_Fls, hyps_Var, hyps_Imp];
20.83 + addsimps Prop.intrs
20.84 + addsimps [is_true_Fls, is_true_Var, is_true_Imp,
20.85 + hyps_Fls, hyps_Var, hyps_Imp];
20.86
20.87 (*** Proof theory of propositional logic ***)
20.88
20.89 @@ -162,10 +157,10 @@
20.90 val thms_notE = standard (thms_MP RS thms_FlsE);
20.91
20.92 (*Soundness of the rules wrt truth-table semantics*)
20.93 -val [major] = goalw PropThms.thy [sat_def] "H |- p ==> H |= p";
20.94 -by (rtac (major RS PropThms.induct) 1);
20.95 +goalw PropThms.thy [sat_def] "!!H. H |- p ==> H |= p";
20.96 +by (etac PropThms.induct 1);
20.97 by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
20.98 -by (ALLGOALS (SIMP_TAC prop_ss));
20.99 +by (ALLGOALS (asm_simp_tac prop_ss));
20.100 val soundness = result();
20.101
20.102 (*** Towards the completeness proof ***)
20.103 @@ -194,7 +189,7 @@
20.104 "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
20.105 by (rtac (expand_if RS iffD2) 1);
20.106 by (rtac (major RS Prop.induct) 1);
20.107 -by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [thms_I, thms_H])));
20.108 +by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
20.109 by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2,
20.110 weaken_right, Imp_Fls]
20.111 addSEs [Fls_Imp]) 1);
20.112 @@ -235,10 +230,10 @@
20.113 val [major] = goal PropThms.thy
20.114 "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
20.115 by (rtac (major RS Prop.induct) 1);
20.116 -by (SIMP_TAC prop_ss 1);
20.117 -by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
20.118 +by (simp_tac prop_ss 1);
20.119 +by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
20.120 by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
20.121 -by (ASM_SIMP_TAC prop_ss 1);
20.122 +by (asm_simp_tac prop_ss 1);
20.123 by (fast_tac ZF_cs 1);
20.124 val hyps_Diff = result();
20.125
20.126 @@ -247,10 +242,10 @@
20.127 val [major] = goal PropThms.thy
20.128 "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
20.129 by (rtac (major RS Prop.induct) 1);
20.130 -by (SIMP_TAC prop_ss 1);
20.131 -by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
20.132 +by (simp_tac prop_ss 1);
20.133 +by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
20.134 by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
20.135 -by (ASM_SIMP_TAC prop_ss 1);
20.136 +by (asm_simp_tac prop_ss 1);
20.137 by (fast_tac ZF_cs 1);
20.138 val hyps_cons = result();
20.139
20.140 @@ -269,9 +264,9 @@
20.141 val [major] = goal PropThms.thy
20.142 "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
20.143 by (rtac (major RS Prop.induct) 1);
20.144 -by (ASM_SIMP_TAC (prop_ss addrews [Fin_0I, Fin_consI, UN_I]
20.145 - addsplits [expand_if]) 2);
20.146 -by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [Un_0, Fin_0I, Fin_UnI])));
20.147 +by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I]
20.148 + setloop (split_tac [expand_if])) 2);
20.149 +by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
20.150 val hyps_finite = result();
20.151
20.152 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
20.153 @@ -281,7 +276,7 @@
20.154 val [premp,sat] = goal PropThms.thy
20.155 "[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
20.156 by (rtac (premp RS hyps_finite RS Fin_induct) 1);
20.157 -by (SIMP_TAC (prop_ss addrews [premp, sat, sat_thms_p, Diff_0]) 1);
20.158 +by (simp_tac (prop_ss addsimps [premp, sat, sat_thms_p, Diff_0]) 1);
20.159 by (safe_tac ZF_cs);
20.160 (*Case hyps(p,t)-cons(#v,Y) |- p *)
20.161 by (rtac thms_excluded_middle_rule 1);
20.162 @@ -309,7 +304,7 @@
20.163
20.164 (*A semantic analogue of the Deduction Theorem*)
20.165 goalw PropThms.thy [sat_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
20.166 -by (SIMP_TAC prop_ss 1);
20.167 +by (simp_tac prop_ss 1);
20.168 by (fast_tac ZF_cs 1);
20.169 val sat_Imp = result();
20.170
21.1 --- a/src/ZF/ex/ramsey.ML Fri Sep 17 16:16:38 1993 +0200
21.2 +++ b/src/ZF/ex/ramsey.ML Fri Sep 17 16:52:10 1993 +0200
21.3 @@ -20,9 +20,6 @@
21.4
21.5 open Ramsey;
21.6
21.7 -val ramsey_congs = mk_congs Ramsey.thy ["Atleast"];
21.8 -val ramsey_ss = arith_ss addcongs ramsey_congs;
21.9 -
21.10 (*** Cliques and Independent sets ***)
21.11
21.12 goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
21.13 @@ -95,11 +92,12 @@
21.14 \ Atleast(m,A) | Atleast(n,B)";
21.15 by (nat_ind_tac "m" prems 1);
21.16 by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
21.17 -by (ASM_SIMP_TAC ramsey_ss 1);
21.18 +by (asm_simp_tac arith_ss 1);
21.19 by (rtac ballI 1);
21.20 +by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*)
21.21 by (nat_ind_tac "n" [] 1);
21.22 by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
21.23 -by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
21.24 +by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
21.25 by (safe_tac ZF_cs);
21.26 by (etac (Atleast_succD RS bexE) 1);
21.27 by (etac UnE 1);
21.28 @@ -118,7 +116,7 @@
21.29 (*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
21.30 by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
21.31 (*proving the condition*)
21.32 -by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
21.33 +by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
21.34 by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
21.35 val pigeon2_lemma = result();
21.36
21.37 @@ -147,7 +145,7 @@
21.38 "[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \
21.39 \ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
21.40 by (rtac (nat_succI RS pigeon2) 1);
21.41 -by (SIMP_TAC (ramsey_ss addrews prems) 3);
21.42 +by (simp_tac (arith_ss addsimps prems) 3);
21.43 by (rtac Atleast_superset 3);
21.44 by (REPEAT (resolve_tac prems 1));
21.45 by (fast_tac ZF_cs 1);
22.1 --- a/src/ZF/ex/termfn.ML Fri Sep 17 16:16:38 1993 +0200
22.2 +++ b/src/ZF/ex/termfn.ML Fri Sep 17 16:52:10 1993 +0200
22.3 @@ -18,11 +18,11 @@
22.4 "[| l: list(A); Ord(i) |] ==> \
22.5 \ rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
22.6 by (rtac (major RS List.induct) 1);
22.7 -by (SIMP_TAC list_ss 1);
22.8 +by (simp_tac list_ss 1);
22.9 by (rtac impI 1);
22.10 by (forward_tac [rank_Cons1 RS Ord_trans] 1);
22.11 by (dtac (rank_Cons2 RS Ord_trans) 2);
22.12 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [ordi, VsetI])));
22.13 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [ordi, VsetI])));
22.14 val map_lemma = result();
22.15
22.16 (*Typing premise is necessary to invoke map_lemma*)
22.17 @@ -31,10 +31,8 @@
22.18 \ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
22.19 by (rtac (term_rec_def RS def_Vrec RS trans) 1);
22.20 by (rewrite_goals_tac Term.con_defs);
22.21 -val term_rec_ss = ZF_ss
22.22 - addcongs (mk_typed_congs TermFn.thy [("d", "[i,i,i]=>i")])
22.23 - addrews [Ord_rank, rank_pair2, prem RS map_lemma];
22.24 -by (SIMP_TAC term_rec_ss 1);
22.25 +val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
22.26 +by (simp_tac term_rec_ss 1);
22.27 val term_rec = result();
22.28
22.29 (*Slightly odd typing condition on r in the second premise!*)
22.30 @@ -49,7 +47,7 @@
22.31 by (rtac (term_rec RS ssubst) 1);
22.32 by (REPEAT (ares_tac prems 1));
22.33 by (etac List.induct 1);
22.34 -by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [term_rec])));
22.35 +by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
22.36 by (etac CollectE 1);
22.37 by (REPEAT (ares_tac [ConsI, UN_I] 1));
22.38 val term_rec_type = result();
22.39 @@ -122,31 +120,27 @@
22.40
22.41 (*map_type2 and term_map_type2 instantiate variables*)
22.42 val term_ss = list_ss
22.43 - addcongs (Term.congs @
22.44 - mk_congs TermFn.thy ["term_rec","term_map","term_size",
22.45 - "reflect","preorder"])
22.46 - addrews [term_rec, term_map, term_size, reflect,
22.47 - preorder]
22.48 - setauto type_auto_tac (list_typechecks@term_typechecks);
22.49 + addsimps [term_rec, term_map, term_size, reflect, preorder]
22.50 + setsolver type_auto_tac (list_typechecks@term_typechecks);
22.51
22.52
22.53 (** theorems about term_map **)
22.54
22.55 goal TermFn.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
22.56 by (etac term_induct_eqn 1);
22.57 -by (ASM_SIMP_TAC (term_ss addrews [map_ident]) 1);
22.58 +by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
22.59 val term_map_ident = result();
22.60
22.61 goal TermFn.thy
22.62 "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
22.63 by (etac term_induct_eqn 1);
22.64 -by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
22.65 +by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
22.66 val term_map_compose = result();
22.67
22.68 goal TermFn.thy
22.69 "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
22.70 by (etac term_induct_eqn 1);
22.71 -by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose]) 1);
22.72 +by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
22.73 val term_map_reflect = result();
22.74
22.75
22.76 @@ -155,18 +149,18 @@
22.77 goal TermFn.thy
22.78 "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
22.79 by (etac term_induct_eqn 1);
22.80 -by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
22.81 +by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
22.82 val term_size_term_map = result();
22.83
22.84 goal TermFn.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
22.85 by (etac term_induct_eqn 1);
22.86 -by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose,
22.87 - list_add_rev]) 1);
22.88 +by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
22.89 + list_add_rev]) 1);
22.90 val term_size_reflect = result();
22.91
22.92 goal TermFn.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
22.93 by (etac term_induct_eqn 1);
22.94 -by (ASM_SIMP_TAC (term_ss addrews [length_flat, map_compose]) 1);
22.95 +by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
22.96 val term_size_length = result();
22.97
22.98
22.99 @@ -174,8 +168,8 @@
22.100
22.101 goal TermFn.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
22.102 by (etac term_induct_eqn 1);
22.103 -by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib, map_compose,
22.104 - map_ident, rev_rev_ident]) 1);
22.105 +by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
22.106 + map_ident, rev_rev_ident]) 1);
22.107 val reflect_reflect_ident = result();
22.108
22.109
22.110 @@ -184,7 +178,7 @@
22.111 goal TermFn.thy
22.112 "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
22.113 by (etac term_induct_eqn 1);
22.114 -by (ASM_SIMP_TAC (term_ss addrews [map_compose, map_flat]) 1);
22.115 +by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
22.116 val preorder_term_map = result();
22.117
22.118 (** preorder(reflect(t)) = rev(postorder(t)) **)
23.1 --- a/src/ZF/ex/tf_fn.ML Fri Sep 17 16:16:38 1993 +0200
23.2 +++ b/src/ZF/ex/tf_fn.ML Fri Sep 17 16:52:10 1993 +0200
23.3 @@ -16,33 +16,29 @@
23.4
23.5 (*** TF_rec -- by Vset recursion ***)
23.6
23.7 -(*Used only to verify TF_rec*)
23.8 -val TF_congs = mk_typed_congs TF.thy
23.9 - [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
23.10 -
23.11 (** conversion rules **)
23.12
23.13 goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
23.14 by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
23.15 by (rewrite_goals_tac TF.con_defs);
23.16 -by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
23.17 +by (simp_tac rank_ss 1);
23.18 val TF_rec_Tcons = result();
23.19
23.20 goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
23.21 by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
23.22 by (rewrite_goals_tac TF.con_defs);
23.23 -by (SIMP_TAC rank_ss 1);
23.24 +by (simp_tac rank_ss 1);
23.25 val TF_rec_Fnil = result();
23.26
23.27 goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
23.28 \ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
23.29 by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
23.30 by (rewrite_goals_tac TF.con_defs);
23.31 -by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
23.32 +by (simp_tac rank_ss 1);
23.33 val TF_rec_Fcons = result();
23.34
23.35 (*list_ss includes list operations as well as arith_ss*)
23.36 -val TF_rec_ss = list_ss addrews
23.37 +val TF_rec_ss = list_ss addsimps
23.38 [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
23.39
23.40 (** Type checking **)
23.41 @@ -56,7 +52,7 @@
23.42 \ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
23.43 \ |] ==> TF_rec(z,b,c,d) : C(z)";
23.44 by (rtac (major RS TF.induct) 1);
23.45 -by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
23.46 +by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
23.47 val TF_rec_type = result();
23.48
23.49 (*Mutually recursive version*)
23.50 @@ -70,7 +66,7 @@
23.51 \ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
23.52 by (rewtac Ball_def);
23.53 by (rtac TF.mutual_induct 1);
23.54 -by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
23.55 +by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
23.56 val tree_forest_rec_type = result();
23.57
23.58
23.59 @@ -159,10 +155,6 @@
23.60 [TconsI, FnilI, FconsI, treeI, forestI,
23.61 list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
23.62
23.63 -val TF_congs = TF.congs @
23.64 - mk_congs TF_Fn.thy
23.65 - ["TF_rec", "list_of_TF", "TF_of_list", "TF_map", "TF_size", "TF_preorder"];
23.66 -
23.67 val TF_rewrites =
23.68 [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
23.69 list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
23.70 @@ -171,8 +163,8 @@
23.71 TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
23.72 TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
23.73
23.74 -val TF_ss = list_ss addcongs TF_congs
23.75 - addrews (TF_rewrites@TF_typechecks);
23.76 +val TF_ss = list_ss addsimps TF_rewrites
23.77 + setsolver type_auto_tac (list_typechecks@TF_typechecks);
23.78
23.79 (** theorems about list_of_TF and TF_of_list **)
23.80
23.81 @@ -188,26 +180,26 @@
23.82
23.83 goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
23.84 by (etac forest_induct 1);
23.85 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
23.86 +by (ALLGOALS (asm_simp_tac TF_ss));
23.87 val forest_iso = result();
23.88
23.89 goal TF_Fn.thy
23.90 "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
23.91 by (etac List.induct 1);
23.92 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
23.93 +by (ALLGOALS (asm_simp_tac TF_ss));
23.94 val tree_list_iso = result();
23.95
23.96 (** theorems about TF_map **)
23.97
23.98 goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
23.99 by (etac TF.induct 1);
23.100 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
23.101 +by (ALLGOALS (asm_simp_tac TF_ss));
23.102 val TF_map_ident = result();
23.103
23.104 goal TF_Fn.thy
23.105 "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
23.106 by (etac TF.induct 1);
23.107 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
23.108 +by (ALLGOALS (asm_simp_tac TF_ss));
23.109 val TF_map_compose = result();
23.110
23.111 (** theorems about TF_size **)
23.112 @@ -215,13 +207,13 @@
23.113 goal TF_Fn.thy
23.114 "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
23.115 by (etac TF.induct 1);
23.116 -by (ALLGOALS (ASM_SIMP_TAC TF_ss));
23.117 +by (ALLGOALS (asm_simp_tac TF_ss));
23.118 val TF_size_TF_map = result();
23.119
23.120 goal TF_Fn.thy
23.121 "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
23.122 by (etac TF.induct 1);
23.123 -by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [length_app])));
23.124 +by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
23.125 val TF_size_length = result();
23.126
23.127 (** theorems about TF_preorder **)
23.128 @@ -229,5 +221,5 @@
23.129 goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
23.130 \ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
23.131 by (etac TF.induct 1);
23.132 -by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [map_app_distrib])));
23.133 +by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
23.134 val TF_preorder_TF_map = result();