src/HOL/Semiring_Normalization.thy

 header {* Semiring normalization *}
 
 theory Semiring_Normalization
 imports Numeral_Simprocs Nat_Transfer
 uses
-  "Tools/Groebner_Basis/normalizer.ML"
-begin
-
-setup Normalizer.setup
+  "Tools/semiring_normalizer.ML"
+begin
+
+setup Semiring_Normalizer.setup
 
 locale normalizing_semiring =
   fixes add mul pwr r0 r1
   assumes add_a:"(add x (add y z) = add (add x y) z)"
     and add_c: "add x y = add y x" and add_0:"add r0 x = x"

 sublocale comm_semiring_1
   < normalizing!: normalizing_semiring plus times power zero one
 proof
 qed (simp_all add: algebra_simps)
 
-declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
+declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *}
 
 locale normalizing_ring = normalizing_semiring +
   fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     and neg :: "'a \<Rightarrow> 'a"
   assumes neg_mul: "neg x = mul (neg r1) x"

 sublocale comm_ring_1
   < normalizing!: normalizing_ring plus times power zero one minus uminus
 proof
 qed (simp_all add: diff_minus)
 
-declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
+declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *}
 
 locale normalizing_field = normalizing_ring +
   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     and inverse:: "'a \<Rightarrow> 'a"
   assumes divide_inverse: "divide x y = mul x (inverse y)"

     then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
     then show "w = x \<or> y = z" by auto
   qed (auto simp add: add_ac)
 qed (simp_all add: algebra_simps)
 
-declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
+declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *}
 
 interpretation normalizing_nat!: normalizing_semiring_cancel
   "op +" "op *" "op ^" "0::nat" "1"
 proof (unfold_locales, simp add: algebra_simps)
   fix w x y z ::"nat"

       hence "w = x" using kp by simp }
     ultimately have "w=x" by blast }
   thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
 qed
 
-declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
+declaration {* Semiring_Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *}
 
 locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field
 begin
 
 declare normalizing_field_axioms' [normalizer del]

 sublocale field 
   < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse
 proof
 qed (simp_all add: divide_inverse)
 
-declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
-
-end
+declaration {* Semiring_Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *}
+
+end