--- 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];
--- 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;
--- 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),
--- 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"],