moved nat_arith ot Nat_Numeral: clarified normalizer setup
authorhaftmann
Wed May 05 16:53:21 2010 +0200 (2010-05-05)
changeset 36699816da1023508
parent 36698 45f1a487cd27
child 36700 9b85b9d74b83
moved nat_arith ot Nat_Numeral: clarified normalizer setup
src/HOL/Groebner_Basis.thy
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed May 05 16:46:19 2010 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed May 05 16:53:21 2010 +0200
     1.3 @@ -5,10 +5,10 @@
     1.4  header {* Semiring normalization and Groebner Bases *}
     1.5  
     1.6  theory Groebner_Basis
     1.7 -imports Numeral_Simprocs
     1.8 +imports Numeral_Simprocs Nat_Transfer
     1.9  uses
    1.10    "Tools/Groebner_Basis/normalizer_data.ML"
    1.11 -  ("Tools/Groebner_Basis/normalizer.ML")
    1.12 +  "Tools/Groebner_Basis/normalizer.ML"
    1.13    ("Tools/Groebner_Basis/groebner.ML")
    1.14  begin
    1.15  
    1.16 @@ -16,7 +16,6 @@
    1.17  
    1.18  setup NormalizerData.setup
    1.19  
    1.20 -
    1.21  locale gb_semiring =
    1.22    fixes add mul pwr r0 r1
    1.23    assumes add_a:"(add x (add y z) = add (add x y) z)"
     2.1 --- a/src/HOL/Nat_Numeral.thy	Wed May 05 16:46:19 2010 +0200
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Wed May 05 16:53:21 2010 +0200
     2.3 @@ -687,6 +687,13 @@
     2.4  lemmas nat_number' =
     2.5    nat_number_of_Bit0 nat_number_of_Bit1
     2.6  
     2.7 +lemmas nat_arith =
     2.8 +  add_nat_number_of
     2.9 +  diff_nat_number_of
    2.10 +  mult_nat_number_of
    2.11 +  eq_nat_number_of
    2.12 +  less_nat_number_of
    2.13 +
    2.14  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
    2.15    by (fact Let_def)
    2.16