src/HOL/Real_Vector_Spaces.thy
changeset 59867 58043346ca64
parent 59741 5b762cd73a8e
child 60017 b785d6d06430
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4  by (rule inverse_unique, simp)
     1.5  
     1.6  lemma inverse_scaleR_distrib:
     1.7 -  fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}"
     1.8 +  fixes x :: "'a::{real_div_algebra, division_ring}"
     1.9    shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
    1.10  apply (case_tac "a = 0", simp)
    1.11  apply (case_tac "x = 0", simp)
    1.12 @@ -270,7 +270,7 @@
    1.13  
    1.14  lemma of_real_inverse [simp]:
    1.15    "of_real (inverse x) =
    1.16 -   inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})"
    1.17 +   inverse (of_real x :: 'a::{real_div_algebra, division_ring})"
    1.18  by (simp add: of_real_def inverse_scaleR_distrib)
    1.19  
    1.20  lemma nonzero_of_real_divide:
    1.21 @@ -280,7 +280,7 @@
    1.22  
    1.23  lemma of_real_divide [simp]:
    1.24    "of_real (x / y) =
    1.25 -   (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})"
    1.26 +   (of_real x / of_real y :: 'a::{real_field, field})"
    1.27  by (simp add: divide_inverse)
    1.28  
    1.29  lemma of_real_power [simp]:
    1.30 @@ -398,7 +398,7 @@
    1.31  done
    1.32  
    1.33  lemma Reals_inverse:
    1.34 -  fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
    1.35 +  fixes a :: "'a::{real_div_algebra, division_ring}"
    1.36    shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
    1.37  apply (auto simp add: Reals_def)
    1.38  apply (rule range_eqI)
    1.39 @@ -406,7 +406,7 @@
    1.40  done
    1.41  
    1.42  lemma Reals_inverse_iff [simp]: 
    1.43 -  fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}"
    1.44 +  fixes x:: "'a :: {real_div_algebra, division_ring}"
    1.45    shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
    1.46  by (metis Reals_inverse inverse_inverse_eq)
    1.47  
    1.48 @@ -419,7 +419,7 @@
    1.49  done
    1.50  
    1.51  lemma Reals_divide [simp]:
    1.52 -  fixes a b :: "'a::{real_field, field_inverse_zero}"
    1.53 +  fixes a b :: "'a::{real_field, field}"
    1.54    shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
    1.55  apply (auto simp add: Reals_def)
    1.56  apply (rule range_eqI)
    1.57 @@ -819,7 +819,7 @@
    1.58  done
    1.59  
    1.60  lemma norm_inverse:
    1.61 -  fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}"
    1.62 +  fixes a :: "'a::{real_normed_div_algebra, division_ring}"
    1.63    shows "norm (inverse a) = inverse (norm a)"
    1.64  apply (case_tac "a = 0", simp)
    1.65  apply (erule nonzero_norm_inverse)
    1.66 @@ -831,7 +831,7 @@
    1.67  by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
    1.68  
    1.69  lemma norm_divide:
    1.70 -  fixes a b :: "'a::{real_normed_field, field_inverse_zero}"
    1.71 +  fixes a b :: "'a::{real_normed_field, field}"
    1.72    shows "norm (a / b) = norm a / norm b"
    1.73  by (simp add: divide_inverse norm_mult norm_inverse)
    1.74