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.
--- a/src/ZF/ex/BT_Fn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/BT_Fn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -12,28 +12,24 @@
(** bt_rec -- by Vset recursion **)
-(*Used to verify bt_rec*)
-val bt_rec_ss = ZF_ss
- addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")])
- addrews BT.case_eqns;
-
goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Br1 = result();
goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Br2 = result();
goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC bt_rec_ss 1);
+by (simp_tac (ZF_ss addsimps BT.case_eqns) 1);
val bt_rec_Lf = result();
goal BT_Fn.thy
"bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1);
+by (simp_tac (ZF_ss addsimps
+ (BT.case_eqns @ [Vset_rankI, rank_Br1, rank_Br2])) 1);
val bt_rec_Br = result();
(*Type checking -- proved by induction, as usual*)
@@ -44,7 +40,7 @@
\ h(x,y,z,r,s): C(Br(x,y,z)) \
\ |] ==> bt_rec(t,c,h) : C(t)";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
(prems@[bt_rec_Lf,bt_rec_Br]))));
val bt_rec_type = result();
@@ -98,15 +94,10 @@
val bt_typechecks =
[LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
-val bt_congs =
- BT.congs @
- mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"];
-
val bt_ss = arith_ss
- addcongs bt_congs
- addrews BT.case_eqns
- addrews bt_typechecks
- addrews [bt_rec_Lf, bt_rec_Br,
+ addsimps BT.case_eqns
+ addsimps bt_typechecks
+ addsimps [bt_rec_Lf, bt_rec_Br,
n_nodes_Lf, n_nodes_Br,
n_leaves_Lf, n_leaves_Br,
bt_reflect_Lf, bt_reflect_Br];
@@ -117,14 +108,14 @@
val prems = goal BT_Fn.thy
"t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC bt_ss));
+by (ALLGOALS (asm_simp_tac bt_ss));
by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
val n_leaves_reflect = result();
val prems = goal BT_Fn.thy
"t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right])));
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
val n_leaves_nodes = result();
(*** theorems about bt_reflect ***)
@@ -132,7 +123,7 @@
val prems = goal BT_Fn.thy
"t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC bt_ss));
+by (ALLGOALS (asm_simp_tac bt_ss));
val bt_reflect_bt_reflect_ident = result();
--- a/src/ZF/ex/BinFn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/BinFn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -14,20 +14,19 @@
goal BinFn.thy "bin_rec(Plus,a,b,h) = a";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Bin.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val bin_rec_Plus = result();
goal BinFn.thy "bin_rec(Minus,a,b,h) = b";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Bin.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val bin_rec_Minus = result();
goal BinFn.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Bin.con_defs);
-by (SIMP_TAC (rank_ss addcongs
- (mk_typed_congs BinFn.thy [("h", "[i,i,i]=>i")])) 1);
+by (simp_tac rank_ss 1);
val bin_rec_Bcons = result();
(*Type checking*)
@@ -38,7 +37,7 @@
\ |] ==> bin_rec(w,a,b,h) : C(w)";
by (bin_ind_tac "w" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC (ZF_ss addrews (prems@[bin_rec_Plus,bin_rec_Minus,
+ (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
bin_rec_Bcons]))));
val bin_rec_type = result();
@@ -106,13 +105,8 @@
[integ_of_bin_type, bin_succ_type, bin_pred_type,
bin_minus_type, bin_add_type, bin_mult_type];
-val bin_congs = mk_congs BinFn.thy
- ["bin_rec","op $$","integ_of_bin","bin_succ","bin_pred",
- "bin_minus","bin_add","bin_mult"];
-
val bin_ss = integ_ss
- addcongs (bin_congs@bool_congs)
- addrews([bool_1I, bool_0I,
+ addsimps([bool_1I, bool_0I,
bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
@@ -127,7 +121,7 @@
"!!z v. [| z $+ v = z' $+ v'; \
\ z: integ; z': integ; v: integ; v': integ; w: integ |] \
\ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
-by (ASM_SIMP_TAC (integ_ss addrews ([zadd_assoc RS sym])) 1);
+by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
val zadd_assoc_cong = result();
goal Integ.thy
@@ -136,7 +130,8 @@
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
val zadd_assoc_swap = result();
-val [zadd_cong] = mk_congs Integ.thy ["op $+"];
+val zadd_cong =
+ read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2;
val zadd_kill = (refl RS zadd_cong);
val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
@@ -151,28 +146,28 @@
val zadd_swap_pairs = result();
-val carry_ss = bin_ss addrews
+val carry_ss = bin_ss addsimps
(bin_recs bin_succ_def @ bin_recs bin_pred_def);
goal BinFn.thy
"!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
-by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
by (etac boolE 1);
-by (ALLGOALS (ASM_SIMP_TAC (carry_ss addrews [zadd_assoc])));
+by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc])));
by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
val integ_of_bin_succ = result();
goal BinFn.thy
"!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
-by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
by (etac boolE 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (carry_ss addrews [zadd_assoc RS sym,
+ (asm_simp_tac
+ (carry_ss addsimps [zadd_assoc RS sym,
zadd_zminus_inverse, zadd_zminus_inverse2])));
by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
val integ_of_bin_pred = result();
@@ -183,68 +178,68 @@
(*** bin_minus: (unary!) negation of binary integers ***)
val bin_minus_ss =
- bin_ss addrews (bin_recs bin_minus_def @
+ bin_ss addsimps (bin_recs bin_minus_def @
[integ_of_bin_succ, integ_of_bin_pred]);
goal BinFn.thy
"!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC (bin_minus_ss addrews [zminus_0]) 1);
-by (SIMP_TAC (bin_minus_ss addrews [zadd_0_right]) 1);
+by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1);
+by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1);
by (etac boolE 1);
by (ALLGOALS
- (ASM_SIMP_TAC (bin_minus_ss addrews [zminus_zadd_distrib, zadd_assoc])));
+ (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
val integ_of_bin_minus = result();
(*** bin_add: binary addition ***)
goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
-by (ASM_SIMP_TAC bin_ss 1);
+by (asm_simp_tac bin_ss 1);
val bin_add_Plus = result();
goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
-by (ASM_SIMP_TAC bin_ss 1);
+by (asm_simp_tac bin_ss 1);
val bin_add_Minus = result();
goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
-by (SIMP_TAC bin_ss 1);
+by (simp_tac bin_ss 1);
val bin_add_Bcons_Plus = result();
goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
-by (SIMP_TAC bin_ss 1);
+by (simp_tac bin_ss 1);
val bin_add_Bcons_Minus = result();
goalw BinFn.thy [bin_add_def]
"!!w y. [| w: bin; y: bool |] ==> \
\ bin_add(v$$x, w$$y) = \
\ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
-by (ASM_SIMP_TAC bin_ss 1);
+by (asm_simp_tac bin_ss 1);
val bin_add_Bcons_Bcons = result();
val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
integ_of_bin_succ, integ_of_bin_pred];
-val bin_add_ss = bin_ss addrews ([bool_subset_nat RS subsetD] @ bin_add_rews);
+val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews);
goal BinFn.thy
"!!v. v: bin ==> \
\ ALL w: bin. integ_of_bin(bin_add(v,w)) = \
\ integ_of_bin(v) $+ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC bin_add_ss 1);
-by (SIMP_TAC bin_add_ss 1);
+by (simp_tac bin_add_ss 1);
+by (simp_tac bin_add_ss 1);
by (rtac ballI 1);
by (bin_ind_tac "wa" [] 1);
-by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_0_right]) 1);
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1);
+by (asm_simp_tac bin_add_ss 1);
by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
by (etac boolE 1);
-by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc, zadd_swap_pairs]) 2);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2);
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
by (etac boolE 1);
-by (ALLGOALS (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc,zadd_swap_pairs])));
+by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
typechecks) 1));
val integ_of_bin_add_lemma = result();
@@ -255,7 +250,7 @@
(*** bin_add: binary multiplication ***)
val bin_mult_ss =
- bin_ss addrews (bin_recs bin_mult_def @
+ bin_ss addsimps (bin_recs bin_mult_def @
[integ_of_bin_minus, integ_of_bin_add]);
@@ -265,12 +260,12 @@
\ integ_of_bin(v) $* integ_of_bin(w)";
by (cut_facts_tac prems 1);
by (bin_ind_tac "v" [major] 1);
-by (SIMP_TAC (bin_mult_ss addrews [zmult_0]) 1);
-by (SIMP_TAC (bin_mult_ss addrews [zmult_1,zmult_zminus]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1);
by (etac boolE 1);
-by (ASM_SIMP_TAC (bin_mult_ss addrews [zadd_zmult_distrib]) 2);
-by (ASM_SIMP_TAC
- (bin_mult_ss addrews [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2);
+by (asm_simp_tac
+ (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
typechecks) 1));
val integ_of_bin_mult = result();
@@ -283,19 +278,19 @@
val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
goal BinFn.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_succ_Bcons1 = result();
goal BinFn.thy "bin_succ(w$$0) = w$$1";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_succ_Bcons0 = result();
goal BinFn.thy "bin_pred(w$$1) = w$$0";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_pred_Bcons1 = result();
goal BinFn.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_pred_Bcons0 = result();
(** extra rules for bin_minus **)
@@ -303,28 +298,28 @@
val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
goal BinFn.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
-by (SIMP_TAC bin_minus_ss 1);
+by (simp_tac bin_minus_ss 1);
val bin_minus_Bcons1 = result();
goal BinFn.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
-by (SIMP_TAC bin_minus_ss 1);
+by (simp_tac bin_minus_ss 1);
val bin_minus_Bcons0 = result();
(** extra rules for bin_add **)
goal BinFn.thy
"!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac bin_add_ss 1);
val bin_add_Bcons_Bcons11 = result();
goal BinFn.thy
"!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac bin_add_ss 1);
val bin_add_Bcons_Bcons10 = result();
goal BinFn.thy
"!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac bin_add_ss 1);
val bin_add_Bcons_Bcons0 = result();
(** extra rules for bin_mult **)
@@ -332,24 +327,18 @@
val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
goal BinFn.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
-by (SIMP_TAC bin_mult_ss 1);
+by (simp_tac bin_mult_ss 1);
val bin_mult_Bcons1 = result();
goal BinFn.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
-by (SIMP_TAC bin_mult_ss 1);
+by (simp_tac bin_mult_ss 1);
val bin_mult_Bcons0 = result();
(*** The computation simpset ***)
-val bin_comp_ss = carry_ss addrews
- [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, bin_add_Bcons_Minus,
- bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11]
- setauto (type_auto_tac bin_typechecks0);
-
val bin_comp_ss = integ_ss
- addcongs bin_congs
- addrews [bin_succ_Plus, bin_succ_Minus,
+ addsimps [bin_succ_Plus, bin_succ_Minus,
bin_succ_Bcons1, bin_succ_Bcons0,
bin_pred_Plus, bin_pred_Minus,
bin_pred_Bcons1, bin_pred_Bcons0,
@@ -360,7 +349,7 @@
bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
bin_mult_Plus, bin_mult_Minus,
bin_mult_Bcons1, bin_mult_Bcons0]
- setauto (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+ setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
(*** Examples of performing binary arithmetic by simplification ***)
@@ -370,7 +359,7 @@
(* 13+19 = 32 *)
goal BinFn.thy
"bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*1.9 secs*)
+by (simp_tac bin_comp_ss 1); (*0.6 secs*)
result();
bin_add(binary_of_int 13, binary_of_int 19);
@@ -380,7 +369,7 @@
"bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
\ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
\ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*8.9 secs*)
+by (simp_tac bin_comp_ss 1); (*2.6 secs*)
result();
bin_add(binary_of_int 1234, binary_of_int 5678);
@@ -390,7 +379,7 @@
"bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
\ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*7.4 secs*)
+by (simp_tac bin_comp_ss 1); (*2.3 secs*)
result();
bin_add(binary_of_int 1359, binary_of_int ~2468);
@@ -400,7 +389,7 @@
"bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
\ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
\ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*13.7 secs*)
+by (simp_tac bin_comp_ss 1); (*3.9 secs*)
result();
bin_add(binary_of_int 93746, binary_of_int ~46375);
@@ -409,7 +398,7 @@
goal BinFn.thy
"bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
\ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*2.8 secs*)
+by (simp_tac bin_comp_ss 1); (*0.6 secs*)
result();
bin_minus(binary_of_int 65745);
@@ -418,7 +407,7 @@
goal BinFn.thy
"bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
\ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
-by (SIMP_TAC bin_comp_ss 1); (*3.3 secs*)
+by (simp_tac bin_comp_ss 1); (*0.7 secs*)
result();
bin_minus(binary_of_int ~54321);
@@ -426,7 +415,7 @@
(* 13*19 = 247 *)
goal BinFn.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
\ Plus$$1$$1$$1$$1$$0$$1$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*4.4 secs*)
+by (simp_tac bin_comp_ss 1); (*1.5 secs*)
result();
bin_mult(binary_of_int 13, binary_of_int 19);
@@ -435,7 +424,7 @@
goal BinFn.thy
"bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
\ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*9.2 secs*)
+by (simp_tac bin_comp_ss 1); (*2.6 secs*)
result();
bin_mult(binary_of_int ~84, binary_of_int 51);
@@ -445,19 +434,17 @@
"bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
\ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
\ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
-by (SIMP_TAC bin_comp_ss 1); (*38.4 secs*)
+by (simp_tac bin_comp_ss 1); (*9.8 secs*)
result();
bin_mult(binary_of_int 255, binary_of_int 255);
-(***************** TOO SLOW TO INCLUDE IN TEST RUNS
(* 1359 * ~2468 = ~3354012 *)
goal BinFn.thy
"bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
\ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*54.8 secs*)
+by (simp_tac bin_comp_ss 1); (*13.7 secs*)
result();
-****************)
bin_mult(binary_of_int 1359, binary_of_int ~2468);
--- a/src/ZF/ex/Enum.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/Enum.ML Fri Sep 17 16:52:10 1993 +0200
@@ -28,6 +28,6 @@
val type_elims = []);
goal Enum.thy "~ con59=con60";
-by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1); (*2.3 secs*)
+by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*)
result();
--- a/src/ZF/ex/Equiv.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/Equiv.ML Fri Sep 17 16:52:10 1993 +0200
@@ -190,7 +190,7 @@
by (safe_tac ZF_cs);
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
+by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
congruent2_implies_congruent]) 1);
by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
by (fast_tac ZF_cs 1);
@@ -200,7 +200,7 @@
"[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \
\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
by (cut_facts_tac prems 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
+by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
congruent2_implies_congruent,
congruent2_implies_congruent_UN]) 1);
val UN_equiv_class2 = result();
@@ -235,7 +235,7 @@
val [equivA,commute,congt] = goal Equiv.thy
"[| equiv(A,r); \
-\ !! y z w. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
+\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
\ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
\ |] ==> congruent2(r,b)";
by (resolve_tac [equivA RS congruent2I] 1);
@@ -259,7 +259,7 @@
by (safe_tac ZF_cs);
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [congt RS (equivA RS UN_equiv_class)]) 1);
+by (asm_simp_tac (ZF_ss addsimps [congt RS (equivA RS UN_equiv_class)]) 1);
by (rtac (commute RS trans) 1);
by (rtac (commute RS trans RS sym) 3);
by (rtac sym 5);
--- a/src/ZF/ex/Integ.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/Integ.ML Fri Sep 17 16:52:10 1993 +0200
@@ -12,16 +12,18 @@
$+ and $* are monotonic wrt $<
*)
-open Integ;
+val add_cong =
+ read_instantiate_sg (sign_of Arith.thy) [("t","op #+")] subst_context2;
-val [add_cong] = mk_congs Arith.thy ["op #+"];
+
+open Integ;
(*** Proving that intrel is an equivalence relation ***)
val prems = goal Arith.thy
"[| m #+ n = m' #+ n'; m: nat; m': nat |] \
\ ==> m #+ (n #+ k) = m' #+ (n' #+ k)";
-by (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym] @ prems)) 1);
+by (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym] @ prems)) 1);
val add_assoc_cong = result();
val prems = goal Arith.thy
@@ -31,6 +33,7 @@
val add_assoc_swap = result();
val add_kill = (refl RS add_cong);
+
val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans);
(*By luck, requires no typing premises for y1, y2,y3*)
@@ -90,22 +93,17 @@
val equiv_intrel = result();
-val integ_congs = mk_congs Integ.thy
- ["znat", "zminus", "znegative", "zmagnitude", "op $+", "op $-", "op $*"];
-
-val intrel_ss0 = arith_ss addcongs integ_congs;
+val intrel_ss =
+ arith_ss addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
-val intrel_ss =
- intrel_ss0 addrews [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
-
-(*More than twice as fast as simplifying with intrel_ss*)
+(*Roughly twice as fast as simplifying with intrel_ss*)
fun INTEG_SIMP_TAC ths =
- let val ss = intrel_ss0 addrews ths
+ let val ss = arith_ss addsimps ths
in fn i =>
- EVERY [ASM_SIMP_TAC ss i,
+ EVERY [asm_simp_tac ss i,
rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i,
typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks),
- ASM_SIMP_TAC ss i]
+ asm_simp_tac ss i]
end;
@@ -130,7 +128,7 @@
goalw Integ.thy [congruent_def]
"congruent(intrel, split(%x y. intrel``{<y,x>}))";
by (safe_tac intrel_cs);
-by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
+by (ALLGOALS (asm_simp_tac intrel_ss));
by (etac (box_equals RS sym) 1);
by (REPEAT (ares_tac [add_commute] 1));
val zminus_congruent = result();
@@ -150,7 +148,7 @@
by (REPEAT (ares_tac prems 1));
by (REPEAT (etac SigmaE 1));
by (etac rev_mp 1);
-by (ASM_SIMP_TAC ZF_ss 1);
+by (asm_simp_tac ZF_ss 1);
by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel]
addSEs [box_equals RS sym, add_commute,
make_elim eq_equiv_class]) 1);
@@ -158,17 +156,17 @@
val prems = goalw Integ.thy [zminus_def]
"[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (ASM_SIMP_TAC
- (ZF_ss addrews (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
+by (asm_simp_tac
+ (ZF_ss addsimps (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
val zminus = result();
goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [zminus] addcongs integ_congs) 1);
+by (asm_simp_tac (ZF_ss addsimps [zminus]) 1);
val zminus_zminus = result();
goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0";
-by (SIMP_TAC (arith_ss addrews [zminus]) 1);
+by (simp_tac (arith_ss addsimps [zminus]) 1);
val zminus_0 = result();
@@ -179,13 +177,13 @@
by (safe_tac intrel_cs);
by (rtac (add_not_less_self RS notE) 1);
by (etac ssubst 3);
-by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 3);
+by (asm_simp_tac (arith_ss addsimps [add_0_right]) 3);
by (REPEAT (assume_tac 1));
val not_znegative_znat = result();
val [nnat] = goalw Integ.thy [znegative_def, znat_def]
"n: nat ==> znegative($~ $# succ(n))";
-by (SIMP_TAC (intrel_ss addrews [zminus,nnat]) 1);
+by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
by (REPEAT
(resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
refl RS intrelI RS imageI, consI1, nnat, nat_0I,
@@ -198,19 +196,19 @@
goalw Integ.thy [congruent_def]
"congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))";
by (safe_tac intrel_cs);
-by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
+by (ALLGOALS (asm_simp_tac intrel_ss));
by (etac rev_mp 1);
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
by (REPEAT (assume_tac 1));
-by (ASM_SIMP_TAC (arith_ss addrews [add_succ_right,succ_inject_iff]) 3);
-by (ASM_SIMP_TAC
- (arith_ss addrews [diff_add_inverse,diff_add_0,add_0_right]) 2);
-by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_succ_right,succ_inject_iff]) 3);
+by (asm_simp_tac
+ (arith_ss addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2);
+by (asm_simp_tac (arith_ss addsimps [add_0_right]) 1);
by (rtac impI 1);
by (etac subst 1);
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
by (REPEAT (assume_tac 1));
-by (ASM_SIMP_TAC (arith_ss addrews [diff_add_inverse,diff_add_0]) 1);
+by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
val zmagnitude_congruent = result();
(*Resolve th against the corresponding facts for zmagnitude*)
@@ -225,18 +223,18 @@
val prems = goalw Integ.thy [zmagnitude_def]
"[| x: nat; y: nat |] ==> \
\ zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)";
-by (ASM_SIMP_TAC
- (ZF_ss addrews (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
+by (asm_simp_tac
+ (ZF_ss addsimps (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
val zmagnitude = result();
val [nnat] = goalw Integ.thy [znat_def]
"n: nat ==> zmagnitude($# n) = n";
-by (SIMP_TAC (intrel_ss addrews [zmagnitude,nnat]) 1);
+by (simp_tac (intrel_ss addsimps [zmagnitude,nnat]) 1);
val zmagnitude_znat = result();
val [nnat] = goalw Integ.thy [znat_def]
"n: nat ==> zmagnitude($~ $# n) = n";
-by (SIMP_TAC (intrel_ss addrews [zmagnitude,zminus,nnat,add_0_right]) 1);
+by (simp_tac (intrel_ss addsimps [zmagnitude,zminus,nnat,add_0_right]) 1);
val zmagnitude_zminus_znat = result();
@@ -254,7 +252,7 @@
by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1);
by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3);
by (typechk_tac [add_type]);
-by (ASM_SIMP_TAC (arith_ss addrews [add_assoc RS sym]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
val zadd_congruent2 = result();
(*Resolve th against the corresponding facts for zadd*)
@@ -269,19 +267,19 @@
val prems = goalw Integ.thy [zadd_def]
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
\ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = intrel `` {<x1#+x2, y1#+y2>}";
-by (ASM_SIMP_TAC (ZF_ss addrews
+by (asm_simp_tac (ZF_ss addsimps
(prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1);
val zadd = result();
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zadd]) 1);
+by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
val zadd_0 = result();
goalw Integ.thy [integ_def]
"!!z w. [| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zminus,zadd] addcongs integ_congs) 1);
+by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
val zminus_zadd_distrib = result();
goalw Integ.thy [integ_def]
@@ -296,17 +294,17 @@
\ (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
(*rewriting is much faster without intrel_iff, etc.*)
-by (ASM_SIMP_TAC (intrel_ss0 addrews [zadd,add_assoc]) 1);
+by (asm_simp_tac (arith_ss addsimps [zadd,add_assoc]) 1);
val zadd_assoc = result();
val prems = goalw Integ.thy [znat_def]
"[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
-by (ASM_SIMP_TAC (arith_ss addrews (zadd::prems)) 1);
+by (asm_simp_tac (arith_ss addsimps (zadd::prems)) 1);
val znat_add = result();
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (intrel_ss addrews [zminus,zadd,add_0_right]) 1);
+by (asm_simp_tac (intrel_ss addsimps [zminus,zadd,add_0_right]) 1);
by (REPEAT (ares_tac [add_commute] 1));
val zadd_zminus_inverse = result();
@@ -334,7 +332,7 @@
"[| k: nat; l: nat; m: nat; n: nat |] ==> \
\ (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)";
val add_commute' = read_instantiate [("m","l")] add_commute;
-by (SIMP_TAC (arith_ss addrews ([add_commute',add_assoc]@prems)) 1);
+by (simp_tac (arith_ss addsimps ([add_commute',add_assoc]@prems)) 1);
val zmult_congruent_lemma = result();
goal Integ.thy
@@ -348,7 +346,7 @@
by (rtac (zmult_congruent_lemma RS trans) 2);
by (rtac (zmult_congruent_lemma RS trans RS sym) 6);
by (typechk_tac [mult_type]);
-by (ASM_SIMP_TAC (arith_ss addrews [add_mult_distrib_left RS sym]) 2);
+by (asm_simp_tac (arith_ss addsimps [add_mult_distrib_left RS sym]) 2);
(*Proof that zmult is commutative on representatives*)
by (rtac add_cong 1);
by (rtac (add_commute RS trans) 2);
@@ -370,19 +368,19 @@
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
\ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (ASM_SIMP_TAC (ZF_ss addrews
+by (asm_simp_tac (ZF_ss addsimps
(prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1);
val zmult = result();
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zmult]) 1);
+by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
val zmult_0 = result();
goalw Integ.thy [integ_def,znat_def,one_def]
"!!z. z : integ ==> $#1 $* z = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zmult,add_0_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
val zmult_1 = result();
goalw Integ.thy [integ_def]
@@ -432,6 +430,5 @@
[znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
val integ_ss =
- arith_ss addcongs integ_congs
- addrews ([zminus_zminus,zmagnitude_znat,zmagnitude_zminus_znat,
- zadd_0] @ integ_typechecks);
+ arith_ss addsimps ([zminus_zminus, zmagnitude_znat,
+ zmagnitude_zminus_znat, zadd_0] @ integ_typechecks);
--- a/src/ZF/ex/LList.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/LList.ML Fri Sep 17 16:52:10 1993 +0200
@@ -11,7 +11,6 @@
structure LList = Co_Datatype_Fun
(val thy = QUniv.thy;
- val thy = QUniv.thy;
val rec_specs =
[("llist", "quniv(A)",
[(["LNil"], "i"),
--- a/src/ZF/ex/ListN.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/ListN.ML Fri Sep 17 16:52:10 1993 +0200
@@ -20,28 +20,24 @@
val type_intrs = nat_typechecks@List.intrs@[SigmaI]
val type_elims = [SigmaE2]);
-(*Could be generated automatically; requires use of fsplitD*)
-val listn_induct = standard
- (fsplitI RSN
- (2, fsplitI RSN
- (3, (read_instantiate [("P", "fsplit(R)")] ListN.induct) RS fsplitD)));
+val listn_induct = standard
+ (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
by (rtac (major RS List.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
by (REPEAT (ares_tac ListN.intrs 1));
val list_into_listn = result();
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
by (rtac iffI 1);
by (etac listn_induct 1);
-by (dtac fsplitD 2);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [Pair_iff])));
-by (fast_tac (ZF_cs addSIs [list_into_listn]) 1);
+by (safe_tac (ZF_cs addSIs (list_typechecks @
+ [length_Nil, length_Cons, list_into_listn])));
val listn_iff = result();
goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
by (rtac equality_iffI 1);
-by (SIMP_TAC (list_ss addrews [listn_iff,separation,image_singleton_iff]) 1);
+by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
val listn_image_eq = result();
--- a/src/ZF/ex/PropLog.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/PropLog.ML Fri Sep 17 16:52:10 1993 +0200
@@ -13,71 +13,66 @@
(*** prop_rec -- by Vset recursion ***)
-val prop_congs = mk_typed_congs Prop.thy
- [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
-
(** conversion rules **)
goal PropLog.thy "prop_rec(Fls,b,c,d) = b";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Prop.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val prop_rec_Fls = result();
goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Prop.con_defs);
-by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
+by (simp_tac rank_ss 1);
val prop_rec_Var = result();
goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
\ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Prop.con_defs);
-by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
+by (simp_tac rank_ss 1);
val prop_rec_Imp = result();
val prop_rec_ss =
- arith_ss addrews [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
+ arith_ss addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
(*** Semantics of propositional logic ***)
(** The function is_true **)
goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False";
-by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]) 1);
+by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1);
val is_true_Fls = result();
goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t";
-by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]
- addsplits [expand_if]) 1);
+by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]
+ setloop (split_tac [expand_if])) 1);
val is_true_Var = result();
goalw PropLog.thy [is_true_def]
"is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
-by (SIMP_TAC (prop_rec_ss addsplits [expand_if]) 1);
+by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1);
val is_true_Imp = result();
(** The function hyps **)
goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0";
-by (SIMP_TAC prop_rec_ss 1);
+by (simp_tac prop_rec_ss 1);
val hyps_Fls = result();
goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}";
-by (SIMP_TAC prop_rec_ss 1);
+by (simp_tac prop_rec_ss 1);
val hyps_Var = result();
goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)";
-by (SIMP_TAC prop_rec_ss 1);
+by (simp_tac prop_rec_ss 1);
val hyps_Imp = result();
val prop_ss = prop_rec_ss
- addcongs Prop.congs
- addcongs (mk_congs PropLog.thy ["Fin", "thms", "op |=","is_true","hyps"])
- addrews Prop.intrs
- addrews [is_true_Fls, is_true_Var, is_true_Imp,
- hyps_Fls, hyps_Var, hyps_Imp];
+ addsimps Prop.intrs
+ addsimps [is_true_Fls, is_true_Var, is_true_Imp,
+ hyps_Fls, hyps_Var, hyps_Imp];
(*** Proof theory of propositional logic ***)
@@ -162,10 +157,10 @@
val thms_notE = standard (thms_MP RS thms_FlsE);
(*Soundness of the rules wrt truth-table semantics*)
-val [major] = goalw PropThms.thy [sat_def] "H |- p ==> H |= p";
-by (rtac (major RS PropThms.induct) 1);
+goalw PropThms.thy [sat_def] "!!H. H |- p ==> H |= p";
+by (etac PropThms.induct 1);
by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (SIMP_TAC prop_ss));
+by (ALLGOALS (asm_simp_tac prop_ss));
val soundness = result();
(*** Towards the completeness proof ***)
@@ -194,7 +189,7 @@
"p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
by (rtac (expand_if RS iffD2) 1);
by (rtac (major RS Prop.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [thms_I, thms_H])));
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2,
weaken_right, Imp_Fls]
addSEs [Fls_Imp]) 1);
@@ -235,10 +230,10 @@
val [major] = goal PropThms.thy
"p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
by (rtac (major RS Prop.induct) 1);
-by (SIMP_TAC prop_ss 1);
-by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
+by (simp_tac prop_ss 1);
+by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
-by (ASM_SIMP_TAC prop_ss 1);
+by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val hyps_Diff = result();
@@ -247,10 +242,10 @@
val [major] = goal PropThms.thy
"p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
by (rtac (major RS Prop.induct) 1);
-by (SIMP_TAC prop_ss 1);
-by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
+by (simp_tac prop_ss 1);
+by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
-by (ASM_SIMP_TAC prop_ss 1);
+by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val hyps_cons = result();
@@ -269,9 +264,9 @@
val [major] = goal PropThms.thy
"p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
by (rtac (major RS Prop.induct) 1);
-by (ASM_SIMP_TAC (prop_ss addrews [Fin_0I, Fin_consI, UN_I]
- addsplits [expand_if]) 2);
-by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [Un_0, Fin_0I, Fin_UnI])));
+by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I]
+ setloop (split_tac [expand_if])) 2);
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
val hyps_finite = result();
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
@@ -281,7 +276,7 @@
val [premp,sat] = goal PropThms.thy
"[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
by (rtac (premp RS hyps_finite RS Fin_induct) 1);
-by (SIMP_TAC (prop_ss addrews [premp, sat, sat_thms_p, Diff_0]) 1);
+by (simp_tac (prop_ss addsimps [premp, sat, sat_thms_p, Diff_0]) 1);
by (safe_tac ZF_cs);
(*Case hyps(p,t)-cons(#v,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
@@ -309,7 +304,7 @@
(*A semantic analogue of the Deduction Theorem*)
goalw PropThms.thy [sat_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
-by (SIMP_TAC prop_ss 1);
+by (simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val sat_Imp = result();
--- a/src/ZF/ex/Ramsey.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/Ramsey.ML Fri Sep 17 16:52:10 1993 +0200
@@ -20,9 +20,6 @@
open Ramsey;
-val ramsey_congs = mk_congs Ramsey.thy ["Atleast"];
-val ramsey_ss = arith_ss addcongs ramsey_congs;
-
(*** Cliques and Independent sets ***)
goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
@@ -95,11 +92,12 @@
\ Atleast(m,A) | Atleast(n,B)";
by (nat_ind_tac "m" prems 1);
by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
-by (ASM_SIMP_TAC ramsey_ss 1);
+by (asm_simp_tac arith_ss 1);
by (rtac ballI 1);
+by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*)
by (nat_ind_tac "n" [] 1);
by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
-by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
by (safe_tac ZF_cs);
by (etac (Atleast_succD RS bexE) 1);
by (etac UnE 1);
@@ -118,7 +116,7 @@
(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
(*proving the condition*)
-by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
val pigeon2_lemma = result();
@@ -147,7 +145,7 @@
"[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \
\ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
by (rtac (nat_succI RS pigeon2) 1);
-by (SIMP_TAC (ramsey_ss addrews prems) 3);
+by (simp_tac (arith_ss addsimps prems) 3);
by (rtac Atleast_superset 3);
by (REPEAT (resolve_tac prems 1));
by (fast_tac ZF_cs 1);
--- a/src/ZF/ex/TF_Fn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/TF_Fn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -16,33 +16,29 @@
(*** TF_rec -- by Vset recursion ***)
-(*Used only to verify TF_rec*)
-val TF_congs = mk_typed_congs TF.thy
- [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
-
(** conversion rules **)
goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
-by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
+by (simp_tac rank_ss 1);
val TF_rec_Tcons = result();
goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val TF_rec_Fnil = result();
goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
\ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
-by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
+by (simp_tac rank_ss 1);
val TF_rec_Fcons = result();
(*list_ss includes list operations as well as arith_ss*)
-val TF_rec_ss = list_ss addrews
+val TF_rec_ss = list_ss addsimps
[TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
(** Type checking **)
@@ -56,7 +52,7 @@
\ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
\ |] ==> TF_rec(z,b,c,d) : C(z)";
by (rtac (major RS TF.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
val TF_rec_type = result();
(*Mutually recursive version*)
@@ -70,7 +66,7 @@
\ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
by (rewtac Ball_def);
by (rtac TF.mutual_induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
val tree_forest_rec_type = result();
@@ -159,10 +155,6 @@
[TconsI, FnilI, FconsI, treeI, forestI,
list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
-val TF_congs = TF.congs @
- mk_congs TF_Fn.thy
- ["TF_rec", "list_of_TF", "TF_of_list", "TF_map", "TF_size", "TF_preorder"];
-
val TF_rewrites =
[TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
@@ -171,8 +163,8 @@
TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
-val TF_ss = list_ss addcongs TF_congs
- addrews (TF_rewrites@TF_typechecks);
+val TF_ss = list_ss addsimps TF_rewrites
+ setsolver type_auto_tac (list_typechecks@TF_typechecks);
(** theorems about list_of_TF and TF_of_list **)
@@ -188,26 +180,26 @@
goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
by (etac forest_induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val forest_iso = result();
goal TF_Fn.thy
"!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
by (etac List.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val tree_list_iso = result();
(** theorems about TF_map **)
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val TF_map_ident = result();
goal TF_Fn.thy
"!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val TF_map_compose = result();
(** theorems about TF_size **)
@@ -215,13 +207,13 @@
goal TF_Fn.thy
"!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val TF_size_TF_map = result();
goal TF_Fn.thy
"!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [length_app])));
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
val TF_size_length = result();
(** theorems about TF_preorder **)
@@ -229,5 +221,5 @@
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
val TF_preorder_TF_map = result();
--- a/src/ZF/ex/TermFn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/TermFn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -18,11 +18,11 @@
"[| l: list(A); Ord(i) |] ==> \
\ rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
by (rtac (major RS List.induct) 1);
-by (SIMP_TAC list_ss 1);
+by (simp_tac list_ss 1);
by (rtac impI 1);
by (forward_tac [rank_Cons1 RS Ord_trans] 1);
by (dtac (rank_Cons2 RS Ord_trans) 2);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [ordi, VsetI])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [ordi, VsetI])));
val map_lemma = result();
(*Typing premise is necessary to invoke map_lemma*)
@@ -31,10 +31,8 @@
\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
by (rtac (term_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Term.con_defs);
-val term_rec_ss = ZF_ss
- addcongs (mk_typed_congs TermFn.thy [("d", "[i,i,i]=>i")])
- addrews [Ord_rank, rank_pair2, prem RS map_lemma];
-by (SIMP_TAC term_rec_ss 1);
+val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
+by (simp_tac term_rec_ss 1);
val term_rec = result();
(*Slightly odd typing condition on r in the second premise!*)
@@ -49,7 +47,7 @@
by (rtac (term_rec RS ssubst) 1);
by (REPEAT (ares_tac prems 1));
by (etac List.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [term_rec])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
by (etac CollectE 1);
by (REPEAT (ares_tac [ConsI, UN_I] 1));
val term_rec_type = result();
@@ -122,31 +120,27 @@
(*map_type2 and term_map_type2 instantiate variables*)
val term_ss = list_ss
- addcongs (Term.congs @
- mk_congs TermFn.thy ["term_rec","term_map","term_size",
- "reflect","preorder"])
- addrews [term_rec, term_map, term_size, reflect,
- preorder]
- setauto type_auto_tac (list_typechecks@term_typechecks);
+ addsimps [term_rec, term_map, term_size, reflect, preorder]
+ setsolver type_auto_tac (list_typechecks@term_typechecks);
(** theorems about term_map **)
goal TermFn.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_ident]) 1);
+by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
val term_map_ident = result();
goal TermFn.thy
"!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
val term_map_compose = result();
goal TermFn.thy
"!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
val term_map_reflect = result();
@@ -155,18 +149,18 @@
goal TermFn.thy
"!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
val term_size_term_map = result();
goal TermFn.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose,
- list_add_rev]) 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
+ list_add_rev]) 1);
val term_size_reflect = result();
goal TermFn.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [length_flat, map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
val term_size_length = result();
@@ -174,8 +168,8 @@
goal TermFn.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib, map_compose,
- map_ident, rev_rev_ident]) 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
+ map_ident, rev_rev_ident]) 1);
val reflect_reflect_ident = result();
@@ -184,7 +178,7 @@
goal TermFn.thy
"!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_compose, map_flat]) 1);
+by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
val preorder_term_map = result();
(** preorder(reflect(t)) = rev(postorder(t)) **)
--- a/src/ZF/ex/binfn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/binfn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -14,20 +14,19 @@
goal BinFn.thy "bin_rec(Plus,a,b,h) = a";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Bin.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val bin_rec_Plus = result();
goal BinFn.thy "bin_rec(Minus,a,b,h) = b";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Bin.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val bin_rec_Minus = result();
goal BinFn.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Bin.con_defs);
-by (SIMP_TAC (rank_ss addcongs
- (mk_typed_congs BinFn.thy [("h", "[i,i,i]=>i")])) 1);
+by (simp_tac rank_ss 1);
val bin_rec_Bcons = result();
(*Type checking*)
@@ -38,7 +37,7 @@
\ |] ==> bin_rec(w,a,b,h) : C(w)";
by (bin_ind_tac "w" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC (ZF_ss addrews (prems@[bin_rec_Plus,bin_rec_Minus,
+ (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
bin_rec_Bcons]))));
val bin_rec_type = result();
@@ -106,13 +105,8 @@
[integ_of_bin_type, bin_succ_type, bin_pred_type,
bin_minus_type, bin_add_type, bin_mult_type];
-val bin_congs = mk_congs BinFn.thy
- ["bin_rec","op $$","integ_of_bin","bin_succ","bin_pred",
- "bin_minus","bin_add","bin_mult"];
-
val bin_ss = integ_ss
- addcongs (bin_congs@bool_congs)
- addrews([bool_1I, bool_0I,
+ addsimps([bool_1I, bool_0I,
bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
@@ -127,7 +121,7 @@
"!!z v. [| z $+ v = z' $+ v'; \
\ z: integ; z': integ; v: integ; v': integ; w: integ |] \
\ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
-by (ASM_SIMP_TAC (integ_ss addrews ([zadd_assoc RS sym])) 1);
+by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
val zadd_assoc_cong = result();
goal Integ.thy
@@ -136,7 +130,8 @@
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
val zadd_assoc_swap = result();
-val [zadd_cong] = mk_congs Integ.thy ["op $+"];
+val zadd_cong =
+ read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2;
val zadd_kill = (refl RS zadd_cong);
val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
@@ -151,28 +146,28 @@
val zadd_swap_pairs = result();
-val carry_ss = bin_ss addrews
+val carry_ss = bin_ss addsimps
(bin_recs bin_succ_def @ bin_recs bin_pred_def);
goal BinFn.thy
"!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
-by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
by (etac boolE 1);
-by (ALLGOALS (ASM_SIMP_TAC (carry_ss addrews [zadd_assoc])));
+by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc])));
by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
val integ_of_bin_succ = result();
goal BinFn.thy
"!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
-by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
by (etac boolE 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (carry_ss addrews [zadd_assoc RS sym,
+ (asm_simp_tac
+ (carry_ss addsimps [zadd_assoc RS sym,
zadd_zminus_inverse, zadd_zminus_inverse2])));
by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
val integ_of_bin_pred = result();
@@ -183,68 +178,68 @@
(*** bin_minus: (unary!) negation of binary integers ***)
val bin_minus_ss =
- bin_ss addrews (bin_recs bin_minus_def @
+ bin_ss addsimps (bin_recs bin_minus_def @
[integ_of_bin_succ, integ_of_bin_pred]);
goal BinFn.thy
"!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC (bin_minus_ss addrews [zminus_0]) 1);
-by (SIMP_TAC (bin_minus_ss addrews [zadd_0_right]) 1);
+by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1);
+by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1);
by (etac boolE 1);
by (ALLGOALS
- (ASM_SIMP_TAC (bin_minus_ss addrews [zminus_zadd_distrib, zadd_assoc])));
+ (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
val integ_of_bin_minus = result();
(*** bin_add: binary addition ***)
goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
-by (ASM_SIMP_TAC bin_ss 1);
+by (asm_simp_tac bin_ss 1);
val bin_add_Plus = result();
goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
-by (ASM_SIMP_TAC bin_ss 1);
+by (asm_simp_tac bin_ss 1);
val bin_add_Minus = result();
goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
-by (SIMP_TAC bin_ss 1);
+by (simp_tac bin_ss 1);
val bin_add_Bcons_Plus = result();
goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
-by (SIMP_TAC bin_ss 1);
+by (simp_tac bin_ss 1);
val bin_add_Bcons_Minus = result();
goalw BinFn.thy [bin_add_def]
"!!w y. [| w: bin; y: bool |] ==> \
\ bin_add(v$$x, w$$y) = \
\ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
-by (ASM_SIMP_TAC bin_ss 1);
+by (asm_simp_tac bin_ss 1);
val bin_add_Bcons_Bcons = result();
val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
integ_of_bin_succ, integ_of_bin_pred];
-val bin_add_ss = bin_ss addrews ([bool_subset_nat RS subsetD] @ bin_add_rews);
+val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews);
goal BinFn.thy
"!!v. v: bin ==> \
\ ALL w: bin. integ_of_bin(bin_add(v,w)) = \
\ integ_of_bin(v) $+ integ_of_bin(w)";
by (etac Bin.induct 1);
-by (SIMP_TAC bin_add_ss 1);
-by (SIMP_TAC bin_add_ss 1);
+by (simp_tac bin_add_ss 1);
+by (simp_tac bin_add_ss 1);
by (rtac ballI 1);
by (bin_ind_tac "wa" [] 1);
-by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_0_right]) 1);
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1);
+by (asm_simp_tac bin_add_ss 1);
by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
by (etac boolE 1);
-by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc, zadd_swap_pairs]) 2);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2);
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
by (etac boolE 1);
-by (ALLGOALS (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc,zadd_swap_pairs])));
+by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
typechecks) 1));
val integ_of_bin_add_lemma = result();
@@ -255,7 +250,7 @@
(*** bin_add: binary multiplication ***)
val bin_mult_ss =
- bin_ss addrews (bin_recs bin_mult_def @
+ bin_ss addsimps (bin_recs bin_mult_def @
[integ_of_bin_minus, integ_of_bin_add]);
@@ -265,12 +260,12 @@
\ integ_of_bin(v) $* integ_of_bin(w)";
by (cut_facts_tac prems 1);
by (bin_ind_tac "v" [major] 1);
-by (SIMP_TAC (bin_mult_ss addrews [zmult_0]) 1);
-by (SIMP_TAC (bin_mult_ss addrews [zmult_1,zmult_zminus]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1);
by (etac boolE 1);
-by (ASM_SIMP_TAC (bin_mult_ss addrews [zadd_zmult_distrib]) 2);
-by (ASM_SIMP_TAC
- (bin_mult_ss addrews [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2);
+by (asm_simp_tac
+ (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
typechecks) 1));
val integ_of_bin_mult = result();
@@ -283,19 +278,19 @@
val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
goal BinFn.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_succ_Bcons1 = result();
goal BinFn.thy "bin_succ(w$$0) = w$$1";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_succ_Bcons0 = result();
goal BinFn.thy "bin_pred(w$$1) = w$$0";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_pred_Bcons1 = result();
goal BinFn.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
-by (SIMP_TAC carry_ss 1);
+by (simp_tac carry_ss 1);
val bin_pred_Bcons0 = result();
(** extra rules for bin_minus **)
@@ -303,28 +298,28 @@
val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
goal BinFn.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
-by (SIMP_TAC bin_minus_ss 1);
+by (simp_tac bin_minus_ss 1);
val bin_minus_Bcons1 = result();
goal BinFn.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
-by (SIMP_TAC bin_minus_ss 1);
+by (simp_tac bin_minus_ss 1);
val bin_minus_Bcons0 = result();
(** extra rules for bin_add **)
goal BinFn.thy
"!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac bin_add_ss 1);
val bin_add_Bcons_Bcons11 = result();
goal BinFn.thy
"!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac bin_add_ss 1);
val bin_add_Bcons_Bcons10 = result();
goal BinFn.thy
"!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
-by (ASM_SIMP_TAC bin_add_ss 1);
+by (asm_simp_tac bin_add_ss 1);
val bin_add_Bcons_Bcons0 = result();
(** extra rules for bin_mult **)
@@ -332,24 +327,18 @@
val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
goal BinFn.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
-by (SIMP_TAC bin_mult_ss 1);
+by (simp_tac bin_mult_ss 1);
val bin_mult_Bcons1 = result();
goal BinFn.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
-by (SIMP_TAC bin_mult_ss 1);
+by (simp_tac bin_mult_ss 1);
val bin_mult_Bcons0 = result();
(*** The computation simpset ***)
-val bin_comp_ss = carry_ss addrews
- [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, bin_add_Bcons_Minus,
- bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11]
- setauto (type_auto_tac bin_typechecks0);
-
val bin_comp_ss = integ_ss
- addcongs bin_congs
- addrews [bin_succ_Plus, bin_succ_Minus,
+ addsimps [bin_succ_Plus, bin_succ_Minus,
bin_succ_Bcons1, bin_succ_Bcons0,
bin_pred_Plus, bin_pred_Minus,
bin_pred_Bcons1, bin_pred_Bcons0,
@@ -360,7 +349,7 @@
bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
bin_mult_Plus, bin_mult_Minus,
bin_mult_Bcons1, bin_mult_Bcons0]
- setauto (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+ setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
(*** Examples of performing binary arithmetic by simplification ***)
@@ -370,7 +359,7 @@
(* 13+19 = 32 *)
goal BinFn.thy
"bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*1.9 secs*)
+by (simp_tac bin_comp_ss 1); (*0.6 secs*)
result();
bin_add(binary_of_int 13, binary_of_int 19);
@@ -380,7 +369,7 @@
"bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
\ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
\ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*8.9 secs*)
+by (simp_tac bin_comp_ss 1); (*2.6 secs*)
result();
bin_add(binary_of_int 1234, binary_of_int 5678);
@@ -390,7 +379,7 @@
"bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
\ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*7.4 secs*)
+by (simp_tac bin_comp_ss 1); (*2.3 secs*)
result();
bin_add(binary_of_int 1359, binary_of_int ~2468);
@@ -400,7 +389,7 @@
"bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
\ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
\ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*13.7 secs*)
+by (simp_tac bin_comp_ss 1); (*3.9 secs*)
result();
bin_add(binary_of_int 93746, binary_of_int ~46375);
@@ -409,7 +398,7 @@
goal BinFn.thy
"bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
\ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*2.8 secs*)
+by (simp_tac bin_comp_ss 1); (*0.6 secs*)
result();
bin_minus(binary_of_int 65745);
@@ -418,7 +407,7 @@
goal BinFn.thy
"bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
\ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
-by (SIMP_TAC bin_comp_ss 1); (*3.3 secs*)
+by (simp_tac bin_comp_ss 1); (*0.7 secs*)
result();
bin_minus(binary_of_int ~54321);
@@ -426,7 +415,7 @@
(* 13*19 = 247 *)
goal BinFn.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
\ Plus$$1$$1$$1$$1$$0$$1$$1$$1";
-by (SIMP_TAC bin_comp_ss 1); (*4.4 secs*)
+by (simp_tac bin_comp_ss 1); (*1.5 secs*)
result();
bin_mult(binary_of_int 13, binary_of_int 19);
@@ -435,7 +424,7 @@
goal BinFn.thy
"bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
\ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*9.2 secs*)
+by (simp_tac bin_comp_ss 1); (*2.6 secs*)
result();
bin_mult(binary_of_int ~84, binary_of_int 51);
@@ -445,19 +434,17 @@
"bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
\ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
\ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
-by (SIMP_TAC bin_comp_ss 1); (*38.4 secs*)
+by (simp_tac bin_comp_ss 1); (*9.8 secs*)
result();
bin_mult(binary_of_int 255, binary_of_int 255);
-(***************** TOO SLOW TO INCLUDE IN TEST RUNS
(* 1359 * ~2468 = ~3354012 *)
goal BinFn.thy
"bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
\ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
-by (SIMP_TAC bin_comp_ss 1); (*54.8 secs*)
+by (simp_tac bin_comp_ss 1); (*13.7 secs*)
result();
-****************)
bin_mult(binary_of_int 1359, binary_of_int ~2468);
--- a/src/ZF/ex/bt_fn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/bt_fn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -12,28 +12,24 @@
(** bt_rec -- by Vset recursion **)
-(*Used to verify bt_rec*)
-val bt_rec_ss = ZF_ss
- addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")])
- addrews BT.case_eqns;
-
goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Br1 = result();
goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Br2 = result();
goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC bt_rec_ss 1);
+by (simp_tac (ZF_ss addsimps BT.case_eqns) 1);
val bt_rec_Lf = result();
goal BT_Fn.thy
"bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1);
+by (simp_tac (ZF_ss addsimps
+ (BT.case_eqns @ [Vset_rankI, rank_Br1, rank_Br2])) 1);
val bt_rec_Br = result();
(*Type checking -- proved by induction, as usual*)
@@ -44,7 +40,7 @@
\ h(x,y,z,r,s): C(Br(x,y,z)) \
\ |] ==> bt_rec(t,c,h) : C(t)";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
(prems@[bt_rec_Lf,bt_rec_Br]))));
val bt_rec_type = result();
@@ -98,15 +94,10 @@
val bt_typechecks =
[LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
-val bt_congs =
- BT.congs @
- mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"];
-
val bt_ss = arith_ss
- addcongs bt_congs
- addrews BT.case_eqns
- addrews bt_typechecks
- addrews [bt_rec_Lf, bt_rec_Br,
+ addsimps BT.case_eqns
+ addsimps bt_typechecks
+ addsimps [bt_rec_Lf, bt_rec_Br,
n_nodes_Lf, n_nodes_Br,
n_leaves_Lf, n_leaves_Br,
bt_reflect_Lf, bt_reflect_Br];
@@ -117,14 +108,14 @@
val prems = goal BT_Fn.thy
"t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC bt_ss));
+by (ALLGOALS (asm_simp_tac bt_ss));
by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
val n_leaves_reflect = result();
val prems = goal BT_Fn.thy
"t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right])));
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
val n_leaves_nodes = result();
(*** theorems about bt_reflect ***)
@@ -132,7 +123,7 @@
val prems = goal BT_Fn.thy
"t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
by (bt_ind_tac "t" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC bt_ss));
+by (ALLGOALS (asm_simp_tac bt_ss));
val bt_reflect_bt_reflect_ident = result();
--- a/src/ZF/ex/enum.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/enum.ML Fri Sep 17 16:52:10 1993 +0200
@@ -28,6 +28,6 @@
val type_elims = []);
goal Enum.thy "~ con59=con60";
-by (SIMP_TAC (ZF_ss addrews Enum.free_iffs) 1); (*2.3 secs*)
+by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1); (*2.3 secs*)
result();
--- a/src/ZF/ex/equiv.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/equiv.ML Fri Sep 17 16:52:10 1993 +0200
@@ -190,7 +190,7 @@
by (safe_tac ZF_cs);
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
+by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
congruent2_implies_congruent]) 1);
by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
by (fast_tac ZF_cs 1);
@@ -200,7 +200,7 @@
"[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \
\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
by (cut_facts_tac prems 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class,
+by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
congruent2_implies_congruent,
congruent2_implies_congruent_UN]) 1);
val UN_equiv_class2 = result();
@@ -235,7 +235,7 @@
val [equivA,commute,congt] = goal Equiv.thy
"[| equiv(A,r); \
-\ !! y z w. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
+\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
\ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
\ |] ==> congruent2(r,b)";
by (resolve_tac [equivA RS congruent2I] 1);
@@ -259,7 +259,7 @@
by (safe_tac ZF_cs);
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [congt RS (equivA RS UN_equiv_class)]) 1);
+by (asm_simp_tac (ZF_ss addsimps [congt RS (equivA RS UN_equiv_class)]) 1);
by (rtac (commute RS trans) 1);
by (rtac (commute RS trans RS sym) 3);
by (rtac sym 5);
--- a/src/ZF/ex/integ.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/integ.ML Fri Sep 17 16:52:10 1993 +0200
@@ -12,16 +12,18 @@
$+ and $* are monotonic wrt $<
*)
-open Integ;
+val add_cong =
+ read_instantiate_sg (sign_of Arith.thy) [("t","op #+")] subst_context2;
-val [add_cong] = mk_congs Arith.thy ["op #+"];
+
+open Integ;
(*** Proving that intrel is an equivalence relation ***)
val prems = goal Arith.thy
"[| m #+ n = m' #+ n'; m: nat; m': nat |] \
\ ==> m #+ (n #+ k) = m' #+ (n' #+ k)";
-by (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym] @ prems)) 1);
+by (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym] @ prems)) 1);
val add_assoc_cong = result();
val prems = goal Arith.thy
@@ -31,6 +33,7 @@
val add_assoc_swap = result();
val add_kill = (refl RS add_cong);
+
val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans);
(*By luck, requires no typing premises for y1, y2,y3*)
@@ -90,22 +93,17 @@
val equiv_intrel = result();
-val integ_congs = mk_congs Integ.thy
- ["znat", "zminus", "znegative", "zmagnitude", "op $+", "op $-", "op $*"];
-
-val intrel_ss0 = arith_ss addcongs integ_congs;
+val intrel_ss =
+ arith_ss addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
-val intrel_ss =
- intrel_ss0 addrews [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
-
-(*More than twice as fast as simplifying with intrel_ss*)
+(*Roughly twice as fast as simplifying with intrel_ss*)
fun INTEG_SIMP_TAC ths =
- let val ss = intrel_ss0 addrews ths
+ let val ss = arith_ss addsimps ths
in fn i =>
- EVERY [ASM_SIMP_TAC ss i,
+ EVERY [asm_simp_tac ss i,
rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i,
typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks),
- ASM_SIMP_TAC ss i]
+ asm_simp_tac ss i]
end;
@@ -130,7 +128,7 @@
goalw Integ.thy [congruent_def]
"congruent(intrel, split(%x y. intrel``{<y,x>}))";
by (safe_tac intrel_cs);
-by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
+by (ALLGOALS (asm_simp_tac intrel_ss));
by (etac (box_equals RS sym) 1);
by (REPEAT (ares_tac [add_commute] 1));
val zminus_congruent = result();
@@ -150,7 +148,7 @@
by (REPEAT (ares_tac prems 1));
by (REPEAT (etac SigmaE 1));
by (etac rev_mp 1);
-by (ASM_SIMP_TAC ZF_ss 1);
+by (asm_simp_tac ZF_ss 1);
by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel]
addSEs [box_equals RS sym, add_commute,
make_elim eq_equiv_class]) 1);
@@ -158,17 +156,17 @@
val prems = goalw Integ.thy [zminus_def]
"[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (ASM_SIMP_TAC
- (ZF_ss addrews (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
+by (asm_simp_tac
+ (ZF_ss addsimps (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
val zminus = result();
goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [zminus] addcongs integ_congs) 1);
+by (asm_simp_tac (ZF_ss addsimps [zminus]) 1);
val zminus_zminus = result();
goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0";
-by (SIMP_TAC (arith_ss addrews [zminus]) 1);
+by (simp_tac (arith_ss addsimps [zminus]) 1);
val zminus_0 = result();
@@ -179,13 +177,13 @@
by (safe_tac intrel_cs);
by (rtac (add_not_less_self RS notE) 1);
by (etac ssubst 3);
-by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 3);
+by (asm_simp_tac (arith_ss addsimps [add_0_right]) 3);
by (REPEAT (assume_tac 1));
val not_znegative_znat = result();
val [nnat] = goalw Integ.thy [znegative_def, znat_def]
"n: nat ==> znegative($~ $# succ(n))";
-by (SIMP_TAC (intrel_ss addrews [zminus,nnat]) 1);
+by (simp_tac (intrel_ss addsimps [zminus,nnat]) 1);
by (REPEAT
(resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
refl RS intrelI RS imageI, consI1, nnat, nat_0I,
@@ -198,19 +196,19 @@
goalw Integ.thy [congruent_def]
"congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))";
by (safe_tac intrel_cs);
-by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
+by (ALLGOALS (asm_simp_tac intrel_ss));
by (etac rev_mp 1);
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
by (REPEAT (assume_tac 1));
-by (ASM_SIMP_TAC (arith_ss addrews [add_succ_right,succ_inject_iff]) 3);
-by (ASM_SIMP_TAC
- (arith_ss addrews [diff_add_inverse,diff_add_0,add_0_right]) 2);
-by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_succ_right,succ_inject_iff]) 3);
+by (asm_simp_tac
+ (arith_ss addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2);
+by (asm_simp_tac (arith_ss addsimps [add_0_right]) 1);
by (rtac impI 1);
by (etac subst 1);
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
by (REPEAT (assume_tac 1));
-by (ASM_SIMP_TAC (arith_ss addrews [diff_add_inverse,diff_add_0]) 1);
+by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
val zmagnitude_congruent = result();
(*Resolve th against the corresponding facts for zmagnitude*)
@@ -225,18 +223,18 @@
val prems = goalw Integ.thy [zmagnitude_def]
"[| x: nat; y: nat |] ==> \
\ zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)";
-by (ASM_SIMP_TAC
- (ZF_ss addrews (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
+by (asm_simp_tac
+ (ZF_ss addsimps (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
val zmagnitude = result();
val [nnat] = goalw Integ.thy [znat_def]
"n: nat ==> zmagnitude($# n) = n";
-by (SIMP_TAC (intrel_ss addrews [zmagnitude,nnat]) 1);
+by (simp_tac (intrel_ss addsimps [zmagnitude,nnat]) 1);
val zmagnitude_znat = result();
val [nnat] = goalw Integ.thy [znat_def]
"n: nat ==> zmagnitude($~ $# n) = n";
-by (SIMP_TAC (intrel_ss addrews [zmagnitude,zminus,nnat,add_0_right]) 1);
+by (simp_tac (intrel_ss addsimps [zmagnitude,zminus,nnat,add_0_right]) 1);
val zmagnitude_zminus_znat = result();
@@ -254,7 +252,7 @@
by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1);
by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3);
by (typechk_tac [add_type]);
-by (ASM_SIMP_TAC (arith_ss addrews [add_assoc RS sym]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
val zadd_congruent2 = result();
(*Resolve th against the corresponding facts for zadd*)
@@ -269,19 +267,19 @@
val prems = goalw Integ.thy [zadd_def]
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
\ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = intrel `` {<x1#+x2, y1#+y2>}";
-by (ASM_SIMP_TAC (ZF_ss addrews
+by (asm_simp_tac (ZF_ss addsimps
(prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1);
val zadd = result();
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zadd]) 1);
+by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
val zadd_0 = result();
goalw Integ.thy [integ_def]
"!!z w. [| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zminus,zadd] addcongs integ_congs) 1);
+by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
val zminus_zadd_distrib = result();
goalw Integ.thy [integ_def]
@@ -296,17 +294,17 @@
\ (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
(*rewriting is much faster without intrel_iff, etc.*)
-by (ASM_SIMP_TAC (intrel_ss0 addrews [zadd,add_assoc]) 1);
+by (asm_simp_tac (arith_ss addsimps [zadd,add_assoc]) 1);
val zadd_assoc = result();
val prems = goalw Integ.thy [znat_def]
"[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
-by (ASM_SIMP_TAC (arith_ss addrews (zadd::prems)) 1);
+by (asm_simp_tac (arith_ss addsimps (zadd::prems)) 1);
val znat_add = result();
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (intrel_ss addrews [zminus,zadd,add_0_right]) 1);
+by (asm_simp_tac (intrel_ss addsimps [zminus,zadd,add_0_right]) 1);
by (REPEAT (ares_tac [add_commute] 1));
val zadd_zminus_inverse = result();
@@ -334,7 +332,7 @@
"[| k: nat; l: nat; m: nat; n: nat |] ==> \
\ (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)";
val add_commute' = read_instantiate [("m","l")] add_commute;
-by (SIMP_TAC (arith_ss addrews ([add_commute',add_assoc]@prems)) 1);
+by (simp_tac (arith_ss addsimps ([add_commute',add_assoc]@prems)) 1);
val zmult_congruent_lemma = result();
goal Integ.thy
@@ -348,7 +346,7 @@
by (rtac (zmult_congruent_lemma RS trans) 2);
by (rtac (zmult_congruent_lemma RS trans RS sym) 6);
by (typechk_tac [mult_type]);
-by (ASM_SIMP_TAC (arith_ss addrews [add_mult_distrib_left RS sym]) 2);
+by (asm_simp_tac (arith_ss addsimps [add_mult_distrib_left RS sym]) 2);
(*Proof that zmult is commutative on representatives*)
by (rtac add_cong 1);
by (rtac (add_commute RS trans) 2);
@@ -370,19 +368,19 @@
"[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
\ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (ASM_SIMP_TAC (ZF_ss addrews
+by (asm_simp_tac (ZF_ss addsimps
(prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1);
val zmult = result();
goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zmult]) 1);
+by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
val zmult_0 = result();
goalw Integ.thy [integ_def,znat_def,one_def]
"!!z. z : integ ==> $#1 $* z = z";
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (ASM_SIMP_TAC (arith_ss addrews [zmult,add_0_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [zmult,add_0_right]) 1);
val zmult_1 = result();
goalw Integ.thy [integ_def]
@@ -432,6 +430,5 @@
[znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
val integ_ss =
- arith_ss addcongs integ_congs
- addrews ([zminus_zminus,zmagnitude_znat,zmagnitude_zminus_znat,
- zadd_0] @ integ_typechecks);
+ arith_ss addsimps ([zminus_zminus, zmagnitude_znat,
+ zmagnitude_zminus_znat, zadd_0] @ integ_typechecks);
--- a/src/ZF/ex/listn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/listn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -20,28 +20,24 @@
val type_intrs = nat_typechecks@List.intrs@[SigmaI]
val type_elims = [SigmaE2]);
-(*Could be generated automatically; requires use of fsplitD*)
-val listn_induct = standard
- (fsplitI RSN
- (2, fsplitI RSN
- (3, (read_instantiate [("P", "fsplit(R)")] ListN.induct) RS fsplitD)));
+val listn_induct = standard
+ (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
by (rtac (major RS List.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
by (REPEAT (ares_tac ListN.intrs 1));
val list_into_listn = result();
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
by (rtac iffI 1);
by (etac listn_induct 1);
-by (dtac fsplitD 2);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [Pair_iff])));
-by (fast_tac (ZF_cs addSIs [list_into_listn]) 1);
+by (safe_tac (ZF_cs addSIs (list_typechecks @
+ [length_Nil, length_Cons, list_into_listn])));
val listn_iff = result();
goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
by (rtac equality_iffI 1);
-by (SIMP_TAC (list_ss addrews [listn_iff,separation,image_singleton_iff]) 1);
+by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
val listn_image_eq = result();
--- a/src/ZF/ex/llist.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/llist.ML Fri Sep 17 16:52:10 1993 +0200
@@ -11,7 +11,6 @@
structure LList = Co_Datatype_Fun
(val thy = QUniv.thy;
- val thy = QUniv.thy;
val rec_specs =
[("llist", "quniv(A)",
[(["LNil"], "i"),
--- a/src/ZF/ex/misc.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/misc.ML Fri Sep 17 16:52:10 1993 +0200
@@ -62,7 +62,7 @@
\ X - lfp(X, %W. X - g``(Y - f``W)) ";
by (res_inst_tac [("P", "%u. ?v = X-u")]
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
-by (SIMP_TAC (ZF_ss addrews [subset_refl, double_complement, Diff_subset,
+by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, Diff_subset,
gfun RS fun_is_rel RS image_subset]) 1);
val Banach_last_equation = result();
@@ -97,22 +97,29 @@
JAR 2 (1986), 287-327
*)
-val hom_ss = (*collecting the relevant lemmas*)
- ZF_ss addrews [comp_func,comp_func_apply,SigmaI,apply_type]
- addcongs (mk_congs Perm.thy ["op O"]);
+(*collecting the relevant lemmas*)
+val hom_ss = ZF_ss addsimps [comp_func,comp_func_apply,SigmaI,apply_funtype];
-(*This version uses a super application of SIMP_TAC; it is SLOW
- Expressing the goal by --> instead of ==> would make it slower still*)
-val [hom_eq] = goal Perm.thy
+(*The problem below is proving conditions of rewrites such as comp_func_apply;
+ rewriting does not instantiate Vars; we must prove the conditions
+ explicitly.*)
+fun hom_tac hyps =
+ resolve_tac (TrueI::refl::iff_refl::hyps) ORELSE'
+ (cut_facts_tac hyps THEN' fast_tac prop_cs);
+
+(*This version uses a super application of simp_tac*)
+goal Perm.thy
"(ALL A f B g. hom(A,f,B,g) = \
\ {H: A->B. f:A*A->A & g:B*B->B & \
-\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
+\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \
\ (K O J) : hom(A,f,C,h)";
-by (SIMP_TAC (hom_ss setauto K(fast_tac prop_cs) addrews [hom_eq]) 1);
+by (simp_tac (hom_ss setsolver hom_tac) 1);
+(*Also works but slower:
+ by (asm_simp_tac (hom_ss setloop (K (safe_tac FOL_cs))) 1); *)
val comp_homs = result();
-(*This version uses meta-level rewriting, safe_tac and ASM_SIMP_TAC*)
+(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
val [hom_def] = goal Perm.thy
"(!! A f B g. hom(A,f,B,g) == \
\ {H: A->B. f:A*A->A & g:B*B->B & \
@@ -121,8 +128,8 @@
\ (K O J) : hom(A,f,C,h)";
by (rewtac hom_def);
by (safe_tac ZF_cs);
-by (ASM_SIMP_TAC hom_ss 1);
-by (ASM_SIMP_TAC hom_ss 1);
+by (asm_simp_tac hom_ss 1);
+by (asm_simp_tac hom_ss 1);
val comp_homs = result();
@@ -210,4 +217,31 @@
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
val pastre6 = result();
+(** Yet another example... **)
+
+goalw (merge_theories(Sum.thy,Perm.thy)) [bij_def,inj_def,surj_def]
+ "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
+\ : bij(Pow(A+B), Pow(A)*Pow(B))";
+by (DO_GOAL
+ [rtac IntI,
+ DO_GOAL
+ [rtac CollectI,
+ fast_tac (ZF_cs addSIs [lam_type]),
+ simp_tac ZF_ss,
+ fast_tac (eq_cs addSEs [sumE]
+ addEs [equalityD1 RS subsetD RS CollectD2,
+ equalityD2 RS subsetD RS CollectD2])],
+ DO_GOAL
+ [rtac CollectI,
+ fast_tac (ZF_cs addSIs [lam_type]),
+ simp_tac ZF_ss,
+ K(safe_tac ZF_cs),
+ res_inst_tac [("x", "{Inl(u). u: ?U} Un {Inr(v). v: ?V}")] bexI,
+ DO_GOAL
+ [res_inst_tac [("t", "Pair")] subst_context2,
+ fast_tac (sum_cs addSIs [equalityI]),
+ fast_tac (sum_cs addSIs [equalityI])],
+ DO_GOAL [fast_tac sum_cs]]] 1);
+val Pow_bij = result();
+
writeln"Reached end of file.";
--- a/src/ZF/ex/proplog.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/proplog.ML Fri Sep 17 16:52:10 1993 +0200
@@ -13,71 +13,66 @@
(*** prop_rec -- by Vset recursion ***)
-val prop_congs = mk_typed_congs Prop.thy
- [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
-
(** conversion rules **)
goal PropLog.thy "prop_rec(Fls,b,c,d) = b";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Prop.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val prop_rec_Fls = result();
goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Prop.con_defs);
-by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
+by (simp_tac rank_ss 1);
val prop_rec_Var = result();
goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
\ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Prop.con_defs);
-by (SIMP_TAC (rank_ss addcongs prop_congs) 1);
+by (simp_tac rank_ss 1);
val prop_rec_Imp = result();
val prop_rec_ss =
- arith_ss addrews [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
+ arith_ss addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
(*** Semantics of propositional logic ***)
(** The function is_true **)
goalw PropLog.thy [is_true_def] "is_true(Fls,t) <-> False";
-by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]) 1);
+by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]) 1);
val is_true_Fls = result();
goalw PropLog.thy [is_true_def] "is_true(#v,t) <-> v:t";
-by (SIMP_TAC (prop_rec_ss addrews [one_not_0 RS not_sym]
- addsplits [expand_if]) 1);
+by (simp_tac (prop_rec_ss addsimps [one_not_0 RS not_sym]
+ setloop (split_tac [expand_if])) 1);
val is_true_Var = result();
goalw PropLog.thy [is_true_def]
"is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
-by (SIMP_TAC (prop_rec_ss addsplits [expand_if]) 1);
+by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1);
val is_true_Imp = result();
(** The function hyps **)
goalw PropLog.thy [hyps_def] "hyps(Fls,t) = 0";
-by (SIMP_TAC prop_rec_ss 1);
+by (simp_tac prop_rec_ss 1);
val hyps_Fls = result();
goalw PropLog.thy [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}";
-by (SIMP_TAC prop_rec_ss 1);
+by (simp_tac prop_rec_ss 1);
val hyps_Var = result();
goalw PropLog.thy [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)";
-by (SIMP_TAC prop_rec_ss 1);
+by (simp_tac prop_rec_ss 1);
val hyps_Imp = result();
val prop_ss = prop_rec_ss
- addcongs Prop.congs
- addcongs (mk_congs PropLog.thy ["Fin", "thms", "op |=","is_true","hyps"])
- addrews Prop.intrs
- addrews [is_true_Fls, is_true_Var, is_true_Imp,
- hyps_Fls, hyps_Var, hyps_Imp];
+ addsimps Prop.intrs
+ addsimps [is_true_Fls, is_true_Var, is_true_Imp,
+ hyps_Fls, hyps_Var, hyps_Imp];
(*** Proof theory of propositional logic ***)
@@ -162,10 +157,10 @@
val thms_notE = standard (thms_MP RS thms_FlsE);
(*Soundness of the rules wrt truth-table semantics*)
-val [major] = goalw PropThms.thy [sat_def] "H |- p ==> H |= p";
-by (rtac (major RS PropThms.induct) 1);
+goalw PropThms.thy [sat_def] "!!H. H |- p ==> H |= p";
+by (etac PropThms.induct 1);
by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (SIMP_TAC prop_ss));
+by (ALLGOALS (asm_simp_tac prop_ss));
val soundness = result();
(*** Towards the completeness proof ***)
@@ -194,7 +189,7 @@
"p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
by (rtac (expand_if RS iffD2) 1);
by (rtac (major RS Prop.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [thms_I, thms_H])));
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
by (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2,
weaken_right, Imp_Fls]
addSEs [Fls_Imp]) 1);
@@ -235,10 +230,10 @@
val [major] = goal PropThms.thy
"p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
by (rtac (major RS Prop.induct) 1);
-by (SIMP_TAC prop_ss 1);
-by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
+by (simp_tac prop_ss 1);
+by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
-by (ASM_SIMP_TAC prop_ss 1);
+by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val hyps_Diff = result();
@@ -247,10 +242,10 @@
val [major] = goal PropThms.thy
"p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
by (rtac (major RS Prop.induct) 1);
-by (SIMP_TAC prop_ss 1);
-by (ASM_SIMP_TAC (prop_ss addsplits [expand_if]) 1);
+by (simp_tac prop_ss 1);
+by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
-by (ASM_SIMP_TAC prop_ss 1);
+by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val hyps_cons = result();
@@ -269,9 +264,9 @@
val [major] = goal PropThms.thy
"p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
by (rtac (major RS Prop.induct) 1);
-by (ASM_SIMP_TAC (prop_ss addrews [Fin_0I, Fin_consI, UN_I]
- addsplits [expand_if]) 2);
-by (ALLGOALS (ASM_SIMP_TAC (prop_ss addrews [Un_0, Fin_0I, Fin_UnI])));
+by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I]
+ setloop (split_tac [expand_if])) 2);
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
val hyps_finite = result();
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
@@ -281,7 +276,7 @@
val [premp,sat] = goal PropThms.thy
"[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
by (rtac (premp RS hyps_finite RS Fin_induct) 1);
-by (SIMP_TAC (prop_ss addrews [premp, sat, sat_thms_p, Diff_0]) 1);
+by (simp_tac (prop_ss addsimps [premp, sat, sat_thms_p, Diff_0]) 1);
by (safe_tac ZF_cs);
(*Case hyps(p,t)-cons(#v,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
@@ -309,7 +304,7 @@
(*A semantic analogue of the Deduction Theorem*)
goalw PropThms.thy [sat_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
-by (SIMP_TAC prop_ss 1);
+by (simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val sat_Imp = result();
--- a/src/ZF/ex/ramsey.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/ramsey.ML Fri Sep 17 16:52:10 1993 +0200
@@ -20,9 +20,6 @@
open Ramsey;
-val ramsey_congs = mk_congs Ramsey.thy ["Atleast"];
-val ramsey_ss = arith_ss addcongs ramsey_congs;
-
(*** Cliques and Independent sets ***)
goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
@@ -95,11 +92,12 @@
\ Atleast(m,A) | Atleast(n,B)";
by (nat_ind_tac "m" prems 1);
by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
-by (ASM_SIMP_TAC ramsey_ss 1);
+by (asm_simp_tac arith_ss 1);
by (rtac ballI 1);
+by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*)
by (nat_ind_tac "n" [] 1);
by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
-by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
by (safe_tac ZF_cs);
by (etac (Atleast_succD RS bexE) 1);
by (etac UnE 1);
@@ -118,7 +116,7 @@
(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
(*proving the condition*)
-by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
+by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
val pigeon2_lemma = result();
@@ -147,7 +145,7 @@
"[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \
\ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
by (rtac (nat_succI RS pigeon2) 1);
-by (SIMP_TAC (ramsey_ss addrews prems) 3);
+by (simp_tac (arith_ss addsimps prems) 3);
by (rtac Atleast_superset 3);
by (REPEAT (resolve_tac prems 1));
by (fast_tac ZF_cs 1);
--- a/src/ZF/ex/termfn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/termfn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -18,11 +18,11 @@
"[| l: list(A); Ord(i) |] ==> \
\ rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
by (rtac (major RS List.induct) 1);
-by (SIMP_TAC list_ss 1);
+by (simp_tac list_ss 1);
by (rtac impI 1);
by (forward_tac [rank_Cons1 RS Ord_trans] 1);
by (dtac (rank_Cons2 RS Ord_trans) 2);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [ordi, VsetI])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [ordi, VsetI])));
val map_lemma = result();
(*Typing premise is necessary to invoke map_lemma*)
@@ -31,10 +31,8 @@
\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
by (rtac (term_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac Term.con_defs);
-val term_rec_ss = ZF_ss
- addcongs (mk_typed_congs TermFn.thy [("d", "[i,i,i]=>i")])
- addrews [Ord_rank, rank_pair2, prem RS map_lemma];
-by (SIMP_TAC term_rec_ss 1);
+val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
+by (simp_tac term_rec_ss 1);
val term_rec = result();
(*Slightly odd typing condition on r in the second premise!*)
@@ -49,7 +47,7 @@
by (rtac (term_rec RS ssubst) 1);
by (REPEAT (ares_tac prems 1));
by (etac List.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [term_rec])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
by (etac CollectE 1);
by (REPEAT (ares_tac [ConsI, UN_I] 1));
val term_rec_type = result();
@@ -122,31 +120,27 @@
(*map_type2 and term_map_type2 instantiate variables*)
val term_ss = list_ss
- addcongs (Term.congs @
- mk_congs TermFn.thy ["term_rec","term_map","term_size",
- "reflect","preorder"])
- addrews [term_rec, term_map, term_size, reflect,
- preorder]
- setauto type_auto_tac (list_typechecks@term_typechecks);
+ addsimps [term_rec, term_map, term_size, reflect, preorder]
+ setsolver type_auto_tac (list_typechecks@term_typechecks);
(** theorems about term_map **)
goal TermFn.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_ident]) 1);
+by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
val term_map_ident = result();
goal TermFn.thy
"!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
val term_map_compose = result();
goal TermFn.thy
"!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
val term_map_reflect = result();
@@ -155,18 +149,18 @@
goal TermFn.thy
"!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
val term_size_term_map = result();
goal TermFn.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose,
- list_add_rev]) 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
+ list_add_rev]) 1);
val term_size_reflect = result();
goal TermFn.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [length_flat, map_compose]) 1);
+by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
val term_size_length = result();
@@ -174,8 +168,8 @@
goal TermFn.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib, map_compose,
- map_ident, rev_rev_ident]) 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
+ map_ident, rev_rev_ident]) 1);
val reflect_reflect_ident = result();
@@ -184,7 +178,7 @@
goal TermFn.thy
"!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
by (etac term_induct_eqn 1);
-by (ASM_SIMP_TAC (term_ss addrews [map_compose, map_flat]) 1);
+by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
val preorder_term_map = result();
(** preorder(reflect(t)) = rev(postorder(t)) **)
--- a/src/ZF/ex/tf_fn.ML Fri Sep 17 16:16:38 1993 +0200
+++ b/src/ZF/ex/tf_fn.ML Fri Sep 17 16:52:10 1993 +0200
@@ -16,33 +16,29 @@
(*** TF_rec -- by Vset recursion ***)
-(*Used only to verify TF_rec*)
-val TF_congs = mk_typed_congs TF.thy
- [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
-
(** conversion rules **)
goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
-by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
+by (simp_tac rank_ss 1);
val TF_rec_Tcons = result();
goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val TF_rec_Fnil = result();
goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
\ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
-by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
+by (simp_tac rank_ss 1);
val TF_rec_Fcons = result();
(*list_ss includes list operations as well as arith_ss*)
-val TF_rec_ss = list_ss addrews
+val TF_rec_ss = list_ss addsimps
[TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
(** Type checking **)
@@ -56,7 +52,7 @@
\ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
\ |] ==> TF_rec(z,b,c,d) : C(z)";
by (rtac (major RS TF.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
val TF_rec_type = result();
(*Mutually recursive version*)
@@ -70,7 +66,7 @@
\ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
by (rewtac Ball_def);
by (rtac TF.mutual_induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
val tree_forest_rec_type = result();
@@ -159,10 +155,6 @@
[TconsI, FnilI, FconsI, treeI, forestI,
list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
-val TF_congs = TF.congs @
- mk_congs TF_Fn.thy
- ["TF_rec", "list_of_TF", "TF_of_list", "TF_map", "TF_size", "TF_preorder"];
-
val TF_rewrites =
[TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
@@ -171,8 +163,8 @@
TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
-val TF_ss = list_ss addcongs TF_congs
- addrews (TF_rewrites@TF_typechecks);
+val TF_ss = list_ss addsimps TF_rewrites
+ setsolver type_auto_tac (list_typechecks@TF_typechecks);
(** theorems about list_of_TF and TF_of_list **)
@@ -188,26 +180,26 @@
goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
by (etac forest_induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val forest_iso = result();
goal TF_Fn.thy
"!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
by (etac List.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val tree_list_iso = result();
(** theorems about TF_map **)
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val TF_map_ident = result();
goal TF_Fn.thy
"!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val TF_map_compose = result();
(** theorems about TF_size **)
@@ -215,13 +207,13 @@
goal TF_Fn.thy
"!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC TF_ss));
+by (ALLGOALS (asm_simp_tac TF_ss));
val TF_size_TF_map = result();
goal TF_Fn.thy
"!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [length_app])));
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
val TF_size_length = result();
(** theorems about TF_preorder **)
@@ -229,5 +221,5 @@
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
by (etac TF.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
val TF_preorder_TF_map = result();