src/HOL/Hyperreal/HyperPow.thy
author huffman
Thu, 14 Dec 2006 19:15:16 +0100
changeset 21848 b35faf14a89f
parent 21404 eb85850d3eb7
child 21851 030f46b8c4b5
permissions -rw-r--r--
generalized type of hyperpow; removed hcpow
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : HyperPow.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
     7
header{*Exponentials on the Hyperreals*}
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15085
diff changeset
     9
theory HyperPow
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20730
diff changeset
    10
imports HyperArith HyperNat Parity
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15085
diff changeset
    11
begin
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
    12
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    13
(* consts hpowr :: "[hypreal,nat] => hypreal" *)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    14
17298
ad73fb6144cf replace type hypreal with real star
huffman
parents: 16924
diff changeset
    15
lemma hpowr_0 [simp]:   "r ^ 0       = (1::hypreal)"
ad73fb6144cf replace type hypreal with real star
huffman
parents: 16924
diff changeset
    16
by (rule power_0)
ad73fb6144cf replace type hypreal with real star
huffman
parents: 16924
diff changeset
    17
ad73fb6144cf replace type hypreal with real star
huffman
parents: 16924
diff changeset
    18
lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
ad73fb6144cf replace type hypreal with real star
huffman
parents: 16924
diff changeset
    19
by (rule power_Suc)
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    20
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17429
diff changeset
    21
definition
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
  (* hypernatural powers of hyperreals *)
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
    23
  pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
17332
4910cf8c0cd2 added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
huffman
parents: 17318
diff changeset
    24
  hyperpow_def [transfer_unfold]:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
    25
  "R pow N = ( *f2* op ^) R N"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    26
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    27
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
14443
75910c7557c5 generic theorems about exponentials; general tidying up
paulson
parents: 14435
diff changeset
    28
by simp
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    29
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
    30
lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
    31
by (auto simp add: zero_le_mult_iff)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    32
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
    33
lemma hrealpow_two_le_add_order [simp]:
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    34
     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    35
by (simp only: hrealpow_two_le add_nonneg_nonneg)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    36
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
    37
lemma hrealpow_two_le_add_order2 [simp]:
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    38
     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    39
by (simp only: hrealpow_two_le add_nonneg_nonneg)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    40
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    41
lemma hypreal_add_nonneg_eq_0_iff:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    42
     "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
    43
by arith
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
    44
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    45
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    46
text{*FIXME: DELETE THESE*}
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    47
lemma hypreal_three_squares_add_zero_iff:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    48
     "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    49
apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    50
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    51
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    52
lemma hrealpow_three_squares_add_zero_iff [simp]:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    53
     "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    54
      (x = 0 & y = 0 & z = 0)"
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    55
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    56
16924
04246269386e removed the dependence on abs_mult
paulson
parents: 15539
diff changeset
    57
(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
04246269386e removed the dependence on abs_mult
paulson
parents: 15539
diff changeset
    58
  result proved in Ring_and_Field*)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    59
lemma hrabs_hrealpow_two [simp]:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    60
     "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
16924
04246269386e removed the dependence on abs_mult
paulson
parents: 15539
diff changeset
    61
by (simp add: abs_mult)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    62
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    63
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    64
by (insert power_increasing [of 0 n "2::hypreal"], simp)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    65
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
    66
lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    67
apply (induct_tac "n")
20730
da903f59e9ba hypreal_of_nat abbreviates of_nat
huffman
parents: 20541
diff changeset
    68
apply (auto simp add: left_distrib)
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
    69
apply (cut_tac n = n in two_hrealpow_ge_one, arith)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    70
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    71
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    72
lemma hrealpow:
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    73
    "star_n X ^ m = star_n (%n. (X n::real) ^ m)"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    74
apply (induct_tac "m")
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    75
apply (auto simp add: star_n_one_num star_n_mult power_0)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    76
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    77
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    78
lemma hrealpow_sum_square_expand:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    79
     "(x + (y::hypreal)) ^ Suc (Suc 0) =
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    80
      x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
20730
da903f59e9ba hypreal_of_nat abbreviates of_nat
huffman
parents: 20541
diff changeset
    81
by (simp add: right_distrib left_distrib)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    82
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    83
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    84
subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    85
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    86
lemma power_hypreal_of_real_number_of:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    87
     "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
    88
by simp
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    89
declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    90
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 19765
diff changeset
    91
lemma hrealpow_HFinite:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 19765
diff changeset
    92
  fixes x :: "'a::{real_normed_algebra,recpower} star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 19765
diff changeset
    93
  shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    94
apply (induct_tac "n")
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 19765
diff changeset
    95
apply (auto simp add: power_Suc intro: HFinite_mult)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    96
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    97
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    98
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
    99
subsection{*Powers with Hypernatural Exponents*}
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   100
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   101
lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
17429
e8d6ed3aacfe merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents: 17332
diff changeset
   102
by (simp add: hyperpow_def starfun2_star_n)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   103
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   104
lemma hyperpow_zero [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   105
  "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   106
by transfer simp
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   107
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   108
lemma hyperpow_not_zero:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   109
  "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   110
by transfer (rule field_power_not_zero)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   111
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   112
lemma hyperpow_inverse:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   113
  "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   114
   \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   115
by transfer (rule power_inverse)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   116
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   117
lemma hyperpow_hrabs:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   118
  "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   119
by transfer (rule power_abs [symmetric])
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   120
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   121
lemma hyperpow_add:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   122
  "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   123
by transfer (rule power_add)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   124
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   125
lemma hyperpow_one [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   126
  "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   127
by transfer (rule power_one_right)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   128
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   129
lemma hyperpow_two:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   130
  "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   131
by transfer (simp add: power_Suc)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   132
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   133
lemma hyperpow_gt_zero:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   134
  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   135
by transfer (rule zero_less_power)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   136
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   137
lemma hyperpow_ge_zero:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   138
  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   139
by transfer (rule zero_le_power)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   140
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   141
lemma hyperpow_le:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   142
  "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   143
   \<Longrightarrow> x pow n \<le> y pow n"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   144
by transfer (rule power_mono [OF _ order_less_imp_le])
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   145
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   146
lemma hyperpow_eq_one [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   147
  "\<And>n. 1 pow n = (1::'a::recpower star)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   148
by transfer (rule power_one)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   149
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   150
lemma hrabs_hyperpow_minus_one [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   151
  "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   152
by transfer (rule abs_power_minus_one)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   153
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   154
lemma hyperpow_mult:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   155
  "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   156
   = (r pow n) * (s pow n)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   157
by transfer (rule power_mult_distrib)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   158
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   159
lemma hyperpow_two_le [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   160
  "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
   161
by (auto simp add: hyperpow_two zero_le_mult_iff)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   162
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   163
lemma hrabs_hyperpow_two [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   164
  "abs(x pow (1 + 1)) =
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   165
   (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   166
by (simp only: abs_of_nonneg hyperpow_two_le)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   167
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   168
lemma hyperpow_two_hrabs [simp]:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   169
  "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   170
by (simp add: hyperpow_hrabs)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   171
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15169
diff changeset
   172
text{*The precondition could be weakened to @{term "0\<le>x"}*}
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15169
diff changeset
   173
lemma hypreal_mult_less_mono:
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15169
diff changeset
   174
     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15169
diff changeset
   175
 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15169
diff changeset
   176
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   177
lemma hyperpow_two_gt_one:
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   178
  "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   179
by transfer (simp add: power_gt1)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   180
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   181
lemma hyperpow_two_ge_one:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   182
  "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   183
by transfer (simp add: one_le_power)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   184
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   185
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   186
apply (rule_tac y = "1 pow n" in order_trans)
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
   187
apply (rule_tac [2] hyperpow_le, auto)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   188
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   189
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   190
lemma hyperpow_minus_one2 [simp]:
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   191
     "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   192
by transfer (simp)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   193
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   194
lemma hyperpow_less_le:
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   195
     "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   196
by transfer (rule power_decreasing [OF order_less_imp_le])
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   197
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   198
lemma hyperpow_SHNat_le:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   199
     "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   200
      ==> ALL n: Nats. r pow N \<le> r pow n"
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   201
by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   202
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   203
lemma hyperpow_realpow:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   204
      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   205
by (simp add: star_of_def hypnat_of_nat_eq hyperpow)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   206
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   207
lemma hyperpow_SReal [simp]:
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   208
     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   209
by (simp del: star_of_power add: hyperpow_realpow SReal_def)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   210
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   211
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   212
lemma hyperpow_zero_HNatInfinite [simp]:
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14468
diff changeset
   213
     "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
   214
by (drule HNatInfinite_is_Suc, auto)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   215
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   216
lemma hyperpow_le_le:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   217
     "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
   218
apply (drule order_le_less [of n, THEN iffD1])
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   219
apply (auto intro: hyperpow_less_le)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   220
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   221
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   222
lemma hyperpow_Suc_le_self2:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   223
     "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   224
apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   225
apply auto
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   226
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   227
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   228
lemma lemma_Infinitesimal_hyperpow:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   229
     "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   230
apply (unfold Infinitesimal_def)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   231
apply (auto intro!: hyperpow_Suc_le_self2 
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   232
          simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   233
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   234
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   235
lemma Infinitesimal_hyperpow:
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   236
     "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   237
apply (rule hrabs_le_Infinitesimal)
14371
c78c7da09519 Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents: 14348
diff changeset
   238
apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   239
done
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   240
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   241
lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   242
by transfer (rule refl)
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   243
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   244
lemma hrealpow_hyperpow_Infinitesimal_iff:
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   245
     "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
21848
b35faf14a89f generalized type of hyperpow; removed hcpow
huffman
parents: 21404
diff changeset
   246
by (simp only: hyperpow_hypnat_of_nat)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   247
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   248
lemma Infinitesimal_hrealpow:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 19765
diff changeset
   249
     "[| (x::hypreal) \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17299
diff changeset
   250
by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)
14348
744c868ee0b7 Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents: 11713
diff changeset
   251
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   252
end