1.1 --- a/src/HOL/Groebner_Basis.thy Thu Dec 04 13:30:09 2008 -0800
1.2 +++ b/src/HOL/Groebner_Basis.thy Thu Dec 04 16:05:45 2008 -0800
1.3 @@ -169,7 +169,11 @@
1.4 proof qed (auto simp add: ring_simps power_Suc)
1.5
1.6 lemmas nat_arith =
1.7 - add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
1.8 + add_nat_number_of
1.9 + diff_nat_number_of
1.10 + mult_nat_number_of
1.11 + eq_nat_number_of
1.12 + less_nat_number_of
1.13
1.14 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
1.15 by (simp add: numeral_1_eq_1)
1.16 @@ -458,7 +462,6 @@
1.17 declare zmod_eq_dvd_iff[algebra]
1.18 declare nat_mod_eq_iff[algebra]
1.19
1.20 -
1.21 subsection{* Groebner Bases for fields *}
1.22
1.23 interpretation class_fieldgb:
1.24 @@ -607,14 +610,6 @@
1.25 @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
1.26 name = "ord_frac_simproc", proc = proc3, identifier = []}
1.27
1.28 -val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of",
1.29 - "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]
1.30 -
1.31 -val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0",
1.32 - "add_Suc", "add_number_of_left", "mult_number_of_left",
1.33 - "Suc_eq_add_numeral_1"])@
1.34 - (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
1.35 - @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
1.36 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
1.37 @{thm "divide_Numeral1"},
1.38 @{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"},
1.39 @@ -630,7 +625,7 @@
1.40 in
1.41 val comp_conv = (Simplifier.rewrite
1.42 (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
1.43 - addsimps ths addsimps comp_arith addsimps simp_thms
1.44 + addsimps ths addsimps simp_thms
1.45 addsimprocs field_cancel_numeral_factors
1.46 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
1.47 ord_frac_simproc]