--- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Sep 17 15:08:55 2011 +0200
@@ -148,7 +148,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val trans_tac = K Numeral_Simprocs.trans_tac
+ val trans_tac = Numeral_Simprocs.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
[@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
@@ -233,7 +233,7 @@
val dest_coeff = dest_coeff
val left_distrib = @{thm left_add_mult_distrib} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Numeral_Simprocs.trans_tac
+ val trans_tac = Numeral_Simprocs.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -259,7 +259,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
- val trans_tac = K Numeral_Simprocs.trans_tac
+ val trans_tac = Numeral_Simprocs.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
@@ -361,7 +361,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Numeral_Simprocs.trans_tac
+ val trans_tac = Numeral_Simprocs.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
--- a/src/HOL/Tools/numeral_simprocs.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Sep 17 15:08:55 2011 +0200
@@ -214,7 +214,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val trans_tac = K trans_tac
+ val trans_tac = trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -289,7 +289,7 @@
val dest_coeff = dest_coeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K trans_tac
+ val trans_tac = trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -315,7 +315,7 @@
val dest_coeff = dest_fcoeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K trans_tac
+ val trans_tac = trans_tac
val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
fun norm_tac ss =
@@ -365,7 +365,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
- val trans_tac = K trans_tac
+ val trans_tac = trans_tac
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -507,7 +507,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K trans_tac
+ val trans_tac = trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
--- a/src/Provers/Arith/cancel_numeral_factor.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Sat Sep 17 15:08:55 2011 +0200
@@ -29,7 +29,7 @@
as with < and <= but not = and div*)
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
- val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
@@ -72,7 +72,7 @@
in
Option.map (export o Data.simplify_meta_eq ss)
(Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.cancel 1,
+ [Data.trans_tac reshape, rtac Data.cancel 1,
Data.numeral_simp_tac ss] ctxt prems (t', rhs))
end
(* FIXME avoid handling of generic exceptions *)
--- a/src/Provers/Arith/cancel_numerals.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Sat Sep 17 15:08:55 2011 +0200
@@ -36,7 +36,7 @@
val bal_add2: thm
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
- val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
@@ -92,12 +92,12 @@
Option.map (export o Data.simplify_meta_eq ss)
(if n2 <= n1 then
Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
+ [Data.trans_tac reshape, rtac Data.bal_add1 1,
Data.numeral_simp_tac ss] ctxt prems
(t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
else
Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
+ [Data.trans_tac reshape, rtac Data.bal_add2 1,
Data.numeral_simp_tac ss] ctxt prems
(t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
end
--- a/src/Provers/Arith/combine_numerals.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Sat Sep 17 15:08:55 2011 +0200
@@ -29,7 +29,7 @@
val left_distrib: thm
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> term * term -> thm option
- val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
@@ -83,7 +83,7 @@
in
Option.map (export o Data.simplify_meta_eq ss)
(Data.prove_conv
- [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+ [Data.trans_tac reshape, rtac Data.left_distrib 1,
Data.numeral_simp_tac ss] ctxt
(t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
--- a/src/ZF/arith_data.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/ZF/arith_data.ML Sat Sep 17 15:08:55 2011 +0200
@@ -165,7 +165,7 @@
val dest_bal = FOLogic.dest_eq
val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans}
val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans}
- fun trans_tac _ = gen_trans_tac @{thm iff_trans}
+ val trans_tac = gen_trans_tac @{thm iff_trans}
end;
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -178,7 +178,7 @@
val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
- fun trans_tac _ = gen_trans_tac @{thm iff_trans}
+ val trans_tac = gen_trans_tac @{thm iff_trans}
end;
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -191,7 +191,7 @@
val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
- fun trans_tac _ = gen_trans_tac @{thm trans}
+ val trans_tac = gen_trans_tac @{thm trans}
end;
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
--- a/src/ZF/int_arith.ML Sat Sep 17 00:40:27 2011 +0200
+++ b/src/ZF/int_arith.ML Sat Sep 17 15:08:55 2011 +0200
@@ -156,7 +156,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- fun trans_tac _ = ArithData.gen_trans_tac @{thm iff_trans}
+ val trans_tac = ArithData.gen_trans_tac @{thm iff_trans}
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
@@ -234,7 +234,7 @@
val dest_coeff = dest_coeff 1
val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
val prove_conv = prove_conv_nohyps "int_combine_numerals"
- fun trans_tac _ = ArithData.gen_trans_tac @{thm trans}
+ val trans_tac = ArithData.gen_trans_tac @{thm trans}
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
@@ -276,7 +276,7 @@
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
- fun trans_tac _ = ArithData.gen_trans_tac @{thm trans}
+ val trans_tac = ArithData.gen_trans_tac @{thm trans}