src/HOL/Number_Theory/Euclidean_Algorithm.thy

 
 end    
 
 lemma semiring_gcd:
   "class.semiring_gcd one zero times gcd lcm
-    divide plus minus normalize unit_factor"
+    divide plus minus unit_factor normalize"
 proof
   show "gcd a b dvd a"
     and "gcd a b dvd b" for a b
     by (induct a b rule: eucl_induct)
       (simp_all add: local.gcd_0 local.gcd_mod dvd_mod_iff)

   show "lcm a b = normalize (a * b) div gcd a b" for a b
     by (fact local.lcm_def)
 qed
 
 interpretation semiring_gcd one zero times gcd lcm
-  divide plus minus normalize unit_factor
+  divide plus minus unit_factor normalize
   by (fact semiring_gcd)
   
 lemma semiring_Gcd:
   "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
-    divide plus minus normalize unit_factor"
+    divide plus minus unit_factor normalize"
 proof -
   show ?thesis
   proof
     have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>b. (\<forall>a\<in>A. a dvd b) \<longrightarrow> Lcm A dvd b)" for A
     proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")

       by (simp add: local.Gcd_def)
   qed
 qed
 
 interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
   by (fact semiring_Gcd)
 
 subclass factorial_semiring
 proof -
   show "class.factorial_semiring divide plus minus zero times one
-     normalize unit_factor"
+     unit_factor normalize"
   proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
     fix x assume "x \<noteq> 0"
     thus "finite {p. p dvd x \<and> normalize p = p}"
     proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
       case (less x)

   "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)"
 proof
   interpret semiring_Gcd 1 0 times
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
     Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
   proof (rule ext)+
     fix a b :: 'a

 instance nat :: euclidean_semiring_gcd
 proof
   interpret semiring_Gcd 1 0 times
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
   proof (rule ext)+
     fix m n :: nat

 instance int :: euclidean_ring_gcd
 proof
   interpret semiring_Gcd 1 0 times
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
   proof (rule ext)+
     fix k l :: int