author | paulson |
Mon, 16 Aug 1999 18:41:32 +0200 | |
changeset 7219 | 4e3f386c2e37 |
parent 7077 | 60b098bb8b8a |
child 7292 | dff3470c5c62 |
permissions | -rw-r--r-- |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
1 |
(* Title : RealPow.ML |
7219 | 2 |
ID : $Id$ |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
3 |
Author : Jacques D. Fleuriot |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
4 |
Copyright : 1998 University of Cambridge |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
5 |
Description : Natural Powers of reals theory |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
6 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
7 |
*) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
8 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
9 |
Goal "0r ^ (Suc n) = 0r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
10 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
11 |
qed "realpow_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
12 |
Addsimps [realpow_zero]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
13 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
14 |
Goal "r ~= 0r --> r ^ n ~= 0r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
15 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
16 |
by (auto_tac (claset() addIs [real_mult_not_zeroE], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
17 |
simpset() addsimps [real_zero_not_eq_one RS not_sym])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
18 |
qed_spec_mp "realpow_not_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
19 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
20 |
Goal "!!r. r ^ n = 0r ==> r = 0r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
21 |
by (blast_tac (claset() addIs [ccontr] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
22 |
addDs [realpow_not_zero]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
23 |
qed "realpow_zero_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
24 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
25 |
Goal "r ~= 0r --> rinv(r ^ n) = (rinv r) ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
26 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
27 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
28 |
by (forw_inst_tac [("n","n")] realpow_not_zero 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
29 |
by (auto_tac (claset() addDs [real_rinv_distrib], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
30 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
31 |
qed_spec_mp "realpow_rinv"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
32 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
33 |
Goal "rabs r ^ n = rabs (r ^ n)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
34 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
35 |
by (auto_tac (claset(),simpset() addsimps |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
36 |
[rabs_mult,rabs_one])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
37 |
qed "realpow_rabs"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
38 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
39 |
Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
40 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
41 |
by (auto_tac (claset(),simpset() addsimps real_mult_ac)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
42 |
qed "realpow_add"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
43 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
44 |
Goal "(r::real) ^ 1 = r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
45 |
by (Simp_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
46 |
qed "realpow_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
47 |
Addsimps [realpow_one]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
48 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
49 |
Goal "(r::real) ^ 2 = r * r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
50 |
by (Simp_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
51 |
qed "realpow_two"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
52 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
53 |
Goal "0r < r --> 0r <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
54 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
55 |
by (auto_tac (claset() addDs [real_less_imp_le] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
56 |
addIs [real_le_mult_order],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
57 |
qed_spec_mp "realpow_ge_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
58 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
59 |
Goal "0r < r --> 0r < r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
60 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
61 |
by (auto_tac (claset() addIs [real_mult_order], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
62 |
simpset() addsimps [real_zero_less_one])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
63 |
qed_spec_mp "realpow_gt_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
64 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
65 |
Goal "0r <= r --> 0r <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
66 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
67 |
by (auto_tac (claset() addIs [real_le_mult_order], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
68 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
69 |
qed_spec_mp "realpow_ge_zero2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
70 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
71 |
Goal "0r < x & x <= y --> x ^ n <= y ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
72 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
73 |
by (auto_tac (claset() addSIs [real_mult_le_mono], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
74 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
75 |
by (asm_simp_tac (simpset() addsimps [realpow_ge_zero]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
76 |
qed_spec_mp "realpow_le"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
77 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
78 |
Goal "0r <= x & x <= y --> x ^ n <= y ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
79 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
80 |
by (auto_tac (claset() addSIs [real_mult_le_mono4], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
81 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
82 |
by (asm_simp_tac (simpset() addsimps [realpow_ge_zero2]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
83 |
qed_spec_mp "realpow_le2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
84 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
85 |
Goal "0r < x & x < y & 0 < n --> x ^ n < y ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
86 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
87 |
by (auto_tac (claset() addIs [real_mult_less_mono, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
88 |
gr0I] addDs [realpow_gt_zero],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
89 |
qed_spec_mp "realpow_less"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
90 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
91 |
Goal "1r ^ n = 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
92 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
93 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
94 |
qed "realpow_eq_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
95 |
Addsimps [realpow_eq_one]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
96 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
97 |
Goal "rabs(-(1r ^ n)) = 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
98 |
by (simp_tac (simpset() addsimps |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
99 |
[rabs_minus_cancel,rabs_one]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
100 |
qed "rabs_minus_realpow_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
101 |
Addsimps [rabs_minus_realpow_one]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
102 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
103 |
Goal "rabs((-1r) ^ n) = 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
104 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
105 |
by (auto_tac (claset(),simpset() addsimps [rabs_mult, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
106 |
rabs_minus_cancel,rabs_one])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
107 |
qed "rabs_realpow_minus_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
108 |
Addsimps [rabs_realpow_minus_one]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
109 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
110 |
Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
111 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
112 |
by (auto_tac (claset(),simpset() addsimps real_mult_ac)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
113 |
qed "realpow_mult"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
114 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
115 |
Goal "0r <= r ^ 2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
116 |
by (simp_tac (simpset() addsimps [realpow_two]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
117 |
qed "realpow_two_le"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
118 |
Addsimps [realpow_two_le]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
119 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
120 |
Goal "rabs(x ^ 2) = x ^ 2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
121 |
by (simp_tac (simpset() addsimps [rabs_eqI1]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
122 |
qed "rabs_realpow_two"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
123 |
Addsimps [rabs_realpow_two]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
124 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
125 |
Goal "rabs(x) ^ 2 = x ^ 2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
126 |
by (simp_tac (simpset() addsimps |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
127 |
[realpow_rabs,rabs_eqI1] delsimps [realpow_Suc]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
128 |
qed "realpow_two_rabs"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
129 |
Addsimps [realpow_two_rabs]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
130 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
131 |
Goal "!!r. 1r < r ==> 1r < r ^ 2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
132 |
by (auto_tac (claset(),simpset() addsimps [realpow_two])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
133 |
by (cut_facts_tac [real_zero_less_one] 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
134 |
by (forw_inst_tac [("R1.0","0r")] real_less_trans 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
135 |
by (assume_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
136 |
by (dres_inst_tac [("z","r"),("x","1r")] real_mult_less_mono1 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
137 |
by (auto_tac (claset() addIs [real_less_trans],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
138 |
qed "realpow_two_gt_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
139 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
140 |
Goal "!!r. 1r <= r ==> 1r <= r ^ 2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
141 |
by (etac (real_le_imp_less_or_eq RS disjE) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
142 |
by (etac (realpow_two_gt_one RS real_less_imp_le) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
143 |
by (asm_simp_tac (simpset()) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
144 |
qed "realpow_two_ge_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
145 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
146 |
(* more general result *) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
147 |
Goal "1r < r --> 1r <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
148 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
149 |
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
150 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
151 |
by (dtac (real_zero_less_one RS real_mult_less_mono) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
152 |
by (dtac sym 4); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
153 |
by (auto_tac (claset() addSIs [real_less_imp_le], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
154 |
simpset() addsimps [real_zero_less_one])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
155 |
qed_spec_mp "realpow_ge_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
156 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
157 |
Goal "!!r. 1r < r ==> 1r < r ^ (Suc n)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
158 |
by (forw_inst_tac [("n","n")] realpow_ge_one 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
159 |
by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
160 |
by (dtac sym 2); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
161 |
by (forward_tac [real_zero_less_one RS real_less_trans] 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
162 |
by (dres_inst_tac [("y","r ^ n")] real_mult_less_mono2 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
163 |
by (auto_tac (claset() addDs [real_less_trans], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
164 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
165 |
qed "realpow_Suc_gt_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
166 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
167 |
Goal "!!r. 1r <= r ==> 1r <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
168 |
by (dtac real_le_imp_less_or_eq 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
169 |
by (auto_tac (claset() addDs [realpow_ge_one], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
170 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
171 |
qed "realpow_ge_one2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
172 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
173 |
Goal "!!r. 0r < r ==> 0r < r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
174 |
by (forw_inst_tac [("n","n")] realpow_ge_zero 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
175 |
by (forw_inst_tac [("n1","n")] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
176 |
((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
177 |
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
178 |
addIs [real_mult_order],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
179 |
qed "realpow_Suc_gt_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
180 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
181 |
Goal "!!r. 0r <= r ==> 0r <= r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
182 |
by (etac (real_le_imp_less_or_eq RS disjE) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
183 |
by (etac (realpow_ge_zero) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
184 |
by (asm_simp_tac (simpset()) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
185 |
qed "realpow_Suc_ge_zero"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
186 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
187 |
Goal "1r <= (1r +1r) ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
188 |
by (res_inst_tac [("j","1r ^ n")] real_le_trans 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
189 |
by (rtac realpow_le 2); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
190 |
by (auto_tac (claset() addIs [real_less_imp_le], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
191 |
simpset() addsimps [real_zero_less_one, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
192 |
real_one_less_two])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
193 |
qed "two_realpow_ge_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
194 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
195 |
Goal "real_of_nat n < (1r + 1r) ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
196 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
197 |
by (rtac (lemmaS RS ssubst) 2); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
198 |
by (rtac (real_of_nat_add RS subst) 2); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
199 |
by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
200 |
real_zero_less_one,real_add_mult_distrib,real_of_nat_one])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
201 |
by (blast_tac (claset() addSIs [real_add_less_le_mono, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
202 |
two_realpow_ge_one]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
203 |
qed "two_realpow_gt"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
204 |
Addsimps [two_realpow_gt,two_realpow_ge_one]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
205 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
206 |
Goal "(-1r) ^ (2*n) = 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
207 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
208 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
209 |
qed "realpow_minus_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
210 |
Addsimps [realpow_minus_one]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
211 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
212 |
Goal "(-1r) ^ (n + n) = 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
213 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
214 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
215 |
qed "realpow_minus_one2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
216 |
Addsimps [realpow_minus_one2]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
217 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
218 |
Goal "(-1r) ^ Suc (n + n) = -1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
219 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
220 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
221 |
qed "realpow_minus_one_odd"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
222 |
Addsimps [realpow_minus_one_odd]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
223 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
224 |
Goal "(-1r) ^ Suc (Suc (n + n)) = 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
225 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
226 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
227 |
qed "realpow_minus_one_even"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
228 |
Addsimps [realpow_minus_one_even]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
229 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
230 |
Goal "0r < r & r < 1r --> r ^ Suc n < r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
231 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
232 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
233 |
qed_spec_mp "realpow_Suc_less"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
234 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
235 |
Goal "0r <= r & r < 1r --> r ^ Suc n <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
236 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
237 |
by (auto_tac (claset() addIs [real_less_imp_le] addSDs |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
238 |
[real_le_imp_less_or_eq],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
239 |
qed_spec_mp "realpow_Suc_le"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
240 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
241 |
Goal "0r <= 0r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
242 |
by (exhaust_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
243 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
244 |
qed "realpow_zero_le"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
245 |
Addsimps [realpow_zero_le]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
246 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
247 |
Goal "0r < r & r < 1r --> r ^ Suc n <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
248 |
by (blast_tac (claset() addSIs [real_less_imp_le, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
249 |
realpow_Suc_less]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
250 |
qed_spec_mp "realpow_Suc_le2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
251 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
252 |
Goal "!!r. [| 0r <= r; r < 1r |] ==> r ^ Suc n <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
253 |
by (etac (real_le_imp_less_or_eq RS disjE) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
254 |
by (rtac realpow_Suc_le2 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
255 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
256 |
qed "realpow_Suc_le3"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
257 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
258 |
Goal "0r <= r & r < 1r & n < N --> r ^ N <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
259 |
by (induct_tac "N" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
260 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
261 |
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
262 |
by (ALLGOALS(dtac real_mult_le_mono3)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
263 |
by (REPEAT(assume_tac 1)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
264 |
by (REPEAT(assume_tac 3)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
265 |
by (auto_tac (claset(),simpset() addsimps |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
266 |
[less_Suc_eq])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
267 |
qed_spec_mp "realpow_less_le"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
268 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
269 |
Goal "!!r. [| 0r <= r; r < 1r; n <= N |] \ |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
270 |
\ ==> r ^ N <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
271 |
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
272 |
by (auto_tac (claset() addIs [realpow_less_le], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
273 |
simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
274 |
qed "realpow_le_le"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
275 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
276 |
Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n <= r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
277 |
by (dres_inst_tac [("n","1"),("N","Suc n")] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
278 |
(real_less_imp_le RS realpow_le_le) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
279 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
280 |
qed "realpow_Suc_le_self"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
281 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
282 |
Goal "!!r. [| 0r < r; r < 1r |] ==> r ^ Suc n < 1r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
283 |
by (blast_tac (claset() addIs [realpow_Suc_le_self, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
284 |
real_le_less_trans]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
285 |
qed "realpow_Suc_less_one"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
286 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
287 |
Goal "1r <= r --> r ^ n <= r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
288 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
289 |
by (auto_tac (claset() addSIs [real_mult_le_le_mono1],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
290 |
by (rtac ccontr 1 THEN dtac not_real_leE 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
291 |
by (dtac real_le_less_trans 1 THEN assume_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
292 |
by (etac (real_zero_less_one RS real_less_asym) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
293 |
qed_spec_mp "realpow_le_Suc"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
294 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
295 |
Goal "1r < r --> r ^ n < r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
296 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
297 |
by (auto_tac (claset() addSIs [real_mult_less_mono2],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
298 |
by (rtac ccontr 1 THEN dtac real_leI 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
299 |
by (dtac real_less_le_trans 1 THEN assume_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
300 |
by (etac (real_zero_less_one RS real_less_asym) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
301 |
qed_spec_mp "realpow_less_Suc"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
302 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
303 |
Goal "1r < r --> r ^ n <= r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
304 |
by (blast_tac (claset() addSIs [real_less_imp_le, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
305 |
realpow_less_Suc]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
306 |
qed_spec_mp "realpow_le_Suc2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
307 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
308 |
Goal "1r < r & n < N --> r ^ n <= r ^ N"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
309 |
by (induct_tac "N" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
310 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
311 |
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
312 |
by (ALLGOALS(dtac real_mult_self_le)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
313 |
by (assume_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
314 |
by (assume_tac 2); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
315 |
by (auto_tac (claset() addIs [real_le_trans], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
316 |
simpset() addsimps [less_Suc_eq])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
317 |
qed_spec_mp "realpow_gt_ge"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
318 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
319 |
Goal "1r <= r & n < N --> r ^ n <= r ^ N"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
320 |
by (induct_tac "N" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
321 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
322 |
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
323 |
by (ALLGOALS(dtac real_mult_self_le2)); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
324 |
by (assume_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
325 |
by (assume_tac 2); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
326 |
by (auto_tac (claset() addIs [real_le_trans], |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
327 |
simpset() addsimps [less_Suc_eq])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
328 |
qed_spec_mp "realpow_gt_ge2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
329 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
330 |
Goal "!!r. [| 1r < r; n <= N |] ==> r ^ n <= r ^ N"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
331 |
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
332 |
by (auto_tac (claset() addIs [realpow_gt_ge],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
333 |
qed "realpow_ge_ge"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
334 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
335 |
Goal "!!r. [| 1r <= r; n <= N |] ==> r ^ n <= r ^ N"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
336 |
by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
337 |
by (auto_tac (claset() addIs [realpow_gt_ge2],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
338 |
qed "realpow_ge_ge2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
339 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
340 |
Goal "!!r. 1r < r ==> r <= r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
341 |
by (dres_inst_tac [("n","1"),("N","Suc n")] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
342 |
realpow_ge_ge 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
343 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
344 |
qed_spec_mp "realpow_Suc_ge_self"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
345 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
346 |
Goal "!!r. 1r <= r ==> r <= r ^ Suc n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
347 |
by (dres_inst_tac [("n","1"),("N","Suc n")] |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
348 |
realpow_ge_ge2 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
349 |
by (Auto_tac); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
350 |
qed_spec_mp "realpow_Suc_ge_self2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
351 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
352 |
Goal "!!r. [| 1r < r; 0 < n |] ==> r <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
353 |
by (dtac (less_not_refl2 RS not0_implies_Suc) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
354 |
by (auto_tac (claset() addSIs |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
355 |
[realpow_Suc_ge_self],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
356 |
qed "realpow_ge_self"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
357 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
358 |
Goal "!!r. [| 1r <= r; 0 < n |] ==> r <= r ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
359 |
by (dtac (less_not_refl2 RS not0_implies_Suc) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
360 |
by (auto_tac (claset() addSIs [realpow_Suc_ge_self2],simpset())); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
361 |
qed "realpow_ge_self2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
362 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
363 |
Goal "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
364 |
by (induct_tac "n" 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
365 |
by (auto_tac (claset(),simpset() |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
366 |
addsimps [real_mult_commute])); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
367 |
qed_spec_mp "realpow_minus_mult"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
368 |
Addsimps [realpow_minus_mult]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
369 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
370 |
Goal "!!r. r ~= 0r ==> r * rinv(r) ^ 2 = rinv r"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
371 |
by (asm_simp_tac (simpset() addsimps [realpow_two, |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
372 |
real_mult_assoc RS sym]) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
373 |
qed "realpow_two_mult_rinv"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
374 |
Addsimps [realpow_two_mult_rinv]; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
diff
changeset
|
375 |