removed division_by_zero class requirements from several lemmas
authorhuffman
Thu Sep 21 03:17:51 2006 +0200 (2006-09-21)
changeset 2065324cda2c5fd40
parent 20652 6e9b7617c89a
child 20654 d80502f0d701
removed division_by_zero class requirements from several lemmas
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/SEQ.thy
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 21 03:16:50 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Thu Sep 21 03:17:51 2006 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4  
     1.5  
     1.6  lemma NSLIM_inverse:
     1.7 -  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
     1.8 +  fixes L :: "'a::real_normed_div_algebra"
     1.9    shows "[| f -- a --NS> L;  L \<noteq> 0 |]
    1.10        ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
    1.11  apply (simp add: NSLIM_def, clarify)
    1.12 @@ -339,7 +339,7 @@
    1.13  done
    1.14  
    1.15  lemma LIM_inverse:
    1.16 -  fixes L :: "'a::{real_normed_div_algebra,division_by_zero}"
    1.17 +  fixes L :: "'a::real_normed_div_algebra"
    1.18    shows "[| f -- a --> L; L \<noteq> 0 |]
    1.19        ==> (%x. inverse(f(x))) -- a --> (inverse L)"
    1.20  by (simp add: LIM_NSLIM_iff NSLIM_inverse)
    1.21 @@ -514,16 +514,14 @@
    1.22  by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
    1.23  
    1.24  lemma isCont_inverse:
    1.25 -  fixes f :: "'a::real_normed_vector \<Rightarrow>
    1.26 -              'b::{real_normed_div_algebra,division_by_zero}"
    1.27 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
    1.28    shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
    1.29  apply (simp add: isCont_def)
    1.30  apply (blast intro: LIM_inverse)
    1.31  done
    1.32  
    1.33  lemma isNSCont_inverse:
    1.34 -  fixes f :: "'a::real_normed_vector \<Rightarrow>
    1.35 -              'b::{real_normed_div_algebra,division_by_zero}"
    1.36 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
    1.37    shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
    1.38  by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
    1.39  
     2.1 --- a/src/HOL/Hyperreal/SEQ.thy	Thu Sep 21 03:16:50 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Thu Sep 21 03:17:51 2006 +0200
     2.3 @@ -264,25 +264,25 @@
     2.4  
     2.5  text{*Proof is like that of @{text NSLIM_inverse}.*}
     2.6  lemma NSLIMSEQ_inverse:
     2.7 -  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
     2.8 +  fixes a :: "'a::real_normed_div_algebra"
     2.9    shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
    2.10  by (simp add: NSLIMSEQ_def star_of_approx_inverse)
    2.11  
    2.12  
    2.13  text{*Standard version of theorem*}
    2.14  lemma LIMSEQ_inverse:
    2.15 -  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
    2.16 +  fixes a :: "'a::real_normed_div_algebra"
    2.17    shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
    2.18  by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
    2.19  
    2.20  lemma NSLIMSEQ_mult_inverse:
    2.21 -  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
    2.22 +  fixes a b :: "'a::{real_normed_div_algebra,field}"
    2.23    shows
    2.24       "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
    2.25  by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
    2.26  
    2.27  lemma LIMSEQ_divide:
    2.28 -  fixes a b :: "'a::{real_normed_div_algebra,field,division_by_zero}"
    2.29 +  fixes a b :: "'a::{real_normed_div_algebra,field}"
    2.30    shows "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
    2.31  by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
    2.32