# HG changeset patch # User wenzelm # Date 1423649916 -3600 # Node ID 2a20354c08779ae7f87aa6cf60c3dac909cc8901 # Parent d881f5288d5a13a8013dc9f7d78b0692951a3f14 proper context; tuned whitespace; diff -r d881f5288d5a -r 2a20354c0877 src/HOL/Tools/numeral_simprocs.ML --- 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; diff -r d881f5288d5a -r 2a20354c0877 src/Provers/Arith/cancel_numeral_factor.ML --- 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 *) diff -r d881f5288d5a -r 2a20354c0877 src/Provers/Arith/cancel_numerals.ML --- 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 diff -r d881f5288d5a -r 2a20354c0877 src/Provers/Arith/combine_numerals.ML --- 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 diff -r d881f5288d5a -r 2a20354c0877 src/ZF/arith_data.ML --- 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); diff -r d881f5288d5a -r 2a20354c0877 src/ZF/int_arith.ML --- 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;