author | paulson |
Fri, 09 Jan 2004 10:46:18 +0100 | |
changeset 14348 | 744c868ee0b7 |
parent 11713 | 883d559b0b8c |
child 14371 | c78c7da09519 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : HyperPow.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Powers theory for hyperreals |
|
5 |
*) |
|
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 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
9 |
theory HyperPow = HRealAbs + HyperNat + RealPow: |
10751 | 10 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
11 |
instance hypnat :: order |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
12 |
by (intro_classes, |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
13 |
(assumption | |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
14 |
rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+) |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
15 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
16 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
17 |
text{*Type @{typ hypnat} is linearly ordered*} |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
18 |
instance hypnat :: linorder |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
19 |
by (intro_classes, rule hypnat_le_linear) |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
20 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
21 |
instance hypnat :: plus_ac0 |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
22 |
by (intro_classes, |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
23 |
(assumption | |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
24 |
rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+) |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
25 |
|
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
26 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
27 |
instance hypreal :: power .. |
10751 | 28 |
|
29 |
consts hpowr :: "[hypreal,nat] => hypreal" |
|
30 |
primrec |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
31 |
hpowr_0: "r ^ 0 = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
32 |
hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
33 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
34 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
35 |
instance hypreal :: ringpower |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
36 |
proof |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
37 |
fix z :: hypreal |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
38 |
fix n :: nat |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
39 |
show "z^0 = 1" by simp |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
40 |
show "z^(Suc n) = z * (z^n)" by simp |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
41 |
qed |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
42 |
|
10751 | 43 |
|
44 |
consts |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
45 |
"pow" :: "[hypreal,hypnat] => hypreal" (infixr 80) |
10751 | 46 |
|
47 |
defs |
|
48 |
||
49 |
(* hypernatural powers of hyperreals *) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
50 |
hyperpow_def: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
51 |
"(R::hypreal) pow (N::hypnat) == |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
52 |
Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N). |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
53 |
hyprel``{%n::nat. (X n) ^ (Y n)})" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
54 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
55 |
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
56 |
apply (simp (no_asm)) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
57 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
58 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
59 |
lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
60 |
apply (simp add: power_abs); |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
61 |
done |
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 hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
64 |
apply (auto simp add: zero_le_mult_iff) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
65 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
66 |
declare hrealpow_two_le [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
67 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
68 |
lemma hrealpow_two_le_add_order: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
69 |
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
70 |
apply (simp only: hrealpow_two_le hypreal_le_add_order) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
71 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
72 |
declare hrealpow_two_le_add_order [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
73 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
74 |
lemma hrealpow_two_le_add_order2: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
75 |
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
76 |
apply (simp only: hrealpow_two_le hypreal_le_add_order) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
77 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
78 |
declare hrealpow_two_le_add_order2 [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
79 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
80 |
lemma hypreal_add_nonneg_eq_0_iff: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
81 |
"[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
82 |
apply arith |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
83 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
84 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
85 |
text{*FIXME: DELETE THESE*} |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
86 |
lemma hypreal_three_squares_add_zero_iff: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
87 |
"(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
88 |
apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
89 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
90 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
91 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
92 |
lemma hrealpow_three_squares_add_zero_iff [simp]: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
93 |
"(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
|
94 |
(x = 0 & y = 0 & z = 0)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
95 |
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
|
96 |
|
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 |
lemma hrabs_hrealpow_two [simp]: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
99 |
"abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
100 |
by (simp add: abs_mult) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
101 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
105 |
lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
106 |
apply (induct_tac "n") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
107 |
apply (auto simp add: hypreal_of_nat_Suc left_distrib) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
108 |
apply (cut_tac n = "n" in two_hrealpow_ge_one) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
109 |
apply arith |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
110 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
111 |
declare two_hrealpow_gt [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
112 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
113 |
lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
114 |
apply (induct_tac "n") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
115 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
116 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
117 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
118 |
lemma double_lemma: "n+n = (2*n::nat)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
119 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
120 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
121 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
122 |
(*ugh: need to get rid fo the n+n*) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
123 |
lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
124 |
apply (auto simp add: double_lemma hrealpow_minus_one) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
125 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
126 |
declare hrealpow_minus_one2 [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
127 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
128 |
lemma hrealpow: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
129 |
"Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
130 |
apply (induct_tac "m") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
131 |
apply (auto simp add: hypreal_one_def hypreal_mult) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
132 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
133 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
134 |
lemma hrealpow_sum_square_expand: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
135 |
"(x + (y::hypreal)) ^ Suc (Suc 0) = |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
136 |
x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
137 |
by (simp add: right_distrib left_distrib hypreal_of_nat_Suc) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
138 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
139 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
140 |
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
|
141 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
142 |
lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
143 |
apply (induct_tac "n") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
144 |
apply (simp_all add: nat_mult_distrib) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
145 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
146 |
declare hypreal_of_real_power [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
147 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
148 |
lemma power_hypreal_of_real_number_of: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
149 |
"(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
150 |
by (simp only: hypreal_number_of_def hypreal_of_real_power) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
151 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
152 |
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
|
153 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
154 |
lemma hrealpow_HFinite: "x \<in> HFinite ==> x ^ n \<in> HFinite" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
155 |
apply (induct_tac "n") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
156 |
apply (auto intro: HFinite_mult) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
157 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
158 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
159 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
160 |
subsection{*Powers with Hypernatural Exponents*} |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
161 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
162 |
lemma hyperpow_congruent: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
163 |
"congruent hyprel |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
164 |
(%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
165 |
apply (unfold congruent_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
166 |
apply (auto intro!: ext) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
167 |
apply fuf+ |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
168 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
169 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
170 |
lemma hyperpow: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
171 |
"Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
172 |
Abs_hypreal(hyprel``{%n. X n ^ Y n})" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
173 |
apply (unfold hyperpow_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
174 |
apply (rule_tac f = "Abs_hypreal" in arg_cong) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
175 |
apply (auto intro!: lemma_hyprel_refl bexI |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
176 |
simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
177 |
hyperpow_congruent) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
178 |
apply fuf |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
179 |
done |
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_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
182 |
apply (unfold hypnat_one_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
183 |
apply (simp (no_asm) add: hypreal_zero_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
184 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
185 |
apply (auto simp add: hyperpow hypnat_add) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
186 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
187 |
declare hyperpow_zero [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
188 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
189 |
lemma hyperpow_not_zero [rule_format (no_asm)]: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
190 |
"r \<noteq> (0::hypreal) --> r pow n \<noteq> 0" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
191 |
apply (simp (no_asm) add: hypreal_zero_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
192 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
193 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
194 |
apply (auto simp add: hyperpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
195 |
apply (drule FreeUltrafilterNat_Compl_mem) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
196 |
apply ultra |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
197 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
198 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
199 |
lemma hyperpow_inverse: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
200 |
"r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
201 |
apply (simp (no_asm) add: hypreal_zero_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
202 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
203 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
204 |
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
205 |
apply (rule FreeUltrafilterNat_subset) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
206 |
apply (auto dest: realpow_not_zero intro: power_inverse) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
207 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
208 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
209 |
lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
210 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
211 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
212 |
apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric]) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
213 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
214 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
215 |
lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
216 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
217 |
apply (rule_tac z = "m" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
218 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
219 |
apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add) |
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_one: "r pow (1::hypnat) = r" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
223 |
apply (unfold hypnat_one_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
224 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
225 |
apply (auto simp add: hyperpow) |
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 |
declare hyperpow_one [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
228 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
229 |
lemma hyperpow_two: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
230 |
"r pow ((1::hypnat) + (1::hypnat)) = r * r" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
231 |
apply (unfold hypnat_one_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
232 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
233 |
apply (auto simp add: hyperpow hypnat_add hypreal_mult) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
234 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
235 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
236 |
lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
237 |
apply (simp add: hypreal_zero_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
238 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
239 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
240 |
apply (auto elim!: FreeUltrafilterNat_subset zero_less_power |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
241 |
simp add: hyperpow hypreal_less hypreal_le) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
242 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
243 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
244 |
lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
245 |
apply (simp add: hypreal_zero_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
246 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
247 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
248 |
apply (auto elim!: FreeUltrafilterNat_subset zero_le_power |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
249 |
simp add: hyperpow hypreal_le) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
250 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
251 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
252 |
lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
253 |
apply (simp add: hypreal_zero_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
254 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
255 |
apply (rule_tac z = "x" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
256 |
apply (rule_tac z = "y" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
257 |
apply (auto simp add: hyperpow hypreal_le hypreal_less) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
258 |
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
259 |
apply (auto intro: power_mono) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
260 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
261 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
262 |
lemma hyperpow_eq_one: "1 pow n = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
263 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
264 |
apply (auto simp add: hypreal_one_def hyperpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
265 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
266 |
declare hyperpow_eq_one [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
267 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
268 |
lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
269 |
apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
270 |
apply simp |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
271 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
272 |
apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
273 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
274 |
declare hrabs_hyperpow_minus_one [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
275 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
276 |
lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
277 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
278 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
279 |
apply (rule_tac z = "s" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
280 |
apply (auto simp add: hyperpow hypreal_mult power_mult_distrib) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
281 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
282 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
283 |
lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
284 |
apply (auto simp add: hyperpow_two zero_le_mult_iff) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
285 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
286 |
declare hyperpow_two_le [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
287 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
288 |
lemma hrabs_hyperpow_two: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
289 |
"abs(x pow (1 + 1)) = x pow (1 + 1)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
290 |
apply (simp (no_asm) add: hrabs_eqI1) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
291 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
292 |
declare hrabs_hyperpow_two [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
293 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
294 |
lemma hyperpow_two_hrabs: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
295 |
"abs(x) pow (1 + 1) = x pow (1 + 1)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
296 |
apply (simp add: hyperpow_hrabs) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
297 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
298 |
declare hyperpow_two_hrabs [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
299 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
300 |
lemma hyperpow_two_gt_one: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
301 |
"(1::hypreal) < r ==> 1 < r pow (1 + 1)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
302 |
apply (auto simp add: hyperpow_two) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
303 |
apply (rule_tac y = "1*1" in order_le_less_trans) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
304 |
apply (rule_tac [2] hypreal_mult_less_mono) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
305 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
306 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
307 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
308 |
lemma hyperpow_two_ge_one: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
309 |
"(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
310 |
apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
311 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
312 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
313 |
lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
314 |
apply (rule_tac y = "1 pow n" in order_trans) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
315 |
apply (rule_tac [2] hyperpow_le) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
316 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
317 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
318 |
declare two_hyperpow_ge_one [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
319 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
320 |
lemma hyperpow_minus_one2: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
321 |
"-1 pow ((1 + 1)*n) = (1::hypreal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
322 |
apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ") |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
323 |
apply simp |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
324 |
apply (simp only: hypreal_one_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
325 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
326 |
apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
327 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
328 |
declare hyperpow_minus_one2 [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
329 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
330 |
lemma hyperpow_less_le: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
331 |
"[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
332 |
apply (rule_tac z = "n" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
333 |
apply (rule_tac z = "N" in eq_Abs_hypnat) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
334 |
apply (rule_tac z = "r" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
335 |
apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
336 |
hypreal_zero_def hypreal_one_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
337 |
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset]) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
338 |
apply (erule FreeUltrafilterNat_Int) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
339 |
apply assumption; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
340 |
apply (auto intro: power_decreasing) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
341 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
342 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
343 |
lemma hyperpow_SHNat_le: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
344 |
"[| 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
|
345 |
==> 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
|
346 |
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
|
347 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
348 |
lemma hyperpow_realpow: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
349 |
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
350 |
apply (unfold hypreal_of_real_def hypnat_of_nat_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
351 |
apply (auto simp add: hyperpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
352 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
353 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
354 |
lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
355 |
apply (unfold SReal_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
356 |
apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
357 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
358 |
declare hyperpow_SReal [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
359 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
360 |
lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
361 |
apply (drule HNatInfinite_is_Suc) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
362 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
363 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
364 |
declare hyperpow_zero_HNatInfinite [simp] |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
365 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
366 |
lemma hyperpow_le_le: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
367 |
"[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
368 |
apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
369 |
apply (auto intro: hyperpow_less_le) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
370 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
371 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
372 |
lemma hyperpow_Suc_le_self2: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
373 |
"[| (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
|
374 |
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
|
375 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
376 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
377 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
378 |
lemma lemma_Infinitesimal_hyperpow: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
379 |
"[| x \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
380 |
apply (unfold Infinitesimal_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
381 |
apply (auto intro!: hyperpow_Suc_le_self2 |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
382 |
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
|
383 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
384 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
385 |
lemma Infinitesimal_hyperpow: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
386 |
"[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
387 |
apply (rule hrabs_le_Infinitesimal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
388 |
apply (rule_tac [2] lemma_Infinitesimal_hyperpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
389 |
apply auto |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
390 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
391 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
392 |
lemma hrealpow_hyperpow_Infinitesimal_iff: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
393 |
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
394 |
apply (unfold hypnat_of_nat_def) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
395 |
apply (rule_tac z = "x" in eq_Abs_hypreal) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
396 |
apply (auto simp add: hrealpow hyperpow) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
397 |
done |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
398 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
399 |
lemma Infinitesimal_hrealpow: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
400 |
"[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
401 |
by (force intro!: Infinitesimal_hyperpow |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
402 |
simp add: hrealpow_hyperpow_Infinitesimal_iff |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
403 |
hypnat_of_nat_less_iff hypnat_of_nat_zero |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
404 |
simp del: hypnat_of_nat_less_iff [symmetric]) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
405 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
406 |
ML |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
407 |
{* |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
408 |
val hrealpow_two = thm "hrealpow_two"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
409 |
val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
410 |
val hrealpow_two_le = thm "hrealpow_two_le"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
411 |
val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
412 |
val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
413 |
val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
414 |
val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
415 |
val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
416 |
val hrabs_hrealpow_two = thm "hrabs_hrealpow_two"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
417 |
val two_hrealpow_ge_one = thm "two_hrealpow_ge_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
418 |
val two_hrealpow_gt = thm "two_hrealpow_gt"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
419 |
val hrealpow_minus_one = thm "hrealpow_minus_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
420 |
val double_lemma = thm "double_lemma"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
421 |
val hrealpow_minus_one2 = thm "hrealpow_minus_one2"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
422 |
val hrealpow = thm "hrealpow"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
423 |
val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
424 |
val hypreal_of_real_power = thm "hypreal_of_real_power"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
425 |
val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
426 |
val hrealpow_HFinite = thm "hrealpow_HFinite"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
427 |
val hyperpow_congruent = thm "hyperpow_congruent"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
428 |
val hyperpow = thm "hyperpow"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
429 |
val hyperpow_zero = thm "hyperpow_zero"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
430 |
val hyperpow_not_zero = thm "hyperpow_not_zero"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
431 |
val hyperpow_inverse = thm "hyperpow_inverse"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
432 |
val hyperpow_hrabs = thm "hyperpow_hrabs"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
433 |
val hyperpow_add = thm "hyperpow_add"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
434 |
val hyperpow_one = thm "hyperpow_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
435 |
val hyperpow_two = thm "hyperpow_two"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
436 |
val hyperpow_gt_zero = thm "hyperpow_gt_zero"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
437 |
val hyperpow_ge_zero = thm "hyperpow_ge_zero"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
438 |
val hyperpow_le = thm "hyperpow_le"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
439 |
val hyperpow_eq_one = thm "hyperpow_eq_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
440 |
val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
441 |
val hyperpow_mult = thm "hyperpow_mult"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
442 |
val hyperpow_two_le = thm "hyperpow_two_le"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
443 |
val hrabs_hyperpow_two = thm "hrabs_hyperpow_two"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
444 |
val hyperpow_two_hrabs = thm "hyperpow_two_hrabs"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
445 |
val hyperpow_two_gt_one = thm "hyperpow_two_gt_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
446 |
val hyperpow_two_ge_one = thm "hyperpow_two_ge_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
447 |
val two_hyperpow_ge_one = thm "two_hyperpow_ge_one"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
448 |
val hyperpow_minus_one2 = thm "hyperpow_minus_one2"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
449 |
val hyperpow_less_le = thm "hyperpow_less_le"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
450 |
val hyperpow_SHNat_le = thm "hyperpow_SHNat_le"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
451 |
val hyperpow_realpow = thm "hyperpow_realpow"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
452 |
val hyperpow_SReal = thm "hyperpow_SReal"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
453 |
val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
454 |
val hyperpow_le_le = thm "hyperpow_le_le"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
455 |
val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
456 |
val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
457 |
val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
458 |
val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
459 |
val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow"; |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
460 |
*} |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
11713
diff
changeset
|
461 |
|
10751 | 462 |
end |