src/HOL/RealVector.thy

   fixes x :: "'a::real_div_algebra" shows
   "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
 by (rule inverse_unique, simp)
 
 lemma inverse_scaleR_distrib:
-  fixes x :: "'a::{real_div_algebra,division_by_zero}"
+  fixes x :: "'a::{real_div_algebra,division_ring_inverse_zero}"
   shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
 apply (case_tac "a = 0", simp)
 apply (case_tac "x = 0", simp)
 apply (erule (1) nonzero_inverse_scaleR_distrib)
 done

    inverse (of_real x :: 'a::real_div_algebra)"
 by (simp add: of_real_def nonzero_inverse_scaleR_distrib)
 
 lemma of_real_inverse [simp]:
   "of_real (inverse x) =
-   inverse (of_real x :: 'a::{real_div_algebra,division_by_zero})"
+   inverse (of_real x :: 'a::{real_div_algebra,division_ring_inverse_zero})"
 by (simp add: of_real_def inverse_scaleR_distrib)
 
 lemma nonzero_of_real_divide:
   "y \<noteq> 0 \<Longrightarrow> of_real (x / y) =
    (of_real x / of_real y :: 'a::real_field)"
 by (simp add: divide_inverse nonzero_of_real_inverse)
 
 lemma of_real_divide [simp]:
   "of_real (x / y) =
-   (of_real x / of_real y :: 'a::{real_field,division_by_zero})"
+   (of_real x / of_real y :: 'a::{real_field,division_ring_inverse_zero})"
 by (simp add: divide_inverse)
 
 lemma of_real_power [simp]:
   "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
 by (induct n) simp_all

 apply (rule range_eqI)
 apply (erule nonzero_of_real_inverse [symmetric])
 done
 
 lemma Reals_inverse [simp]:
-  fixes a :: "'a::{real_div_algebra,division_by_zero}"
+  fixes a :: "'a::{real_div_algebra,division_ring_inverse_zero}"
   shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_inverse [symmetric])
 done

 apply (rule range_eqI)
 apply (erule nonzero_of_real_divide [symmetric])
 done
 
 lemma Reals_divide [simp]:
-  fixes a b :: "'a::{real_field,division_by_zero}"
+  fixes a b :: "'a::{real_field,division_ring_inverse_zero}"
   shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_divide [symmetric])
 done

 apply (rule inverse_unique [symmetric])
 apply (simp add: norm_mult [symmetric])
 done
 
 lemma norm_inverse:
-  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
+  fixes a :: "'a::{real_normed_div_algebra,division_ring_inverse_zero}"
   shows "norm (inverse a) = inverse (norm a)"
 apply (case_tac "a = 0", simp)
 apply (erule nonzero_norm_inverse)
 done
 

   fixes a b :: "'a::real_normed_field"
   shows "b \<noteq> 0 \<Longrightarrow> norm (a / b) = norm a / norm b"
 by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
 
 lemma norm_divide:
-  fixes a b :: "'a::{real_normed_field,division_by_zero}"
+  fixes a b :: "'a::{real_normed_field,division_ring_inverse_zero}"
   shows "norm (a / b) = norm a / norm b"
 by (simp add: divide_inverse norm_mult norm_inverse)
 
 lemma norm_power_ineq:
   fixes x :: "'a::{real_normed_algebra_1}"