diff -r eebe69f31474 -r 58043346ca64 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Tue Mar 31 16:49:41 2015 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Tue Mar 31 21:54:32 2015 +0200 @@ -221,7 +221,7 @@ by (rule inverse_unique, simp) lemma inverse_scaleR_distrib: - fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}" + fixes x :: "'a::{real_div_algebra, division_ring}" shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)" apply (case_tac "a = 0", simp) apply (case_tac "x = 0", simp) @@ -270,7 +270,7 @@ lemma of_real_inverse [simp]: "of_real (inverse x) = - inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})" + inverse (of_real x :: 'a::{real_div_algebra, division_ring})" by (simp add: of_real_def inverse_scaleR_distrib) lemma nonzero_of_real_divide: @@ -280,7 +280,7 @@ lemma of_real_divide [simp]: "of_real (x / y) = - (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})" + (of_real x / of_real y :: 'a::{real_field, field})" by (simp add: divide_inverse) lemma of_real_power [simp]: @@ -398,7 +398,7 @@ done lemma Reals_inverse: - fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}" + fixes a :: "'a::{real_div_algebra, division_ring}" shows "a \ Reals \ inverse a \ Reals" apply (auto simp add: Reals_def) apply (rule range_eqI) @@ -406,7 +406,7 @@ done lemma Reals_inverse_iff [simp]: - fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}" + fixes x:: "'a :: {real_div_algebra, division_ring}" shows "inverse x \ \ \ x \ \" by (metis Reals_inverse inverse_inverse_eq) @@ -419,7 +419,7 @@ done lemma Reals_divide [simp]: - fixes a b :: "'a::{real_field, field_inverse_zero}" + fixes a b :: "'a::{real_field, field}" shows "\a \ Reals; b \ Reals\ \ a / b \ Reals" apply (auto simp add: Reals_def) apply (rule range_eqI) @@ -819,7 +819,7 @@ done lemma norm_inverse: - fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}" + fixes a :: "'a::{real_normed_div_algebra, division_ring}" shows "norm (inverse a) = inverse (norm a)" apply (case_tac "a = 0", simp) apply (erule nonzero_norm_inverse) @@ -831,7 +831,7 @@ by (simp add: divide_inverse norm_mult nonzero_norm_inverse) lemma norm_divide: - fixes a b :: "'a::{real_normed_field, field_inverse_zero}" + fixes a b :: "'a::{real_normed_field, field}" shows "norm (a / b) = norm a / norm b" by (simp add: divide_inverse norm_mult norm_inverse)