# HG changeset patch # User lcp # Date 748277530 -7200 # Node ID 268f93ab3bc436b1e1ab79c70b38725906d63aea # Parent 8ce8c4d13d4dc17b4ae6d4318fac700a93ffc0bd 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. diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/BT_Fn.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/BinFn.ML --- 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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/Enum.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/Equiv.ML --- 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; : 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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/Integ.ML --- 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``{}))"; 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``{}) = intrel `` {}"; -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``{}) = (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``{}) $+ (intrel``{}) = intrel `` {}"; -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``{}) $* (intrel``{}) = \ \ intrel `` {}"; -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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/LList.ML --- 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"), diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/ListN.ML --- 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) ==> : 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 " : 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/PropLog.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/Ramsey.ML --- 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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/TF_Fn.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/TermFn.ML --- 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)) **) diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/binfn.ML --- 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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/bt_fn.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/enum.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/equiv.ML --- 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; : 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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/integ.ML --- 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``{}))"; 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``{}) = intrel `` {}"; -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``{}) = (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``{}) $+ (intrel``{}) = intrel `` {}"; -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``{}) $* (intrel``{}) = \ \ intrel `` {}"; -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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/listn.ML --- 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) ==> : 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 " : 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/llist.ML --- 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"), diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/misc.ML --- 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`) = g`)}) ==> \ +\ (ALL x:A. ALL y:A. H`(f`) = g`)}) --> \ \ 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."; diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/proplog.ML --- 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(); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/ramsey.ML --- 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); diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/termfn.ML --- 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)) **) diff -r 8ce8c4d13d4d -r 268f93ab3bc4 src/ZF/ex/tf_fn.ML --- 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();