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
```