src/HOL/Hyperreal/HyperPow.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15085 5693a977a767
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     1 (*  Title       : HyperPow.thy
     2     Author      : Jacques D. Fleuriot  
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     5 *)
     6 
     7 header{*Exponentials on the Hyperreals*}
     8 
     9 theory HyperPow
    10 import HyperArith HyperNat "../Real/RealPow"
    11 begin
    12 
    13 instance hypreal :: power ..
    14 
    15 consts hpowr :: "[hypreal,nat] => hypreal"  
    16 primrec
    17    hpowr_0:   "r ^ 0       = (1::hypreal)"
    18    hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
    19 
    20 
    21 instance hypreal :: recpower
    22 proof
    23   fix z :: hypreal
    24   fix n :: nat
    25   show "z^0 = 1" by simp
    26   show "z^(Suc n) = z * (z^n)" by simp
    27 qed
    28 
    29 
    30 consts
    31   "pow"  :: "[hypreal,hypnat] => hypreal"     (infixr 80)
    32 
    33 defs
    34 
    35   (* hypernatural powers of hyperreals *)
    36   hyperpow_def:
    37   "(R::hypreal) pow (N::hypnat) ==
    38       Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N).
    39                         hyprel``{%n::nat. (X n) ^ (Y n)})"
    40 
    41 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
    42 by simp
    43 
    44 lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
    45 by (auto simp add: zero_le_mult_iff)
    46 
    47 lemma hrealpow_two_le_add_order [simp]:
    48      "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
    49 by (simp only: hrealpow_two_le hypreal_le_add_order)
    50 
    51 lemma hrealpow_two_le_add_order2 [simp]:
    52      "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
    53 by (simp only: hrealpow_two_le hypreal_le_add_order)
    54 
    55 lemma hypreal_add_nonneg_eq_0_iff:
    56      "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
    57 by arith
    58 
    59 
    60 text{*FIXME: DELETE THESE*}
    61 lemma hypreal_three_squares_add_zero_iff:
    62      "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
    63 apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff, auto)
    64 done
    65 
    66 lemma hrealpow_three_squares_add_zero_iff [simp]:
    67      "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
    68       (x = 0 & y = 0 & z = 0)"
    69 by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
    70 
    71 
    72 lemma hrabs_hrealpow_two [simp]:
    73      "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
    74 by (simp add: abs_mult)
    75 
    76 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
    77 by (insert power_increasing [of 0 n "2::hypreal"], simp)
    78 
    79 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
    80 apply (induct_tac "n")
    81 apply (auto simp add: hypreal_of_nat_Suc left_distrib)
    82 apply (cut_tac n = n in two_hrealpow_ge_one, arith)
    83 done
    84 
    85 lemma hrealpow:
    86     "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
    87 apply (induct_tac "m")
    88 apply (auto simp add: hypreal_one_def hypreal_mult)
    89 done
    90 
    91 lemma hrealpow_sum_square_expand:
    92      "(x + (y::hypreal)) ^ Suc (Suc 0) =
    93       x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
    94 by (simp add: right_distrib left_distrib hypreal_of_nat_Suc)
    95 
    96 
    97 subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
    98 
    99 lemma hypreal_of_real_power [simp]:
   100      "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
   101 by (induct_tac "n", simp_all add: nat_mult_distrib)
   102 
   103 lemma power_hypreal_of_real_number_of:
   104      "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
   105 by (simp only: hypreal_number_of [symmetric] hypreal_of_real_power)
   106 
   107 declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
   108 
   109 lemma hrealpow_HFinite: "x \<in> HFinite ==> x ^ n \<in> HFinite"
   110 apply (induct_tac "n")
   111 apply (auto intro: HFinite_mult)
   112 done
   113 
   114 
   115 subsection{*Powers with Hypernatural Exponents*}
   116 
   117 lemma hyperpow_congruent:
   118      "congruent hyprel
   119      (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
   120 apply (unfold congruent_def)
   121 apply (auto intro!: ext, fuf+)
   122 done
   123 
   124 lemma hyperpow:
   125   "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
   126    Abs_hypreal(hyprel``{%n. X n ^ Y n})"
   127 apply (unfold hyperpow_def)
   128 apply (rule_tac f = Abs_hypreal in arg_cong)
   129 apply (auto intro!: lemma_hyprel_refl bexI 
   130            simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
   131                      hyperpow_congruent, fuf)
   132 done
   133 
   134 lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
   135 apply (unfold hypnat_one_def)
   136 apply (simp (no_asm) add: hypreal_zero_def)
   137 apply (rule_tac z = n in eq_Abs_hypnat)
   138 apply (auto simp add: hyperpow hypnat_add)
   139 done
   140 declare hyperpow_zero [simp]
   141 
   142 lemma hyperpow_not_zero [rule_format (no_asm)]:
   143      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
   144 apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
   145 apply (auto simp add: hyperpow)
   146 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
   147 done
   148 
   149 lemma hyperpow_inverse:
   150      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
   151 apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
   152 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
   153 apply (rule FreeUltrafilterNat_subset)
   154 apply (auto dest: realpow_not_zero intro: power_inverse)
   155 done
   156 
   157 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
   158 apply (cases n, cases r)
   159 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
   160 done
   161 
   162 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
   163 apply (cases n, cases m, cases r)
   164 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
   165 done
   166 
   167 lemma hyperpow_one [simp]: "r pow (1::hypnat) = r"
   168 apply (unfold hypnat_one_def, cases r)
   169 apply (auto simp add: hyperpow)
   170 done
   171 
   172 lemma hyperpow_two:
   173      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
   174 apply (unfold hypnat_one_def, cases r)
   175 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
   176 done
   177 
   178 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
   179 apply (simp add: hypreal_zero_def, cases n, cases r)
   180 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
   181                    simp add: hyperpow hypreal_less hypreal_le)
   182 done
   183 
   184 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
   185 apply (simp add: hypreal_zero_def, cases n, cases r)
   186 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
   187             simp add: hyperpow hypreal_le)
   188 done
   189 
   190 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
   191 apply (simp add: hypreal_zero_def, cases n, cases x, cases y)
   192 apply (auto simp add: hyperpow hypreal_le hypreal_less)
   193 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
   194 apply (auto intro: power_mono)
   195 done
   196 
   197 lemma hyperpow_eq_one [simp]: "1 pow n = (1::hypreal)"
   198 apply (cases n)
   199 apply (auto simp add: hypreal_one_def hyperpow)
   200 done
   201 
   202 lemma hrabs_hyperpow_minus_one [simp]: "abs(-1 pow n) = (1::hypreal)"
   203 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
   204 apply simp
   205 apply (cases n)
   206 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
   207 done
   208 
   209 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
   210 apply (cases n, cases r, cases s)
   211 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
   212 done
   213 
   214 lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
   215 by (auto simp add: hyperpow_two zero_le_mult_iff)
   216 
   217 lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
   218 by (simp add: abs_if hyperpow_two_le linorder_not_less)
   219 
   220 lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1)  = x pow (1 + 1)"
   221 by (simp add: hyperpow_hrabs)
   222 
   223 lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)"
   224 apply (auto simp add: hyperpow_two)
   225 apply (rule_tac y = "1*1" in order_le_less_trans)
   226 apply (rule_tac [2] hypreal_mult_less_mono, auto)
   227 done
   228 
   229 lemma hyperpow_two_ge_one:
   230      "1 \<le> r ==> 1 \<le> r pow (1 + 1)"
   231 by (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
   232 
   233 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
   234 apply (rule_tac y = "1 pow n" in order_trans)
   235 apply (rule_tac [2] hyperpow_le, auto)
   236 done
   237 
   238 lemma hyperpow_minus_one2 [simp]:
   239      "-1 pow ((1 + 1)*n) = (1::hypreal)"
   240 apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
   241 apply simp
   242 apply (simp only: hypreal_one_def, cases n)
   243 apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
   244                       left_distrib)
   245 done
   246 
   247 lemma hyperpow_less_le:
   248      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
   249 apply (cases n, cases N, cases r)
   250 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   251             hypreal_zero_def hypreal_one_def)
   252 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
   253 apply (erule FreeUltrafilterNat_Int, assumption)
   254 apply (auto intro: power_decreasing)
   255 done
   256 
   257 lemma hyperpow_SHNat_le:
   258      "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
   259       ==> ALL n: Nats. r pow N \<le> r pow n"
   260 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
   261 
   262 lemma hyperpow_realpow:
   263       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   264 by (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
   265 
   266 lemma hyperpow_SReal [simp]:
   267      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   268 by (simp del: hypreal_of_real_power add: hyperpow_realpow SReal_def)
   269 
   270 
   271 lemma hyperpow_zero_HNatInfinite [simp]:
   272      "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
   273 by (drule HNatInfinite_is_Suc, auto)
   274 
   275 lemma hyperpow_le_le:
   276      "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
   277 apply (drule order_le_less [of n, THEN iffD1])
   278 apply (auto intro: hyperpow_less_le)
   279 done
   280 
   281 lemma hyperpow_Suc_le_self2:
   282      "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
   283 apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
   284 apply auto
   285 done
   286 
   287 lemma lemma_Infinitesimal_hyperpow:
   288      "[| x \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
   289 apply (unfold Infinitesimal_def)
   290 apply (auto intro!: hyperpow_Suc_le_self2 
   291           simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
   292 done
   293 
   294 lemma Infinitesimal_hyperpow:
   295      "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
   296 apply (rule hrabs_le_Infinitesimal)
   297 apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
   298 done
   299 
   300 lemma hrealpow_hyperpow_Infinitesimal_iff:
   301      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
   302 apply (cases x)
   303 apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
   304 done
   305 
   306 lemma Infinitesimal_hrealpow:
   307      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
   308 by (force intro!: Infinitesimal_hyperpow
   309           simp add: hrealpow_hyperpow_Infinitesimal_iff 
   310                     hypnat_of_nat_less_iff [symmetric] hypnat_of_nat_zero
   311           simp del: hypnat_of_nat_less_iff)
   312 
   313 ML
   314 {*
   315 val hrealpow_two = thm "hrealpow_two";
   316 val hrealpow_two_le = thm "hrealpow_two_le";
   317 val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
   318 val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
   319 val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff";
   320 val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff";
   321 val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff";
   322 val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
   323 val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
   324 val two_hrealpow_gt = thm "two_hrealpow_gt";
   325 val hrealpow = thm "hrealpow";
   326 val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
   327 val hypreal_of_real_power = thm "hypreal_of_real_power";
   328 val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
   329 val hrealpow_HFinite = thm "hrealpow_HFinite";
   330 val hyperpow_congruent = thm "hyperpow_congruent";
   331 val hyperpow = thm "hyperpow";
   332 val hyperpow_zero = thm "hyperpow_zero";
   333 val hyperpow_not_zero = thm "hyperpow_not_zero";
   334 val hyperpow_inverse = thm "hyperpow_inverse";
   335 val hyperpow_hrabs = thm "hyperpow_hrabs";
   336 val hyperpow_add = thm "hyperpow_add";
   337 val hyperpow_one = thm "hyperpow_one";
   338 val hyperpow_two = thm "hyperpow_two";
   339 val hyperpow_gt_zero = thm "hyperpow_gt_zero";
   340 val hyperpow_ge_zero = thm "hyperpow_ge_zero";
   341 val hyperpow_le = thm "hyperpow_le";
   342 val hyperpow_eq_one = thm "hyperpow_eq_one";
   343 val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one";
   344 val hyperpow_mult = thm "hyperpow_mult";
   345 val hyperpow_two_le = thm "hyperpow_two_le";
   346 val hrabs_hyperpow_two = thm "hrabs_hyperpow_two";
   347 val hyperpow_two_hrabs = thm "hyperpow_two_hrabs";
   348 val hyperpow_two_gt_one = thm "hyperpow_two_gt_one";
   349 val hyperpow_two_ge_one = thm "hyperpow_two_ge_one";
   350 val two_hyperpow_ge_one = thm "two_hyperpow_ge_one";
   351 val hyperpow_minus_one2 = thm "hyperpow_minus_one2";
   352 val hyperpow_less_le = thm "hyperpow_less_le";
   353 val hyperpow_SHNat_le = thm "hyperpow_SHNat_le";
   354 val hyperpow_realpow = thm "hyperpow_realpow";
   355 val hyperpow_SReal = thm "hyperpow_SReal";
   356 val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite";
   357 val hyperpow_le_le = thm "hyperpow_le_le";
   358 val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2";
   359 val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow";
   360 val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow";
   361 val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff";
   362 val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow";
   363 *}
   364 
   365 end