# HG changeset patch # User haftmann # Date 1316212641 -7200 # Node ID 2625de88c994b2544e047b54cdeb57cdc5a0aabc # Parent f136409c2ceff573fdd738f95534151d47bcd22e tuned diff -r f136409c2cef -r 2625de88c994 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Sat Sep 17 04:41:44 2011 +0200 +++ b/src/HOL/NSA/NSA.thy Sat Sep 17 00:37:21 2011 +0200 @@ -681,9 +681,10 @@ meta_number_of_approx_reorient); in -val approx_reorient_simproc = - Arith_Data.prep_simproc @{theory} - ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc); + +val approx_reorient_simproc = Simplifier.simproc_global @{theory} + "reorient_simproc" ["0@=x", "1@=x", "number_of w @= x"] reorient_proc; + end; Addsimprocs [approx_reorient_simproc]; diff -r f136409c2cef -r 2625de88c994 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Sat Sep 17 04:41:44 2011 +0200 +++ b/src/HOL/Tools/arith_data.ML Sat Sep 17 00:37:21 2011 +0200 @@ -21,9 +21,6 @@ val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm val simp_all_tac: thm list -> simpset -> tactic val simplify_meta_eq: thm list -> simpset -> thm -> thm - val trans_tac: thm option -> tactic - val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option) - -> simproc val setup: theory -> theory end; @@ -80,21 +77,20 @@ in Const (@{const_name Groups.uminus}, T --> T) $ t end; (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) -fun mk_sum T [] = mk_number T 0 - | mk_sum T [t,u] = mk_plus (t, u) +fun mk_sum T [] = mk_number T 0 + | mk_sum T [t, u] = mk_plus (t, u) | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); (*this version ALWAYS includes a trailing zero*) -fun long_mk_sum T [] = mk_number T 0 +fun long_mk_sum T [] = mk_number T 0 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); (*decompose additions AND subtractions as a sum*) fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (pos, u, ts)) + dest_summing (pos, t, dest_summing (pos, u, ts)) | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (not pos, u, ts)) - | dest_summing (pos, t, ts) = - if pos then t::ts else mk_minus t :: ts; + dest_summing (pos, t, dest_summing (not pos, u, ts)) + | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts; fun dest_sum t = dest_summing (true, t, []); @@ -121,10 +117,4 @@ let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end -fun trans_tac NONE = all_tac - | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); - -fun prep_simproc thy (name, pats, proc) = - Simplifier.simproc_global thy name pats proc; - end; diff -r f136409c2cef -r 2625de88c994 src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Sep 17 04:41:44 2011 +0200 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Sep 17 00:37:21 2011 +0200 @@ -18,8 +18,7 @@ val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; val numeral_sym_ss = HOL_ss addsimps numeral_syms; -fun rename_numerals th = - simplify numeral_sym_ss (Thm.transfer @{theory} th); +val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory}; (*Utilities*) @@ -143,13 +142,13 @@ (*** Applying CancelNumeralsFun ***) structure CancelNumeralsCommon = - struct - val mk_sum = (fn T:typ => mk_sum) - val dest_sum = dest_Sucs_sum true - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first_coeff = find_first_coeff [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = (fn T : typ => mk_sum) + val dest_sum = dest_Sucs_sum true + 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 norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac} @@ -161,12 +160,11 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); val simplify_meta_eq = simplify_meta_eq - end; - + val prove_conv = Arith_Data.prove_conv +end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT val bal_add1 = @{thm nat_eq_add_iff1} RS trans @@ -175,7 +173,6 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val bal_add1 = @{thm nat_less_add_iff1} RS trans @@ -184,7 +181,6 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT val bal_add1 = @{thm nat_le_add_iff1} RS trans @@ -193,7 +189,6 @@ structure DiffCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT val bal_add1 = @{thm nat_diff_add_eq1} RS trans @@ -202,7 +197,7 @@ val cancel_numerals = - map (Arith_Data.prep_simproc @{theory}) + map (Numeral_Simprocs.prep_simproc @{theory}) [("nateq_cancel_numerals", ["(l::nat) + m = n", "(l::nat) = m + n", "(l::nat) * m = n", "(l::nat) = m * n", @@ -228,17 +223,17 @@ (*** Applying CombineNumeralsFun ***) structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) - val dest_sum = dest_Sucs_sum false - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val left_distrib = @{thm left_add_mult_distrib} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - fun trans_tac _ = Arith_Data.trans_tac +struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = (fn T : typ => long_mk_sum) (*to work for 2*x + 3*x *) + val dest_sum = dest_Sucs_sum false + val mk_coeff = mk_coeff + 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 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} @@ -248,23 +243,23 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = simplify_meta_eq - end; + val simplify_meta_eq = simplify_meta_eq +end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); val combine_numerals = - Arith_Data.prep_simproc @{theory} + Numeral_Simprocs.prep_simproc @{theory} ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); (*** Applying CancelNumeralFactorFun ***) structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val trans_tac = K 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} @@ -275,48 +270,44 @@ val numeral_simp_ss = HOL_ss addsimps bin_simps fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = simplify_meta_eq - end + val simplify_meta_eq = simplify_meta_eq + val prove_conv = Arith_Data.prove_conv +end; structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT val cancel = @{thm nat_mult_div_cancel1} RS trans val neg_exchanges = false -) +); structure DvdCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT val cancel = @{thm nat_mult_dvd_cancel1} RS trans val neg_exchanges = false -) +); structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT val cancel = @{thm nat_mult_eq_cancel1} RS trans val neg_exchanges = false -) +); structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT val cancel = @{thm nat_mult_less_cancel1} RS trans val neg_exchanges = true -) +); structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT val cancel = @{thm nat_mult_le_cancel1} RS trans @@ -324,7 +315,7 @@ ) val cancel_numeral_factors = - map (Arith_Data.prep_simproc @{theory}) + map (Numeral_Simprocs.prep_simproc @{theory}) [("nateq_cancel_numeral_factors", ["(l::nat) * m = n", "(l::nat) = m * n"], K EqCancelNumeralFactor.proc), @@ -364,45 +355,42 @@ simplify_one ss (([th, cancel_th]) MRS trans); structure CancelFactorCommon = - struct - val mk_sum = (fn T:typ => long_mk_prod) - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = (fn T : typ => long_mk_prod) + val dest_sum = dest_prod + 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 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 - end; + val prove_conv = Arith_Data.prove_conv +end; structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj} ); +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT + fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} +); + structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} ); -structure LeCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT - fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} -); - structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj} @@ -410,14 +398,13 @@ structure DvdCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} ); val cancel_factor = - map (Arith_Data.prep_simproc @{theory}) + map (Numeral_Simprocs.prep_simproc @{theory}) [("nat_eq_cancel_factor", ["(l::nat) * m = n", "(l::nat) = m * n"], K EqCancelFactor.proc), diff -r f136409c2cef -r 2625de88c994 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Sat Sep 17 04:41:44 2011 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat Sep 17 00:37:21 2011 +0200 @@ -16,6 +16,9 @@ signature NUMERAL_SIMPROCS = sig + val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option) + -> simproc + val trans_tac: thm option -> tactic val assoc_fold_simproc: simproc val combine_numerals: simproc val cancel_numerals: simproc list @@ -30,6 +33,12 @@ structure Numeral_Simprocs : NUMERAL_SIMPROCS = struct +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)); + val mk_number = Arith_Data.mk_number; val mk_sum = Arith_Data.mk_sum; val long_mk_sum = Arith_Data.long_mk_sum; @@ -199,13 +208,13 @@ val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} structure CancelNumeralsCommon = - struct - val mk_sum = 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 _ = Arith_Data.trans_tac +struct + val mk_sum = 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 = K trans_tac fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -215,12 +224,11 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; - + val prove_conv = Arith_Data.prove_conv +end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT val bal_add1 = @{thm eq_add_iff1} RS trans @@ -229,7 +237,6 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val bal_add1 = @{thm less_add_iff1} RS trans @@ -238,7 +245,6 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT val bal_add1 = @{thm le_add_iff1} RS trans @@ -246,7 +252,7 @@ ); val cancel_numerals = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("inteq_cancel_numerals", ["(l::'a::number_ring) + m = n", "(l::'a::number_ring) = m + n", @@ -273,17 +279,17 @@ K LeCancelNumerals.proc)]; structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - fun trans_tac _ = Arith_Data.trans_tac +struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) + val dest_sum = dest_sum + val mk_coeff = mk_coeff + 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 fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) @@ -293,23 +299,23 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; +end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); (*Version for fields, where coefficients can be fractions*) structure FieldCombineNumeralsData = - struct - type coeff = int * int - val iszero = (fn (p, q) => p = 0) - val add = add_frac - val mk_sum = long_mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_fcoeff - val dest_coeff = dest_fcoeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - fun trans_tac _ = Arith_Data.trans_tac +struct + type coeff = int * int + val iszero = (fn (p, q) => p = 0) + val add = add_frac + val mk_sum = long_mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_fcoeff + 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 norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps fun norm_tac ss = @@ -320,18 +326,18 @@ val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) - end; +end; structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); val combine_numerals = - Arith_Data.prep_simproc @{theory} + prep_simproc @{theory} ("int_combine_numerals", ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], K CombineNumerals.proc); val field_combine_numerals = - Arith_Data.prep_simproc @{theory} + prep_simproc @{theory} ("field_combine_numerals", ["(i::'a::{field_inverse_zero, number_ring}) + j", "(i::'a::{field_inverse_zero, number_ring}) - j"], @@ -351,15 +357,15 @@ structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); val assoc_fold_simproc = - Arith_Data.prep_simproc @{theory} + prep_simproc @{theory} ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], K Semiring_Times_Assoc.proc); structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val trans_tac = K trans_tac val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps @@ -375,12 +381,12 @@ val simplify_meta_eq = Arith_Data.simplify_meta_eq [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; - end + val prove_conv = Arith_Data.prove_conv +end (*Version for semiring_div*) structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT val cancel = @{thm div_mult_mult1} RS trans @@ -390,7 +396,6 @@ (*Version for fields*) structure DivideCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT val cancel = @{thm mult_divide_mult_cancel_left} RS trans @@ -399,7 +404,6 @@ structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT val cancel = @{thm mult_cancel_left} RS trans @@ -408,7 +412,6 @@ structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val cancel = @{thm mult_less_cancel_left} RS trans @@ -417,7 +420,6 @@ structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT val cancel = @{thm mult_le_cancel_left} RS trans @@ -425,7 +427,7 @@ ) val cancel_numeral_factors = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("ring_eq_cancel_numeral_factor", ["(l::'a::{idom,number_ring}) * m = n", "(l::'a::{idom,number_ring}) = m * n"], @@ -449,7 +451,7 @@ K DivideCancelNumeralFactor.proc)]; val field_cancel_numeral_factors = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("field_eq_cancel_numeral_factor", ["(l::'a::{field,number_ring}) * m = n", "(l::'a::{field,number_ring}) = m * n"], @@ -499,22 +501,22 @@ end structure CancelFactorCommon = - struct - val mk_sum = long_mk_prod - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - fun trans_tac _ = Arith_Data.trans_tac +struct + val mk_sum = long_mk_prod + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = K 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 - end; + val prove_conv = Arith_Data.prove_conv +end; (*mult_cancel_left requires a ring with no zero divisors.*) structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT fun simp_conv _ _ = SOME @{thm mult_cancel_left} @@ -523,7 +525,6 @@ (*for ordered rings*) structure LeCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT val simp_conv = sign_conv @@ -533,7 +534,6 @@ (*for ordered rings*) structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT val simp_conv = sign_conv @@ -543,7 +543,6 @@ (*for semirings with division*) structure DivCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.div} val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT fun simp_conv _ _ = SOME @{thm div_mult_mult1_if} @@ -551,7 +550,6 @@ structure ModCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT fun simp_conv _ _ = SOME @{thm mod_mult_mult1} @@ -560,7 +558,6 @@ (*for idoms*) structure DvdCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} @@ -569,14 +566,13 @@ (*Version for all fields, including unordered ones (type complex).*) structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} ); val cancel_factors = - map (Arith_Data.prep_simproc @{theory}) + map (prep_simproc @{theory}) [("ring_eq_cancel_factor", ["(l::'a::idom) * m = n", "(l::'a::idom) = m * n"],