src/HOL/Hyperreal/HTranscendental.thy
changeset 14468 6be497cacab5
parent 14430 5cb24165a2e1
child 14477 cc61fd03e589
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 15 10:46:01 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Mar 15 10:46:19 2004 +0100
     1.3 @@ -33,14 +33,14 @@
     1.4  by (simp add: starfun hypreal_one_num)
     1.5  
     1.6  lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
     1.7 -apply (rule eq_Abs_hypreal [of x])
     1.8 +apply (cases x)
     1.9  apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
    1.10                        real_sqrt_pow2_iff 
    1.11              simp del: hpowr_Suc realpow_Suc)
    1.12  done
    1.13  
    1.14  lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
    1.15 -apply (rule eq_Abs_hypreal [of x])
    1.16 +apply (cases x)
    1.17  apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
    1.18              simp add: hypreal_less starfun hrealpow hypreal_zero_num 
    1.19              simp del: hpowr_Suc realpow_Suc)
    1.20 @@ -62,8 +62,7 @@
    1.21  
    1.22  lemma hypreal_sqrt_mult_distrib: 
    1.23      "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
    1.24 -apply (rule eq_Abs_hypreal [of x])
    1.25 -apply (rule eq_Abs_hypreal [of y])
    1.26 +apply (cases x, cases y)
    1.27  apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
    1.28  apply (auto intro: real_sqrt_mult_distrib) 
    1.29  done
    1.30 @@ -101,7 +100,7 @@
    1.31  done
    1.32  
    1.33  lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
    1.34 -apply (rule eq_Abs_hypreal [of x])
    1.35 +apply (cases x)
    1.36  apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
    1.37  apply (auto intro: real_sqrt_gt_zero)
    1.38  done
    1.39 @@ -110,7 +109,7 @@
    1.40  by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
    1.41  
    1.42  lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
    1.43 -apply (rule eq_Abs_hypreal [of x])
    1.44 +apply (cases x)
    1.45  apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
    1.46  done
    1.47  
    1.48 @@ -122,7 +121,7 @@
    1.49  
    1.50  lemma hypreal_sqrt_hyperpow_hrabs [simp]:
    1.51       "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
    1.52 -apply (rule eq_Abs_hypreal [of x])
    1.53 +apply (cases x)
    1.54  apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
    1.55  done
    1.56  
    1.57 @@ -142,8 +141,7 @@
    1.58  done
    1.59  
    1.60  lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
    1.61 -apply (rule eq_Abs_hypreal [of x])
    1.62 -apply (rule eq_Abs_hypreal [of y])
    1.63 +apply (cases x, cases y)
    1.64  apply (simp add: starfun hypreal_add hrealpow hypreal_le 
    1.65              del: hpowr_Suc realpow_Suc)
    1.66  done
    1.67 @@ -274,8 +272,7 @@
    1.68  by (auto intro: STAR_exp_Infinitesimal)
    1.69  
    1.70  lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
    1.71 -apply (rule eq_Abs_hypreal [of x])
    1.72 -apply (rule eq_Abs_hypreal [of y])
    1.73 +apply (cases x, cases y)
    1.74  apply (simp add: starfun hypreal_add hypreal_mult exp_add)
    1.75  done
    1.76  
    1.77 @@ -293,7 +290,7 @@
    1.78  done
    1.79  
    1.80  lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
    1.81 -apply (rule eq_Abs_hypreal [of x])
    1.82 +apply (cases x)
    1.83  apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
    1.84  done
    1.85  
    1.86 @@ -306,7 +303,7 @@
    1.87  done
    1.88  
    1.89  lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
    1.90 -apply (rule eq_Abs_hypreal [of x])
    1.91 +apply (cases x)
    1.92  apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
    1.93  done
    1.94  
    1.95 @@ -320,7 +317,7 @@
    1.96  done
    1.97  
    1.98  lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
    1.99 -apply (rule eq_Abs_hypreal [of x])
   1.100 +apply (cases x)
   1.101  apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
   1.102  done
   1.103  
   1.104 @@ -338,12 +335,12 @@
   1.105  
   1.106  
   1.107  lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
   1.108 -apply (rule eq_Abs_hypreal [of x])
   1.109 +apply (cases x)
   1.110  apply (simp add: starfun)
   1.111  done
   1.112  
   1.113  lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
   1.114 -apply (rule eq_Abs_hypreal [of x])
   1.115 +apply (cases x)
   1.116  apply (simp add: starfun hypreal_zero_num hypreal_less)
   1.117  done
   1.118  
   1.119 @@ -351,22 +348,22 @@
   1.120  by (auto simp add: starfun)
   1.121  
   1.122  lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
   1.123 -apply (rule eq_Abs_hypreal [of x])
   1.124 +apply (cases x)
   1.125  apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
   1.126  done
   1.127  
   1.128  lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
   1.129 -apply (rule eq_Abs_hypreal [of x])
   1.130 +apply (cases x)
   1.131  apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
   1.132  done
   1.133  
   1.134  lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
   1.135 -apply (rule eq_Abs_hypreal [of x])
   1.136 +apply (cases x)
   1.137  apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   1.138  done
   1.139  
   1.140  lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
   1.141 -apply (rule eq_Abs_hypreal [of x])
   1.142 +apply (cases x)
   1.143  apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
   1.144  apply (auto dest: ln_not_eq_zero) 
   1.145  done
   1.146 @@ -379,13 +376,13 @@
   1.147  done
   1.148  
   1.149  lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
   1.150 -apply (rule eq_Abs_hypreal [of x])
   1.151 +apply (cases x)
   1.152  apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
   1.153  apply (simp add: ln_inverse)
   1.154  done
   1.155  
   1.156  lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
   1.157 -apply (rule eq_Abs_hypreal [of x])
   1.158 +apply (cases x)
   1.159  apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
   1.160  apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
   1.161  apply (rule_tac x = "exp u" in exI)
   1.162 @@ -433,7 +430,7 @@
   1.163  done
   1.164  
   1.165  lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
   1.166 -apply (rule eq_Abs_hypreal [of x])
   1.167 +apply (cases x)
   1.168  apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
   1.169  apply (auto intro: ln_less_zero) 
   1.170  done