src/HOL/Computational_Algebra/Field_as_Ring.thy

 definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   where [simp]: "mod_field x y = (if y = 0 then x else 0)"
 
 end
 
-instantiation real :: unique_euclidean_ring
+instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
 definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"

 
 instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
 
 end
 
-instantiation rat :: unique_euclidean_ring
+instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
 definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"

 
 instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
 
 end
 
-instantiation complex :: unique_euclidean_ring
+instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
 definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"