src/HOL/Groebner_Basis.thy
changeset 28987 dc0ab579a5ca
parent 28986 1ff53ff7041d
child 29039 8b9207f82a78
child 29223 e09c53289830
     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]