src/HOL/Complex/NSCA.thy
changeset 14469 c7674b7034f5
parent 14430 5cb24165a2e1
child 14653 0848ab6fe5fc
     1.1 --- a/src/HOL/Complex/NSCA.thy	Mon Mar 15 10:46:19 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Mon Mar 15 10:58:29 2004 +0100
     1.3 @@ -724,8 +724,7 @@
     1.4  
     1.5  lemma hcomplex_of_hypreal_capprox_iff [simp]:
     1.6       "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
     1.7 -apply (rule eq_Abs_hypreal [of x])
     1.8 -apply (rule eq_Abs_hypreal [of z])
     1.9 +apply (cases x, cases z)
    1.10  apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
    1.11  done
    1.12  
    1.13 @@ -1133,13 +1132,13 @@
    1.14  
    1.15  lemma CFinite_HFinite_hcomplex_of_hypreal:
    1.16       "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
    1.17 -apply (rule eq_Abs_hypreal [of z])
    1.18 +apply (cases z)
    1.19  apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
    1.20  done
    1.21  
    1.22  lemma SComplex_SReal_hcomplex_of_hypreal:
    1.23       "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
    1.24 -apply (rule eq_Abs_hypreal [of x])
    1.25 +apply (cases x)
    1.26  apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
    1.27  done
    1.28  
    1.29 @@ -1178,32 +1177,28 @@
    1.30  lemma hcomplex_split_CInfinitesimal_iff:
    1.31       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
    1.32        (x \<in> Infinitesimal & y \<in> Infinitesimal)"
    1.33 -apply (rule eq_Abs_hypreal [of x])
    1.34 -apply (rule eq_Abs_hypreal [of y])
    1.35 +apply (cases x, cases y)
    1.36  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
    1.37  done
    1.38  
    1.39  lemma hcomplex_split_CFinite_iff:
    1.40       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
    1.41        (x \<in> HFinite & y \<in> HFinite)"
    1.42 -apply (rule eq_Abs_hypreal [of x])
    1.43 -apply (rule eq_Abs_hypreal [of y])
    1.44 +apply (cases x, cases y)
    1.45  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
    1.46  done
    1.47  
    1.48  lemma hcomplex_split_SComplex_iff:
    1.49       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
    1.50        (x \<in> Reals & y \<in> Reals)"
    1.51 -apply (rule eq_Abs_hypreal [of x])
    1.52 -apply (rule eq_Abs_hypreal [of y])
    1.53 +apply (cases x, cases y)
    1.54  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
    1.55  done
    1.56  
    1.57  lemma hcomplex_split_CInfinite_iff:
    1.58       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
    1.59        (x \<in> HInfinite | y \<in> HInfinite)"
    1.60 -apply (rule eq_Abs_hypreal [of x])
    1.61 -apply (rule eq_Abs_hypreal [of y])
    1.62 +apply (cases x, cases y)
    1.63  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
    1.64  done
    1.65  
    1.66 @@ -1211,10 +1206,7 @@
    1.67       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
    1.68         hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
    1.69        (x @= x' & y @= y')"
    1.70 -apply (rule eq_Abs_hypreal [of x])
    1.71 -apply (rule eq_Abs_hypreal [of y])
    1.72 -apply (rule eq_Abs_hypreal [of x'])
    1.73 -apply (rule eq_Abs_hypreal [of y'])
    1.74 +apply (cases x, cases y, cases x', cases y')
    1.75  apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
    1.76  done
    1.77