--- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 11 10:54:53 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 11 11:18:36 2015 +0100
@@ -18,7 +18,7 @@
sig
val prep_simproc: theory -> string * string list * (Proof.context -> term -> thm option)
-> simproc
- val trans_tac: thm option -> tactic
+ val trans_tac: Proof.context -> thm option -> tactic
val assoc_fold: Proof.context -> cterm -> thm option
val combine_numerals: Proof.context -> cterm -> thm option
val eq_cancel_numerals: Proof.context -> cterm -> thm option
@@ -48,8 +48,8 @@
fun prep_simproc thy (name, pats, proc) =
Simplifier.simproc_global thy name pats proc;
-fun trans_tac NONE = all_tac
- | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
+fun trans_tac _ NONE = all_tac
+ | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]);
val mk_number = Arith_Data.mk_number;
val mk_sum = Arith_Data.mk_sum;
--- a/src/Provers/Arith/cancel_numeral_factor.ML Wed Feb 11 10:54:53 2015 +0100
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Wed Feb 11 11:18:36 2015 +0100
@@ -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: thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: Proof.context -> tactic (*proves the initial lemma*)
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*)
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -72,7 +72,7 @@
in
Option.map (export o Data.simplify_meta_eq ctxt)
(Data.prove_conv
- [Data.trans_tac reshape, rtac Data.cancel 1,
+ [Data.trans_tac ctxt reshape, rtac Data.cancel 1,
Data.numeral_simp_tac ctxt] ctxt prems (t', rhs))
end
(* FIXME avoid handling of generic exceptions *)
--- a/src/Provers/Arith/cancel_numerals.ML Wed Feb 11 10:54:53 2015 +0100
+++ b/src/Provers/Arith/cancel_numerals.ML Wed Feb 11 11:18:36 2015 +0100
@@ -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: thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: Proof.context -> tactic (*proves the initial lemma*)
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*)
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -92,12 +92,12 @@
Option.map (export o Data.simplify_meta_eq ctxt)
(if n2 <= n1 then
Data.prove_conv
- [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add1] 1,
+ [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1,
Data.numeral_simp_tac ctxt] ctxt prems
(t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
else
Data.prove_conv
- [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add2] 1,
+ [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1,
Data.numeral_simp_tac ctxt] ctxt prems
(t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
end
--- a/src/Provers/Arith/combine_numerals.ML Wed Feb 11 10:54:53 2015 +0100
+++ b/src/Provers/Arith/combine_numerals.ML Wed Feb 11 11:18:36 2015 +0100
@@ -29,7 +29,7 @@
val left_distrib: thm
(*proof tools*)
val prove_conv: tactic list -> Proof.context -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
+ val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: Proof.context -> tactic (*proves the initial lemma*)
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*)
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
@@ -83,7 +83,7 @@
in
Option.map (export o Data.simplify_meta_eq ctxt)
(Data.prove_conv
- [Data.trans_tac reshape, resolve_tac ctxt [Data.left_distrib] 1,
+ [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.left_distrib] 1,
Data.numeral_simp_tac ctxt] ctxt
(t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
--- a/src/ZF/arith_data.ML Wed Feb 11 10:54:53 2015 +0100
+++ b/src/ZF/arith_data.ML Wed Feb 11 11:18:36 2015 +0100
@@ -9,7 +9,7 @@
(*the main outcome*)
val nat_cancel: simproc list
(*tools for use in similar applications*)
- val gen_trans_tac: thm -> thm option -> tactic
+ val gen_trans_tac: Proof.context -> thm -> thm option -> tactic
val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option
val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
(*debugging*)
@@ -50,8 +50,8 @@
| dest_sum tm = [tm];
(*Apply the given rewrite (if present) just once*)
-fun gen_trans_tac th2 NONE = all_tac
- | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve0_tac [th RS th2]);
+fun gen_trans_tac _ _ NONE = all_tac
+ | gen_trans_tac ctxt th2 (SOME th) = ALLGOALS (resolve_tac ctxt [th RS th2]);
(*Use <-> or = depending on the type of t*)
fun mk_eq_iff(t,u) =
@@ -169,7 +169,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}
- val trans_tac = gen_trans_tac @{thm iff_trans}
+ fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
end;
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -182,7 +182,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}
- val trans_tac = gen_trans_tac @{thm iff_trans}
+ fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
end;
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -195,7 +195,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}
- val trans_tac = gen_trans_tac @{thm trans}
+ fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
end;
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);
--- a/src/ZF/int_arith.ML Wed Feb 11 10:54:53 2015 +0100
+++ b/src/ZF/int_arith.ML Wed Feb 11 11:18:36 2015 +0100
@@ -151,12 +151,12 @@
structure CancelNumeralsCommon =
struct
- val mk_sum = (fn _ : typ => mk_sum)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val find_first_coeff = find_first_coeff []
- val trans_tac = ArithData.gen_trans_tac @{thm iff_trans}
+ val mk_sum = (fn _ : typ => mk_sum)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
+ fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss @{context}
@@ -233,16 +233,16 @@
structure CombineNumeralsData =
struct
- type coeff = int
- val iszero = (fn x => x = 0)
- val add = op +
- val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- 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"
- val trans_tac = ArithData.gen_trans_tac @{thm trans}
+ type coeff = int
+ val iszero = (fn x => x = 0)
+ val add = op +
+ val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ 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 ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss @{context}
@@ -281,34 +281,33 @@
structure CombineNumeralsProdData =
struct
- type coeff = int
- val iszero = (fn x => x = 0)
- val add = op *
- val mk_sum = (fn _ : typ => mk_prod)
- val dest_sum = dest_prod
- fun mk_coeff(k,t) = if t=one then mk_numeral k
- else raise TERM("mk_coeff", [])
+ type coeff = int
+ val iszero = (fn x => x = 0)
+ val add = op *
+ val mk_sum = (fn _ : typ => mk_prod)
+ val dest_sum = dest_prod
+ fun mk_coeff(k,t) =
+ if t = one then mk_numeral k
+ else raise TERM("mk_coeff", [])
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"
- val trans_tac = ArithData.gen_trans_tac @{thm trans}
-
-
+ 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 ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
-val norm_ss1 =
- simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps)
-val norm_ss2 =
- simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
- bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
-fun norm_tac ctxt =
- ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
- THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
+ val norm_ss1 =
+ simpset_of (put_simpset ZF_ss @{context} addsimps mult_1s @ diff_simps @ zminus_simps)
+ val norm_ss2 =
+ simpset_of (put_simpset ZF_ss @{context} addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
+ bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
+ fun norm_tac ctxt =
+ ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
+ THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
-val numeral_simp_ss =
- simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys)
-fun numeral_simp_tac ctxt =
- ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
-val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);
+ val numeral_simp_ss =
+ simpset_of (put_simpset ZF_ss @{context} addsimps bin_simps @ tc_rules @ intifys)
+ fun numeral_simp_tac ctxt =
+ ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
+ val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);
end;