Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Hyperreal/HyperPow.thy
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14387 e96d5c42c4b0
equal deleted inserted replaced
14377:f454b3004f8f 14378:69c4d5997669 
   161 declare hyperpow_zero [simp]
 
   161 declare hyperpow_zero [simp]
 
   162 
   162 
   163 lemma hyperpow_not_zero [rule_format (no_asm)]:
 
   163 lemma hyperpow_not_zero [rule_format (no_asm)]:
 
   164      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
 
   164      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
 
   165 apply (simp (no_asm) add: hypreal_zero_def)
 
   165 apply (simp (no_asm) add: hypreal_zero_def)
 
   166 apply (rule_tac z = n in eq_Abs_hypnat)
 
   166 apply (rule eq_Abs_hypnat [of n])
 
   167 apply (rule_tac z = r in eq_Abs_hypreal)
 
   167 apply (rule eq_Abs_hypreal [of r])
 
   168 apply (auto simp add: hyperpow)
 
   168 apply (auto simp add: hyperpow)
 
   169 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 
   169 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 
   170 done
 
   170 done
 
   171 
   171 
   172 lemma hyperpow_inverse:
 
   172 lemma hyperpow_inverse:
 
   173      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
 
   173      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
 
   174 apply (simp (no_asm) add: hypreal_zero_def)
 
   174 apply (simp (no_asm) add: hypreal_zero_def)
 
   175 apply (rule_tac z = n in eq_Abs_hypnat)
 
   175 apply (rule eq_Abs_hypnat [of n])
 
   176 apply (rule_tac z = r in eq_Abs_hypreal)
 
   176 apply (rule eq_Abs_hypreal [of r])
 
   177 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 
   177 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 
   178 apply (rule FreeUltrafilterNat_subset)
 
   178 apply (rule FreeUltrafilterNat_subset)
 
   179 apply (auto dest: realpow_not_zero intro: power_inverse)
 
   179 apply (auto dest: realpow_not_zero intro: power_inverse)
 
   180 done
 
   180 done
 
   181 
   181 
   182 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
 
   182 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
 
   183 apply (rule_tac z = n in eq_Abs_hypnat)
 
   183 apply (rule eq_Abs_hypnat [of n])
 
   184 apply (rule_tac z = r in eq_Abs_hypreal)
 
   184 apply (rule eq_Abs_hypreal [of r])
 
   185 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 
   185 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 
   186 done
 
   186 done
 
   187 
   187 
   188 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
 
   188 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
 
   189 apply (rule_tac z = n in eq_Abs_hypnat)
 
   189 apply (rule eq_Abs_hypnat [of n])
 
   190 apply (rule_tac z = m in eq_Abs_hypnat)
 
   190 apply (rule eq_Abs_hypnat [of m])
 
   191 apply (rule_tac z = r in eq_Abs_hypreal)
 
   191 apply (rule eq_Abs_hypreal [of r])
 
   192 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 
   192 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 
   193 done
 
   193 done
 
   194 
   194 
   195 lemma hyperpow_one: "r pow (1::hypnat) = r"
 
   195 lemma hyperpow_one: "r pow (1::hypnat) = r"
 
   196 apply (unfold hypnat_one_def)
 
   196 apply (unfold hypnat_one_def)
 
   197 apply (rule_tac z = r in eq_Abs_hypreal)
 
   197 apply (rule eq_Abs_hypreal [of r])
 
   198 apply (auto simp add: hyperpow)
 
   198 apply (auto simp add: hyperpow)
 
   199 done
 
   199 done
 
   200 declare hyperpow_one [simp]
 
   200 declare hyperpow_one [simp]
 
   201 
   201 
   202 lemma hyperpow_two:
 
   202 lemma hyperpow_two:
 
   203      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
 
   203      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
 
   204 apply (unfold hypnat_one_def)
 
   204 apply (unfold hypnat_one_def)
 
   205 apply (rule_tac z = r in eq_Abs_hypreal)
 
   205 apply (rule eq_Abs_hypreal [of r])
 
   206 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 
   206 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 
   207 done
 
   207 done
 
   208 
   208 
   209 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
 
   209 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
 
   210 apply (simp add: hypreal_zero_def)
 
   210 apply (simp add: hypreal_zero_def)
 
   211 apply (rule_tac z = n in eq_Abs_hypnat)
 
   211 apply (rule eq_Abs_hypnat [of n])
 
   212 apply (rule_tac z = r in eq_Abs_hypreal)
 
   212 apply (rule eq_Abs_hypreal [of r])
 
   213 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
 
   213 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
 
   214                    simp add: hyperpow hypreal_less hypreal_le)
 
   214                    simp add: hyperpow hypreal_less hypreal_le)
 
   215 done
 
   215 done
 
   216 
   216 
   217 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
 
   217 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
 
   218 apply (simp add: hypreal_zero_def)
 
   218 apply (simp add: hypreal_zero_def)
 
   219 apply (rule_tac z = n in eq_Abs_hypnat)
 
   219 apply (rule eq_Abs_hypnat [of n])
 
   220 apply (rule_tac z = r in eq_Abs_hypreal)
 
   220 apply (rule eq_Abs_hypreal [of r])
 
   221 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
   221 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
   222             simp add: hyperpow hypreal_le)
 
   222             simp add: hyperpow hypreal_le)
 
   223 done
 
   223 done
 
   224 
   224 
   225 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
 
   225 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
 
   226 apply (simp add: hypreal_zero_def)
 
   226 apply (simp add: hypreal_zero_def)
 
   227 apply (rule_tac z = n in eq_Abs_hypnat)
 
   227 apply (rule eq_Abs_hypnat [of n])
 
   228 apply (rule_tac z = x in eq_Abs_hypreal)
 
   228 apply (rule eq_Abs_hypreal [of x])
 
   229 apply (rule_tac z = y in eq_Abs_hypreal)
 
   229 apply (rule eq_Abs_hypreal [of y])
 
   230 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 
   230 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 
   231 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 
   231 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 
   232 apply (auto intro: power_mono)
 
   232 apply (auto intro: power_mono)
 
   233 done
 
   233 done
 
   234 
   234 
   235 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
 
   235 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
 
   236 apply (rule_tac z = n in eq_Abs_hypnat)
 
   236 apply (rule eq_Abs_hypnat [of n])
 
   237 apply (auto simp add: hypreal_one_def hyperpow)
 
   237 apply (auto simp add: hypreal_one_def hyperpow)
 
   238 done
 
   238 done
 
   239 declare hyperpow_eq_one [simp]
 
   239 declare hyperpow_eq_one [simp]
 
   240 
   240 
   241 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
 
   241 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
 
   242 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 
   242 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 
   243 apply simp
 
   243 apply simp
 
   244 apply (rule_tac z = n in eq_Abs_hypnat)
 
   244 apply (rule eq_Abs_hypnat [of n])
 
   245 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 
   245 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 
   246 done
 
   246 done
 
   247 declare hrabs_hyperpow_minus_one [simp]
 
   247 declare hrabs_hyperpow_minus_one [simp]
 
   248 
   248 
   249 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
 
   249 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
 
   250 apply (rule_tac z = n in eq_Abs_hypnat)
 
   250 apply (rule eq_Abs_hypnat [of n])
 
   251 apply (rule_tac z = r in eq_Abs_hypreal)
 
   251 apply (rule eq_Abs_hypreal [of r])
 
   252 apply (rule_tac z = s in eq_Abs_hypreal)
 
   252 apply (rule eq_Abs_hypreal [of s])
 
   253 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 
   253 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 
   254 done
 
   254 done
 
   255 
   255 
   256 lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
 
   256 lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
 
   257 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
   257 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
   295 done
 
   295 done
 
   296 declare hyperpow_minus_one2 [simp]
 
   296 declare hyperpow_minus_one2 [simp]
 
   297 
   297 
   298 lemma hyperpow_less_le:
 
   298 lemma hyperpow_less_le:
 
   299      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
 
   299      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
 
   300 apply (rule_tac z = n in eq_Abs_hypnat)
 
   300 apply (rule eq_Abs_hypnat [of n])
 
   301 apply (rule_tac z = N in eq_Abs_hypnat)
 
   301 apply (rule eq_Abs_hypnat [of N])
 
   302 apply (rule_tac z = r in eq_Abs_hypreal)
 
   302 apply (rule eq_Abs_hypreal [of r])
 
   303 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   303 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   304             hypreal_zero_def hypreal_one_def)
 
   304             hypreal_zero_def hypreal_one_def)
 
   305 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
 
   305 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
 
   306 apply (erule FreeUltrafilterNat_Int, assumption)
 
   306 apply (erule FreeUltrafilterNat_Int, assumption)
 
   307 apply (auto intro: power_decreasing)
 
   307 apply (auto intro: power_decreasing)
 
   312       ==> ALL n: Nats. r pow N \<le> r pow n"
 
   312       ==> ALL n: Nats. r pow N \<le> r pow n"
 
   313 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
 
   313 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
 
   314 
   314 
   315 lemma hyperpow_realpow:
 
   315 lemma hyperpow_realpow:
 
   316       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
 
   316       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
 
   317 apply (unfold hypreal_of_real_def hypnat_of_nat_def)
 
   317 apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
 
   318 apply (auto simp add: hyperpow)
 
       
   319 done
 
   318 done
 
   320 
   319 
   321 lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
 
   320 lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
 
   322 apply (unfold SReal_def)
 
   321 apply (unfold SReal_def)
 
   323 apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
 
   322 apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
 
   353 apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
 
   352 apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
 
   354 done
 
   353 done
 
   355 
   354 
   356 lemma hrealpow_hyperpow_Infinitesimal_iff:
 
   355 lemma hrealpow_hyperpow_Infinitesimal_iff:
 
   357      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
 
   356      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
 
   358 apply (unfold hypnat_of_nat_def)
 
   357 apply (rule eq_Abs_hypreal [of x])
 
   359 apply (rule_tac z = x in eq_Abs_hypreal)
 
   358 apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
 
   360 apply (auto simp add: hrealpow hyperpow)
 
       
   361 done
 
   359 done
 
   362 
   360 
   363 lemma Infinitesimal_hrealpow:
 
   361 lemma Infinitesimal_hrealpow:
 
   364      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
 
   362      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
 
   365 by (force intro!: Infinitesimal_hyperpow
 
   363 by (force intro!: Infinitesimal_hyperpow
wneuper/isa