renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
authorwenzelm
Tue Jun 05 18:36:07 2007 +0200 (2007-06-05)
changeset 232589062e98fdab1
parent 23257 9117e228a8e3
child 23259 ccee01b8d1c5
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
src/HOL/Groebner_Basis.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Jun 05 17:16:41 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Jun 05 18:36:07 2007 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  setup NormalizerData.setup
     1.5  
     1.6  
     1.7 -locale semiring =
     1.8 +locale gb_semiring =
     1.9    fixes add mul pwr r0 r1
    1.10    assumes add_a:"(add x (add y z) = add (add x y) z)"
    1.11      and add_c: "add x y = add y x" and add_0:"add r0 x = x"
    1.12 @@ -161,11 +161,11 @@
    1.13  lemma "axioms" [normalizer
    1.14      semiring ops: semiring_ops
    1.15      semiring rules: semiring_rules]:
    1.16 -  "semiring add mul pwr r0 r1" .
    1.17 +  "gb_semiring add mul pwr r0 r1" .
    1.18  
    1.19  end
    1.20  
    1.21 -interpretation class_semiring: semiring
    1.22 +interpretation class_semiring: gb_semiring
    1.23      ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
    1.24    by unfold_locales (auto simp add: ring_eq_simps power_Suc)
    1.25  
    1.26 @@ -212,7 +212,7 @@
    1.27  *}
    1.28  
    1.29  
    1.30 -locale ring = semiring +
    1.31 +locale gb_ring = gb_semiring +
    1.32    fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.33      and neg :: "'a \<Rightarrow> 'a"
    1.34    assumes neg_mul: "neg x = mul (neg r1) x"
    1.35 @@ -230,12 +230,12 @@
    1.36    semiring rules: semiring_rules
    1.37    ring ops: ring_ops
    1.38    ring rules: ring_rules]:
    1.39 -  "ring add mul pwr r0 r1 sub neg" .
    1.40 +  "gb_ring add mul pwr r0 r1 sub neg" .
    1.41  
    1.42  end
    1.43  
    1.44  
    1.45 -interpretation class_ring: ring ["op +" "op *" "op ^"
    1.46 +interpretation class_ring: gb_ring ["op +" "op *" "op ^"
    1.47      "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
    1.48    by unfold_locales simp_all
    1.49  
    1.50 @@ -261,7 +261,7 @@
    1.51  
    1.52  subsection {* Gröbner Bases *}
    1.53  
    1.54 -locale semiringb = semiring +
    1.55 +locale semiringb = gb_semiring +
    1.56    assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
    1.57    and add_mul_solve: "add (mul w y) (mul x z) =
    1.58      add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
    1.59 @@ -297,7 +297,7 @@
    1.60  
    1.61  end
    1.62  
    1.63 -locale ringb = semiringb + ring
    1.64 +locale ringb = semiringb + gb_ring
    1.65  begin
    1.66  
    1.67  declare "axioms" [normalizer del]
    1.68 @@ -384,7 +384,7 @@
    1.69  *}
    1.70  
    1.71  
    1.72 -lemmas bool_simps =  simp_thms(1-34)
    1.73 +lemmas bool_simps = simp_thms(1-34)
    1.74  lemma dnf:
    1.75      "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
    1.76      "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"