src/HOL/Hyperreal/HyperPow.thy
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -163,8 +163,8 @@
     1.4  lemma hyperpow_not_zero [rule_format (no_asm)]:
     1.5       "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
     1.6  apply (simp (no_asm) add: hypreal_zero_def)
     1.7 -apply (rule_tac z = n in eq_Abs_hypnat)
     1.8 -apply (rule_tac z = r in eq_Abs_hypreal)
     1.9 +apply (rule eq_Abs_hypnat [of n])
    1.10 +apply (rule eq_Abs_hypreal [of r])
    1.11  apply (auto simp add: hyperpow)
    1.12  apply (drule FreeUltrafilterNat_Compl_mem, ultra)
    1.13  done
    1.14 @@ -172,29 +172,29 @@
    1.15  lemma hyperpow_inverse:
    1.16       "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
    1.17  apply (simp (no_asm) add: hypreal_zero_def)
    1.18 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.19 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.20 +apply (rule eq_Abs_hypnat [of n])
    1.21 +apply (rule eq_Abs_hypreal [of r])
    1.22  apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
    1.23  apply (rule FreeUltrafilterNat_subset)
    1.24  apply (auto dest: realpow_not_zero intro: power_inverse)
    1.25  done
    1.26  
    1.27  lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
    1.28 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.29 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.30 +apply (rule eq_Abs_hypnat [of n])
    1.31 +apply (rule eq_Abs_hypreal [of r])
    1.32  apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
    1.33  done
    1.34  
    1.35  lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
    1.36 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.37 -apply (rule_tac z = m in eq_Abs_hypnat)
    1.38 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.39 +apply (rule eq_Abs_hypnat [of n])
    1.40 +apply (rule eq_Abs_hypnat [of m])
    1.41 +apply (rule eq_Abs_hypreal [of r])
    1.42  apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
    1.43  done
    1.44  
    1.45  lemma hyperpow_one: "r pow (1::hypnat) = r"
    1.46  apply (unfold hypnat_one_def)
    1.47 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.48 +apply (rule eq_Abs_hypreal [of r])
    1.49  apply (auto simp add: hyperpow)
    1.50  done
    1.51  declare hyperpow_one [simp]
    1.52 @@ -202,38 +202,38 @@
    1.53  lemma hyperpow_two:
    1.54       "r pow ((1::hypnat) + (1::hypnat)) = r * r"
    1.55  apply (unfold hypnat_one_def)
    1.56 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.57 +apply (rule eq_Abs_hypreal [of r])
    1.58  apply (auto simp add: hyperpow hypnat_add hypreal_mult)
    1.59  done
    1.60  
    1.61  lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
    1.62  apply (simp add: hypreal_zero_def)
    1.63 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.64 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.65 +apply (rule eq_Abs_hypnat [of n])
    1.66 +apply (rule eq_Abs_hypreal [of r])
    1.67  apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
    1.68                     simp add: hyperpow hypreal_less hypreal_le)
    1.69  done
    1.70  
    1.71  lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
    1.72  apply (simp add: hypreal_zero_def)
    1.73 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.74 -apply (rule_tac z = r in eq_Abs_hypreal)
    1.75 +apply (rule eq_Abs_hypnat [of n])
    1.76 +apply (rule eq_Abs_hypreal [of r])
    1.77  apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
    1.78              simp add: hyperpow hypreal_le)
    1.79  done
    1.80  
    1.81  lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
    1.82  apply (simp add: hypreal_zero_def)
    1.83 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.84 -apply (rule_tac z = x in eq_Abs_hypreal)
    1.85 -apply (rule_tac z = y in eq_Abs_hypreal)
    1.86 +apply (rule eq_Abs_hypnat [of n])
    1.87 +apply (rule eq_Abs_hypreal [of x])
    1.88 +apply (rule eq_Abs_hypreal [of y])
    1.89  apply (auto simp add: hyperpow hypreal_le hypreal_less)
    1.90  apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
    1.91  apply (auto intro: power_mono)
    1.92  done
    1.93  
    1.94  lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
    1.95 -apply (rule_tac z = n in eq_Abs_hypnat)
    1.96 +apply (rule eq_Abs_hypnat [of n])
    1.97  apply (auto simp add: hypreal_one_def hyperpow)
    1.98  done
    1.99  declare hyperpow_eq_one [simp]
   1.100 @@ -241,15 +241,15 @@
   1.101  lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
   1.102  apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
   1.103  apply simp
   1.104 -apply (rule_tac z = n in eq_Abs_hypnat)
   1.105 +apply (rule eq_Abs_hypnat [of n])
   1.106  apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
   1.107  done
   1.108  declare hrabs_hyperpow_minus_one [simp]
   1.109  
   1.110  lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
   1.111 -apply (rule_tac z = n in eq_Abs_hypnat)
   1.112 -apply (rule_tac z = r in eq_Abs_hypreal)
   1.113 -apply (rule_tac z = s in eq_Abs_hypreal)
   1.114 +apply (rule eq_Abs_hypnat [of n])
   1.115 +apply (rule eq_Abs_hypreal [of r])
   1.116 +apply (rule eq_Abs_hypreal [of s])
   1.117  apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
   1.118  done
   1.119  
   1.120 @@ -297,9 +297,9 @@
   1.121  
   1.122  lemma hyperpow_less_le:
   1.123       "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
   1.124 -apply (rule_tac z = n in eq_Abs_hypnat)
   1.125 -apply (rule_tac z = N in eq_Abs_hypnat)
   1.126 -apply (rule_tac z = r in eq_Abs_hypreal)
   1.127 +apply (rule eq_Abs_hypnat [of n])
   1.128 +apply (rule eq_Abs_hypnat [of N])
   1.129 +apply (rule eq_Abs_hypreal [of r])
   1.130  apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   1.131              hypreal_zero_def hypreal_one_def)
   1.132  apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
   1.133 @@ -314,8 +314,7 @@
   1.134  
   1.135  lemma hyperpow_realpow:
   1.136        "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   1.137 -apply (unfold hypreal_of_real_def hypnat_of_nat_def)
   1.138 -apply (auto simp add: hyperpow)
   1.139 +apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
   1.140  done
   1.141  
   1.142  lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   1.143 @@ -355,9 +354,8 @@
   1.144  
   1.145  lemma hrealpow_hyperpow_Infinitesimal_iff:
   1.146       "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
   1.147 -apply (unfold hypnat_of_nat_def)
   1.148 -apply (rule_tac z = x in eq_Abs_hypreal)
   1.149 -apply (auto simp add: hrealpow hyperpow)
   1.150 +apply (rule eq_Abs_hypreal [of x])
   1.151 +apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
   1.152  done
   1.153  
   1.154  lemma Infinitesimal_hrealpow: