author | paulson |
Wed, 20 Dec 2000 12:15:52 +0100 | |
changeset 10712 | 351ba950d4d9 |
parent 10607 | 352f6f209775 |
child 10715 | c838477b5c18 |
permissions | -rw-r--r-- |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
1 |
(* Title : HyperPow.ML |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
2 |
Author : Jacques D. Fleuriot |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
3 |
Copyright : 1998 University of Cambridge |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
4 |
Description : Natural Powers of hyperreals theory |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
5 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
6 |
*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
7 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
8 |
Goal "(0::hypreal) ^ (Suc n) = 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
9 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
10 |
qed "hrealpow_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
11 |
Addsimps [hrealpow_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
12 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
13 |
Goal "r ~= (0::hypreal) --> r ^ n ~= 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
14 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
15 |
by (auto_tac (claset() addIs [hypreal_mult_not_0E], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
16 |
simpset() addsimps [hypreal_zero_not_eq_one RS not_sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
17 |
qed_spec_mp "hrealpow_not_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
18 |
|
10607 | 19 |
Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
20 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
21 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
22 |
by (forw_inst_tac [("n","n")] hrealpow_not_zero 1); |
10607 | 23 |
by (auto_tac (claset() addDs [inverse_mult_eq], |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
24 |
simpset())); |
10607 | 25 |
qed_spec_mp "hrealpow_inverse"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
26 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
27 |
Goal "abs (r::hypreal) ^ n = abs (r ^ n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
28 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
29 |
by (auto_tac (claset(),simpset() addsimps [hrabs_mult,hrabs_one])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
30 |
qed "hrealpow_hrabs"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
31 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
32 |
Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
33 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
34 |
by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
35 |
qed "hrealpow_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
36 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
37 |
Goal "(r::hypreal) ^ 1 = r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
38 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
39 |
qed "hrealpow_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
40 |
Addsimps [hrealpow_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
41 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
42 |
Goal "(r::hypreal) ^ 2 = r * r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
43 |
by (Simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
44 |
qed "hrealpow_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
45 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
46 |
Goal "(0::hypreal) < r --> 0 <= r ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
47 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
48 |
by (auto_tac (claset() addDs [hypreal_less_imp_le] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
49 |
addIs [hypreal_le_mult_order],simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
50 |
[hypreal_zero_less_one RS hypreal_less_imp_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
51 |
qed_spec_mp "hrealpow_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
52 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
53 |
Goal "(0::hypreal) < r --> 0 < r ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
54 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
55 |
by (auto_tac (claset() addIs [hypreal_mult_order], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
56 |
simpset() addsimps [hypreal_zero_less_one])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
57 |
qed_spec_mp "hrealpow_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
58 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
59 |
Goal "(0::hypreal) <= r --> 0 <= r ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
60 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
61 |
by (auto_tac (claset() addIs [hypreal_le_mult_order],simpset() |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
62 |
addsimps [hypreal_zero_less_one RS hypreal_less_imp_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
63 |
qed_spec_mp "hrealpow_ge_zero2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
64 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
65 |
Goal "(0::hypreal) < x & x <= y --> x ^ n <= y ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
66 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
67 |
by (auto_tac (claset() addSIs [hypreal_mult_le_mono], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
68 |
simpset() addsimps [hypreal_le_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
69 |
by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
70 |
qed_spec_mp "hrealpow_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
71 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
72 |
Goal "(0::hypreal) < x & x < y & 0 < n --> x ^ n < y ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
73 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
74 |
by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
75 |
addDs [hrealpow_gt_zero],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
76 |
qed "hrealpow_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
77 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
78 |
Goal "1hr ^ n = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
79 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
80 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
81 |
qed "hrealpow_eq_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
82 |
Addsimps [hrealpow_eq_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
83 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
84 |
Goal "abs(-(1hr ^ n)) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
85 |
by (simp_tac (simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
86 |
[hrabs_minus_cancel,hrabs_one]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
87 |
qed "hrabs_minus_hrealpow_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
88 |
Addsimps [hrabs_minus_hrealpow_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
89 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
90 |
Goal "abs((-1hr) ^ n) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
91 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
92 |
by (auto_tac (claset(),simpset() addsimps [hrabs_mult, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
93 |
hrabs_minus_cancel,hrabs_one])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
94 |
qed "hrabs_hrealpow_minus_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
95 |
Addsimps [hrabs_hrealpow_minus_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
96 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
97 |
Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
98 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
99 |
by (auto_tac (claset(),simpset() addsimps hypreal_mult_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
100 |
qed "hrealpow_mult"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
101 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
102 |
Goal "(0::hypreal) <= r ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
103 |
by (simp_tac (simpset() addsimps [hrealpow_two]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
104 |
qed "hrealpow_two_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
105 |
Addsimps [hrealpow_two_le]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
106 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
107 |
Goal "(0::hypreal) <= u ^ 2 + v ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
108 |
by (auto_tac (claset() addIs [hypreal_le_add_order],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
109 |
qed "hrealpow_two_le_add_order"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
110 |
Addsimps [hrealpow_two_le_add_order]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
111 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
112 |
Goal "(0::hypreal) <= u ^ 2 + v ^ 2 + w ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
113 |
by (auto_tac (claset() addSIs [hypreal_le_add_order],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
114 |
qed "hrealpow_two_le_add_order2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
115 |
Addsimps [hrealpow_two_le_add_order2]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
116 |
|
10712 | 117 |
Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (0::hypreal)) = (x = 0 & y = 0 & z = 0)"; |
118 |
by (simp_tac (HOL_ss addsimps [hypreal_three_squares_add_zero_iff, |
|
119 |
hrealpow_two]) 1); |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
120 |
qed "hrealpow_three_squares_add_zero_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
121 |
Addsimps [hrealpow_three_squares_add_zero_iff]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
122 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
123 |
Goal "abs(x ^ 2) = (x::hypreal) ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
124 |
by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
125 |
qed "hrabs_hrealpow_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
126 |
Addsimps [hrabs_hrealpow_two]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
127 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
128 |
Goal "abs(x) ^ 2 = (x::hypreal) ^ 2"; |
10712 | 129 |
by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1] |
130 |
delsimps [hpowr_Suc]) 1); |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
131 |
qed "hrealpow_two_hrabs"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
132 |
Addsimps [hrealpow_two_hrabs]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
133 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
134 |
Goal "!!r. 1hr < r ==> 1hr < r ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
135 |
by (auto_tac (claset(),simpset() addsimps [hrealpow_two])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
136 |
by (cut_facts_tac [hypreal_zero_less_one] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
137 |
by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
138 |
by (assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
139 |
by (dres_inst_tac [("z","r"),("x","1hr")] hypreal_mult_less_mono1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
140 |
by (auto_tac (claset() addIs [hypreal_less_trans],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
141 |
qed "hrealpow_two_gt_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
142 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
143 |
Goal "!!r. 1hr <= r ==> 1hr <= r ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
144 |
by (etac (hypreal_le_imp_less_or_eq RS disjE) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
145 |
by (etac (hrealpow_two_gt_one RS hypreal_less_imp_le) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
146 |
by (asm_simp_tac (simpset() addsimps [hypreal_le_refl]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
147 |
qed "hrealpow_two_ge_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
148 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
149 |
Goal "!!r. (0::hypreal) < r ==> 0 < r ^ Suc n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
150 |
by (forw_inst_tac [("n","n")] hrealpow_ge_zero 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
151 |
by (forw_inst_tac [("n1","n")] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
152 |
((hypreal_not_refl2 RS not_sym) RS hrealpow_not_zero RS not_sym) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
153 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
154 |
addIs [hypreal_mult_order],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
155 |
qed "hrealpow_Suc_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
156 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
157 |
Goal "!!r. (0::hypreal) <= r ==> 0 <= r ^ Suc n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
158 |
by (etac (hypreal_le_imp_less_or_eq RS disjE) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
159 |
by (etac (hrealpow_ge_zero) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
160 |
by (asm_simp_tac (simpset() addsimps [hypreal_le_refl]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
161 |
qed "hrealpow_Suc_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
162 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
163 |
Goal "1hr <= (1hr +1hr) ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
164 |
by (res_inst_tac [("j","1hr ^ n")] hypreal_le_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
165 |
by (rtac hrealpow_le 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
166 |
by (auto_tac (claset() addIs [hypreal_less_imp_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
167 |
simpset() addsimps [hypreal_zero_less_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
168 |
hypreal_one_less_two,hypreal_le_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
169 |
qed "two_hrealpow_ge_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
170 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
171 |
Goal "hypreal_of_nat n < (1hr + 1hr) ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
172 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
173 |
by (auto_tac (claset(),simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
174 |
hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
175 |
by (blast_tac (claset() addSIs [hypreal_add_less_le_mono, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
176 |
two_hrealpow_ge_one]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
177 |
qed "two_hrealpow_gt"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
178 |
Addsimps [two_hrealpow_gt,two_hrealpow_ge_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
179 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
180 |
Goal "(-1hr) ^ (2*n) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
181 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
182 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
183 |
qed "hrealpow_minus_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
184 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
185 |
Goal "(-1hr) ^ (n + n) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
186 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
187 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
188 |
qed "hrealpow_minus_one2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
189 |
Addsimps [hrealpow_minus_one2]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
190 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
191 |
Goal "(-(x::hypreal)) ^ 2 = x ^ 2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
192 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
193 |
qed "hrealpow_minus_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
194 |
Addsimps [hrealpow_minus_two]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
195 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
196 |
Goal "(0::hypreal) < r & r < 1hr --> r ^ Suc n < r ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
197 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
198 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
199 |
[hypreal_mult_less_mono2])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
200 |
qed_spec_mp "hrealpow_Suc_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
201 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
202 |
Goal "(0::hypreal) <= r & r < 1hr --> r ^ Suc n <= r ^ n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
203 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
204 |
by (auto_tac (claset() addIs [hypreal_less_imp_le] addSDs |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
205 |
[hypreal_le_imp_less_or_eq,hrealpow_Suc_less],simpset() |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
206 |
addsimps [hypreal_le_refl,hypreal_mult_less_mono2])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
207 |
qed_spec_mp "hrealpow_Suc_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
208 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
209 |
(* a few more theorems needed here *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
210 |
Goal "1hr <= r --> r ^ n <= r ^ Suc n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
211 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
212 |
by (auto_tac (claset() addSIs [hypreal_mult_le_le_mono1],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
213 |
by (rtac ccontr 1 THEN dtac not_hypreal_leE 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
214 |
by (dtac hypreal_le_less_trans 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
215 |
by (etac (hypreal_zero_less_one RS hypreal_less_asym) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
216 |
qed "hrealpow_less_Suc"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
217 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
218 |
Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
219 |
by (nat_ind_tac "m" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
220 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
221 |
[hypreal_one_def,hypreal_mult])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
222 |
qed "hrealpow"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
223 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
224 |
Goal "(x + (y::hypreal)) ^ 2 = \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
225 |
\ x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
226 |
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
227 |
hypreal_add_mult_distrib,hypreal_of_nat_two] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
228 |
@ hypreal_add_ac @ hypreal_mult_ac) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
229 |
qed "hrealpow_sum_square_expand"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
230 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
231 |
(*--------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
232 |
we'll prove the following theorem by going down to the |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
233 |
level of the ultrafilter and relying on the analogous |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
234 |
property for the real rather than prove it directly |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
235 |
using induction: proof is much simpler this way! |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
236 |
---------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
237 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
238 |
"[|(0::hypreal) <= x;0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
239 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
240 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
241 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
242 |
[hrealpow,hypreal_le,hypreal_mult])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
243 |
by (ultra_tac (claset() addIs [realpow_increasing],simpset()) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
244 |
qed "hrealpow_increasing"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
245 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
246 |
goalw HyperPow.thy [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
247 |
"!!x. [|(0::hypreal) <= x;0 <= y;x ^ Suc n = y ^ Suc n |] ==> x = y"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
248 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
249 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
250 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
251 |
[hrealpow,hypreal_mult,hypreal_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
252 |
by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
253 |
simpset()) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
254 |
qed "hrealpow_Suc_cancel_eq"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
255 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
256 |
Goal "x : HFinite --> x ^ n : HFinite"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
257 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
258 |
by (auto_tac (claset() addIs [HFinite_mult],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
259 |
qed_spec_mp "hrealpow_HFinite"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
260 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
261 |
(*--------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
262 |
Hypernaturals Powers |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
263 |
--------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
264 |
Goalw [congruent_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
265 |
"congruent hyprel \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
266 |
\ (%X Y. hyprel^^{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
267 |
by (safe_tac (claset() addSIs [ext])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
268 |
by (ALLGOALS(Fuf_tac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
269 |
qed "hyperpow_congruent"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
270 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
271 |
Goalw [hyperpow_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
272 |
"Abs_hypreal(hyprel^^{%n. X n}) pow Abs_hypnat(hypnatrel^^{%n. Y n}) = \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
273 |
\ Abs_hypreal(hyprel^^{%n. X n ^ Y n})"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
274 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
275 |
by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
276 |
simpset() addsimps [hyprel_in_hypreal RS |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
277 |
Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
278 |
by (Fuf_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
279 |
qed "hyperpow"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
280 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
281 |
Goalw [hypreal_zero_def,hypnat_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
282 |
"(0::hypreal) pow (n + 1hn) = 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
283 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
284 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
285 |
[hyperpow,hypnat_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
286 |
qed "hyperpow_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
287 |
Addsimps [hyperpow_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
288 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
289 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
290 |
"r ~= (0::hypreal) --> r pow n ~= 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
291 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
292 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
293 |
by (auto_tac (claset(),simpset() addsimps [hyperpow])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
294 |
by (dtac FreeUltrafilterNat_Compl_mem 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
295 |
by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
296 |
simpset()) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
297 |
qed_spec_mp "hyperpow_not_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
298 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
299 |
Goalw [hypreal_zero_def] |
10607 | 300 |
"r ~= (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
301 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
302 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
303 |
by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem], |
10607 | 304 |
simpset() addsimps [hypreal_inverse,hyperpow])); |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
305 |
by (rtac FreeUltrafilterNat_subset 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
306 |
by (auto_tac (claset() addDs [realpow_not_zero] |
10607 | 307 |
addIs [realpow_inverse],simpset())); |
308 |
qed "hyperpow_inverse"; |
|
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
309 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
310 |
Goal "abs r pow n = abs (r pow n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
311 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
312 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
313 |
by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
314 |
hyperpow,realpow_abs])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
315 |
qed "hyperpow_hrabs"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
316 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
317 |
Goal "r pow (n + m) = (r pow n) * (r pow m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
318 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
319 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
320 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
321 |
by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
322 |
hypreal_mult,realpow_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
323 |
qed "hyperpow_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
324 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
325 |
Goalw [hypnat_one_def] "r pow 1hn = r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
326 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
327 |
by (auto_tac (claset(),simpset() addsimps [hyperpow])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
328 |
qed "hyperpow_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
329 |
Addsimps [hyperpow_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
330 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
331 |
Goalw [hypnat_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
332 |
"r pow (1hn + 1hn) = r * r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
333 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
334 |
by (auto_tac (claset(),simpset() addsimps [hyperpow,hypnat_add, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
335 |
hypreal_mult,realpow_two])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
336 |
qed "hyperpow_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
337 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
338 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
339 |
"(0::hypreal) < r --> 0 < r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
340 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
341 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
342 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
343 |
realpow_gt_zero],simpset() addsimps [hyperpow,hypreal_less, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
344 |
hypreal_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
345 |
qed_spec_mp "hyperpow_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
346 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
347 |
Goal "(0::hypreal) < r --> 0 <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
348 |
by (blast_tac (claset() addSIs [hyperpow_gt_zero, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
349 |
hypreal_less_imp_le]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
350 |
qed_spec_mp "hyperpow_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
351 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
352 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
353 |
"(0::hypreal) <= r --> 0 <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
354 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
355 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
356 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
357 |
realpow_ge_zero2],simpset() addsimps [hyperpow,hypreal_le])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
358 |
qed "hyperpow_ge_zero2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
359 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
360 |
Goalw [hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
361 |
"(0::hypreal) < x & x <= y --> x pow n <= y pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
362 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
363 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
364 |
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
365 |
by (auto_tac (claset() addIs [realpow_le, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
366 |
(FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset)], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
367 |
simpset() addsimps [hyperpow,hypreal_le,hypreal_less])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
368 |
qed_spec_mp "hyperpow_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
369 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
370 |
Goalw [hypreal_one_def] "1hr pow n = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
371 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
372 |
by (auto_tac (claset(),simpset() addsimps [hyperpow])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
373 |
qed "hyperpow_eq_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
374 |
Addsimps [hyperpow_eq_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
375 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
376 |
Goalw [hypreal_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
377 |
"abs(-(1hr pow n)) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
378 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
379 |
by (auto_tac (claset(),simpset() addsimps [abs_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
380 |
hrabs_minus_cancel,hyperpow,hypreal_hrabs])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
381 |
qed "hrabs_minus_hyperpow_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
382 |
Addsimps [hrabs_minus_hyperpow_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
383 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
384 |
Goalw [hypreal_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
385 |
"abs((-1hr) pow n) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
386 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
387 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
388 |
[hyperpow,hypreal_minus,hypreal_hrabs])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
389 |
qed "hrabs_hyperpow_minus_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
390 |
Addsimps [hrabs_hyperpow_minus_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
391 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
392 |
Goal "(r * s) pow n = (r pow n) * (s pow n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
393 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
394 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
395 |
by (res_inst_tac [("z","s")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
396 |
by (auto_tac (claset(),simpset() addsimps [hyperpow, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
397 |
hypreal_mult,realpow_mult])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
398 |
qed "hyperpow_mult"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
399 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
400 |
Goal "(0::hypreal) <= r pow (1hn + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
401 |
by (simp_tac (simpset() addsimps [hyperpow_two]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
402 |
qed "hyperpow_two_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
403 |
Addsimps [hyperpow_two_le]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
404 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
405 |
Goal "abs(x pow (1hn + 1hn)) = x pow (1hn + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
406 |
by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
407 |
qed "hrabs_hyperpow_two"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
408 |
Addsimps [hrabs_hyperpow_two]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
409 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
410 |
Goal "abs(x) pow (1hn + 1hn) = x pow (1hn + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
411 |
by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
412 |
qed "hyperpow_two_hrabs"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
413 |
Addsimps [hyperpow_two_hrabs]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
414 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
415 |
Goal "!!r. 1hr < r ==> 1hr < r pow (1hn + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
416 |
by (auto_tac (claset(),simpset() addsimps [hyperpow_two])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
417 |
by (cut_facts_tac [hypreal_zero_less_one] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
418 |
by (forw_inst_tac [("R1.0","0")] hypreal_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
419 |
by (assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
420 |
by (dres_inst_tac [("z","r"),("x","1hr")] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
421 |
hypreal_mult_less_mono1 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
422 |
by (auto_tac (claset() addIs [hypreal_less_trans],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
423 |
qed "hyperpow_two_gt_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
424 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
425 |
Goal "!!r. 1hr <= r ==> 1hr <= r pow (1hn + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
426 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
427 |
addIs [hyperpow_two_gt_one,hypreal_less_imp_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
428 |
simpset() addsimps [hypreal_le_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
429 |
qed "hyperpow_two_ge_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
430 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
431 |
Goalw [hypnat_one_def,hypreal_zero_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
432 |
"!!r. (0::hypreal) < r ==> 0 < r pow (n + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
433 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
434 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
435 |
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
436 |
addDs [realpow_Suc_gt_zero],simpset() addsimps [hyperpow, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
437 |
hypreal_less,hypnat_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
438 |
qed "hyperpow_Suc_gt_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
439 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
440 |
Goal "!!r. (0::hypreal) <= r ==> 0 <= r pow (n + 1hn)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
441 |
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
442 |
addIs [hyperpow_ge_zero,hypreal_less_imp_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
443 |
simpset() addsimps [hypreal_le_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
444 |
qed "hyperpow_Suc_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
445 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
446 |
Goal "1hr <= (1hr +1hr) pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
447 |
by (res_inst_tac [("j","1hr pow n")] hypreal_le_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
448 |
by (rtac hyperpow_le 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
449 |
by (auto_tac (claset() addIs [hypreal_less_imp_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
450 |
simpset() addsimps [hypreal_zero_less_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
451 |
hypreal_one_less_two,hypreal_le_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
452 |
qed "two_hyperpow_ge_one"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
453 |
Addsimps [two_hyperpow_ge_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
454 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
455 |
Addsimps [simplify (simpset()) realpow_minus_one]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
456 |
Goalw [hypreal_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
457 |
"(-1hr) pow ((1hn + 1hn)*n) = 1hr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
458 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
459 |
by (auto_tac (claset(),simpset() addsimps [hyperpow, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
460 |
hypnat_add,hypreal_minus])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
461 |
qed "hyperpow_minus_one2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
462 |
Addsimps [hyperpow_minus_one2]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
463 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
464 |
Goalw [hypreal_zero_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
465 |
hypreal_one_def,hypnat_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
466 |
"(0::hypreal) < r & r < 1hr --> r pow (n + 1hn) < r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
467 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
468 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
469 |
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less] addEs |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
470 |
[FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset ], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
471 |
simpset() addsimps [hyperpow,hypreal_less,hypnat_add])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
472 |
qed_spec_mp "hyperpow_Suc_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
473 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
474 |
Goalw [hypreal_zero_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
475 |
hypreal_one_def,hypnat_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
476 |
"0 <= r & r < 1hr --> r pow (n + 1hn) <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
477 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
478 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
479 |
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] addEs |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
480 |
[FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset ], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
481 |
simpset() addsimps [hyperpow,hypreal_le,hypnat_add, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
482 |
hypreal_less])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
483 |
qed_spec_mp "hyperpow_Suc_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
484 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
485 |
Goalw [hypreal_zero_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
486 |
hypreal_one_def,hypnat_one_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
487 |
"(0::hypreal) <= r & r < 1hr & n < N --> r pow N <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
488 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
489 |
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
490 |
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
491 |
by (auto_tac (claset(),simpset() addsimps [hyperpow, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
492 |
hypreal_le,hypreal_less,hypnat_less])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
493 |
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
494 |
by (etac FreeUltrafilterNat_Int 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
495 |
by (auto_tac (claset() addSDs [conjI RS realpow_less_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
496 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
497 |
qed_spec_mp "hyperpow_less_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
498 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
499 |
Goal "!!r. [| (0::hypreal) <= r; r < 1hr |] ==> \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
500 |
\ ALL N n. n < N --> r pow N <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
501 |
by (blast_tac (claset() addSIs [hyperpow_less_le]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
502 |
qed "hyperpow_less_le2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
503 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
504 |
Goal "!!r. [| 0 <= r; r < 1hr; \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
505 |
\ N : HNatInfinite \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
506 |
\ |] ==> ALL n:SHNat. r pow N <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
507 |
by (auto_tac (claset() addSIs [hyperpow_less_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
508 |
simpset() addsimps [HNatInfinite_iff])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
509 |
qed "hyperpow_SHNat_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
510 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
511 |
Goalw [hypreal_of_real_def,hypnat_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
512 |
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
513 |
by (auto_tac (claset(),simpset() addsimps [hyperpow])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
514 |
qed "hyperpow_realpow"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
515 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
516 |
Goalw [SReal_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
517 |
"(hypreal_of_real r) pow (hypnat_of_nat n) : SReal"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
518 |
by (auto_tac (claset(),simpset() addsimps [hyperpow_realpow])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
519 |
qed "hyperpow_SReal"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
520 |
Addsimps [hyperpow_SReal]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
521 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
522 |
Goal "!!N. N : HNatInfinite ==> (0::hypreal) pow N = 0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
523 |
by (dtac HNatInfinite_is_Suc 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
524 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
525 |
qed "hyperpow_zero_HNatInfinite"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
526 |
Addsimps [hyperpow_zero_HNatInfinite]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
527 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
528 |
Goal "!!r. [| (0::hypreal) <= r; r < 1hr; n <= N |] ==> r pow N <= r pow n"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
529 |
by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
530 |
by (auto_tac (claset() addIs [hyperpow_less_le], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
531 |
simpset() addsimps [hypreal_le_refl])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
532 |
qed "hyperpow_le_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
533 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
534 |
Goal "!!r. [| (0::hypreal) < r; r < 1hr |] ==> r pow (n + 1hn) <= r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
535 |
by (dres_inst_tac [("n","1hn")] (hypreal_less_imp_le RS |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
536 |
hyperpow_le_le) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
537 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
538 |
qed "hyperpow_Suc_le_self"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
539 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
540 |
Goal "!!r. [| (0::hypreal) <= r; r < 1hr |] ==> r pow (n + 1hn) <= r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
541 |
by (dres_inst_tac [("n","1hn")] hyperpow_le_le 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
542 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
543 |
qed "hyperpow_Suc_le_self2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
544 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
545 |
Goalw [Infinitesimal_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
546 |
"!!x. [| x : Infinitesimal; 0 < N |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
547 |
\ ==> (abs x) pow N <= abs x"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
548 |
by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
549 |
simpset() addsimps [hyperpow_hrabs RS sym, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
550 |
hypnat_gt_zero_iff2,hrabs_ge_zero,SReal_one, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
551 |
hypreal_zero_less_one])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
552 |
qed "lemma_Infinitesimal_hyperpow"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
553 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
554 |
Goal "!!x. [| x : Infinitesimal; 0 < N |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
555 |
\ ==> x pow N : Infinitesimal"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
556 |
by (rtac hrabs_le_Infinitesimal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
557 |
by (dtac Infinitesimal_hrabs 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
558 |
by (auto_tac (claset() addSIs [lemma_Infinitesimal_hyperpow], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
559 |
simpset() addsimps [hyperpow_hrabs RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
560 |
qed "Infinitesimal_hyperpow"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
561 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
562 |
goalw HyperPow.thy [hypnat_of_nat_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
563 |
"(x ^ n : Infinitesimal) = \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
564 |
\ (x pow (hypnat_of_nat n) : Infinitesimal)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
565 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
566 |
by (auto_tac (claset(),simpset() addsimps [hrealpow, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
567 |
hyperpow])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
568 |
qed "hrealpow_hyperpow_Infinitesimal_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
569 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
570 |
goal HyperPow.thy |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
571 |
"!!x. [| x : Infinitesimal; 0 < n |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
572 |
\ ==> x ^ n : Infinitesimal"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
573 |
by (auto_tac (claset() addSIs [Infinitesimal_hyperpow], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
574 |
simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
575 |
hypnat_of_nat_less_iff,hypnat_of_nat_zero] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
576 |
delsimps [hypnat_of_nat_less_iff RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
577 |
qed "Infinitesimal_hrealpow"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
578 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
579 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
580 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
581 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
582 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
583 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
584 |