src/HOL/Groebner_Basis.thy
changeset 23327 1654013ec97c
parent 23312 6e32a5bfc30f
child 23330 01c09922ce59
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 16:21:03 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Jun 11 16:23:17 2007 +0200
     1.3 @@ -260,6 +260,22 @@
     1.4  *} "Semiring_normalizer"
     1.5  
     1.6  
     1.7 +locale gb_field = gb_ring +
     1.8 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9 +    and inverse:: "'a \<Rightarrow> 'a"
    1.10 +  assumes divide: "divide x y = mul x (inverse y)"
    1.11 +     and inverse: "inverse x = divide r1 x"
    1.12 +begin
    1.13 +
    1.14 +lemma "axioms" [normalizer
    1.15 +  semiring ops: semiring_ops
    1.16 +  semiring rules: semiring_rules
    1.17 +  ring ops: ring_ops
    1.18 +  ring rules: ring_rules]:
    1.19 +  "gb_field add mul pwr r0 r1 sub neg divide inverse" .
    1.20 +
    1.21 +end
    1.22 +
    1.23  subsection {* Groebner Bases *}
    1.24  
    1.25  locale semiringb = gb_semiring +
    1.26 @@ -384,6 +400,21 @@
    1.27      conv = fn phi => numeral_conv}
    1.28  *}
    1.29  
    1.30 +locale fieldgb = ringb + gb_field
    1.31 +begin
    1.32 +
    1.33 +declare "axioms" [normalizer del]
    1.34 +
    1.35 +lemma "axioms" [normalizer
    1.36 +  semiring ops: semiring_ops
    1.37 +  semiring rules: semiring_rules
    1.38 +  ring ops: ring_ops
    1.39 +  ring rules: ring_rules
    1.40 +  idom rules: noteq_reduce add_scale_eq_noteq]:
    1.41 +  "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
    1.42 +end
    1.43 +
    1.44 +
    1.45  
    1.46  lemmas bool_simps = simp_thms(1-34)
    1.47  lemma dnf:
    1.48 @@ -414,4 +445,6 @@
    1.49    Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
    1.50  *} ""
    1.51  
    1.52 +
    1.53 +
    1.54  end