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, normalization_euclidean_semiring}"
+instantiation real ::
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
 definition [simp]: "modulo_real = (mod_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, normalization_euclidean_semiring}"
+instance real :: field_gcd ..
+
+
+instantiation rat :: 
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
 definition [simp]: "modulo_rat = (mod_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, normalization_euclidean_semiring}"
+instance rat :: field_gcd ..
+
+
+instantiation complex ::
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
 definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"

 
 instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
 
 end
 
+instance complex :: field_gcd ..
+
 end