author | paulson |
Tue, 07 Dec 2004 16:16:23 +0100 | |
changeset 15383 | c49e4225ef4f |
parent 15251 | bb6f072c8d10 |
child 15481 | fc075ae929e4 |
permissions | -rw-r--r-- |
12196 | 1 |
(* Title : Transcendental.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998,1999 University of Cambridge |
|
13958
c1c67582c9b5
New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
12196
diff
changeset
|
4 |
1999,2001 University of Edinburgh |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
12196 | 6 |
*) |
7 |
||
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
8 |
header{*Power Series, Transcendental Functions etc.*} |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
9 |
|
15131 | 10 |
theory Transcendental |
15140 | 11 |
imports NthRoot Fact HSeries EvenOdd Lim |
15131 | 12 |
begin |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
13 |
|
12196 | 14 |
constdefs |
15013 | 15 |
root :: "[nat,real] => real" |
12196 | 16 |
"root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))" |
17 |
||
15013 | 18 |
sqrt :: "real => real" |
12196 | 19 |
"sqrt x == root 2 x" |
20 |
||
15013 | 21 |
exp :: "real => real" |
12196 | 22 |
"exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))" |
23 |
||
15013 | 24 |
sin :: "real => real" |
12196 | 25 |
"sin x == suminf(%n. (if even(n) then 0 else |
26 |
((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)" |
|
27 |
||
15013 | 28 |
diffs :: "(nat => real) => nat => real" |
12196 | 29 |
"diffs c == (%n. real (Suc n) * c(Suc n))" |
30 |
||
15013 | 31 |
cos :: "real => real" |
12196 | 32 |
"cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) |
33 |
else 0) * x ^ n)" |
|
34 |
||
15013 | 35 |
ln :: "real => real" |
12196 | 36 |
"ln x == (@u. exp u = x)" |
37 |
||
15013 | 38 |
pi :: "real" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
39 |
"pi == 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)" |
12196 | 40 |
|
15013 | 41 |
tan :: "real => real" |
12196 | 42 |
"tan x == (sin x)/(cos x)" |
43 |
||
15013 | 44 |
arcsin :: "real => real" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
45 |
"arcsin y == (@x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)" |
12196 | 46 |
|
15013 | 47 |
arcos :: "real => real" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
48 |
"arcos y == (@x. 0 \<le> x & x \<le> pi & cos x = y)" |
12196 | 49 |
|
15013 | 50 |
arctan :: "real => real" |
12196 | 51 |
"arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)" |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
52 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
53 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
54 |
lemma real_root_zero [simp]: "root (Suc n) 0 = 0" |
15229 | 55 |
apply (simp add: root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
56 |
apply (safe intro!: some_equality power_0_Suc elim!: realpow_zero_zero) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
57 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
58 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
59 |
lemma real_root_pow_pos: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
60 |
"0 < x ==> (root(Suc n) x) ^ (Suc n) = x" |
15229 | 61 |
apply (simp add: root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
62 |
apply (drule_tac n = n in realpow_pos_nth2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
63 |
apply (auto intro: someI2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
64 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
65 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
66 |
lemma real_root_pow_pos2: "0 \<le> x ==> (root(Suc n) x) ^ (Suc n) = x" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
67 |
by (auto dest!: real_le_imp_less_or_eq dest: real_root_pow_pos) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
68 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
69 |
lemma real_root_pos: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
70 |
"0 < x ==> root(Suc n) (x ^ (Suc n)) = x" |
15229 | 71 |
apply (simp add: root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
72 |
apply (rule some_equality) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
73 |
apply (frule_tac [2] n = n in zero_less_power) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
74 |
apply (auto simp add: zero_less_mult_iff) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
75 |
apply (rule_tac x = u and y = x in linorder_cases) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
76 |
apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
77 |
apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
78 |
apply (auto simp add: order_less_irrefl) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
79 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
80 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
81 |
lemma real_root_pos2: "0 \<le> x ==> root(Suc n) (x ^ (Suc n)) = x" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
82 |
by (auto dest!: real_le_imp_less_or_eq real_root_pos) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
83 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
84 |
lemma real_root_pos_pos: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
85 |
"0 < x ==> 0 \<le> root(Suc n) x" |
15229 | 86 |
apply (simp add: root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
87 |
apply (drule_tac n = n in realpow_pos_nth2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
88 |
apply (safe, rule someI2) |
15229 | 89 |
apply (auto intro!: order_less_imp_le dest: zero_less_power |
90 |
simp add: zero_less_mult_iff) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
91 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
92 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
93 |
lemma real_root_pos_pos_le: "0 \<le> x ==> 0 \<le> root(Suc n) x" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
94 |
by (auto dest!: real_le_imp_less_or_eq dest: real_root_pos_pos) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
95 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
96 |
lemma real_root_one [simp]: "root (Suc n) 1 = 1" |
15229 | 97 |
apply (simp add: root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
98 |
apply (rule some_equality, auto) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
99 |
apply (rule ccontr) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
100 |
apply (rule_tac x = u and y = 1 in linorder_cases) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
101 |
apply (drule_tac n = n in realpow_Suc_less_one) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
102 |
apply (drule_tac [4] n = n in power_gt1_lemma) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
103 |
apply (auto simp add: order_less_irrefl) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
104 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
105 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
106 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
107 |
subsection{*Square Root*} |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
108 |
|
15229 | 109 |
text{*needed because 2 is a binary numeral!*} |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
110 |
lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))" |
15229 | 111 |
by (simp del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 |
112 |
add: nat_numeral_0_eq_0 [symmetric]) |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
113 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
114 |
lemma real_sqrt_zero [simp]: "sqrt 0 = 0" |
15229 | 115 |
by (simp add: sqrt_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
116 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
117 |
lemma real_sqrt_one [simp]: "sqrt 1 = 1" |
15229 | 118 |
by (simp add: sqrt_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
119 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
120 |
lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)" |
15229 | 121 |
apply (simp add: sqrt_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
122 |
apply (rule iffI) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
123 |
apply (cut_tac r = "root 2 x" in realpow_two_le) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
124 |
apply (simp add: numeral_2_eq_2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
125 |
apply (subst numeral_2_eq_2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
126 |
apply (erule real_root_pow_pos2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
127 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
128 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
129 |
lemma [simp]: "(sqrt(u2\<twosuperior> + v2\<twosuperior>))\<twosuperior> = u2\<twosuperior> + v2\<twosuperior>" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
130 |
by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
131 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
132 |
lemma real_sqrt_pow2 [simp]: "0 \<le> x ==> (sqrt x)\<twosuperior> = x" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
133 |
by (simp add: real_sqrt_pow2_iff) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
134 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
135 |
lemma real_sqrt_abs_abs [simp]: "sqrt\<bar>x\<bar> ^ 2 = \<bar>x\<bar>" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
136 |
by (rule real_sqrt_pow2_iff [THEN iffD2], arith) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
137 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
138 |
lemma real_pow_sqrt_eq_sqrt_pow: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
139 |
"0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(x\<twosuperior>)" |
15229 | 140 |
apply (simp add: sqrt_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
141 |
apply (subst numeral_2_eq_2) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
142 |
apply (auto intro: real_root_pow_pos2 [THEN ssubst] real_root_pos2 [THEN ssubst] simp del: realpow_Suc) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
143 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
144 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
145 |
lemma real_pow_sqrt_eq_sqrt_abs_pow2: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
146 |
"0 \<le> x ==> (sqrt x)\<twosuperior> = sqrt(\<bar>x\<bar> ^ 2)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
147 |
by (simp add: real_pow_sqrt_eq_sqrt_pow [symmetric]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
148 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
149 |
lemma real_sqrt_pow_abs: "0 \<le> x ==> (sqrt x)\<twosuperior> = \<bar>x\<bar>" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
150 |
apply (rule real_sqrt_abs_abs [THEN subst]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
151 |
apply (rule_tac x1 = x in real_pow_sqrt_eq_sqrt_abs_pow2 [THEN ssubst]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
152 |
apply (rule_tac [2] real_pow_sqrt_eq_sqrt_pow [symmetric]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
153 |
apply (assumption, arith) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
154 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
155 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
156 |
lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
157 |
apply auto |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
158 |
apply (cut_tac x = x and y = 0 in linorder_less_linear) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
159 |
apply (simp add: zero_less_mult_iff) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
160 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
161 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
162 |
lemma real_mult_self_eq_zero_iff [simp]: "(r * r = 0) = (r = (0::real))" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
163 |
by auto |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
164 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
165 |
lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)" |
15229 | 166 |
apply (simp add: sqrt_def root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
167 |
apply (drule realpow_pos_nth2 [where n=1], safe) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
168 |
apply (rule someI2, auto) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
169 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
170 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
171 |
lemma real_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> sqrt(x)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
172 |
by (auto intro: real_sqrt_gt_zero simp add: order_le_less) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
173 |
|
15228 | 174 |
lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)" |
175 |
by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero]) |
|
176 |
||
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
177 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
178 |
(*we need to prove something like this: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
179 |
lemma "[|r ^ n = a; 0<n; 0 < a \<longrightarrow> 0 < r|] ==> root n a = r" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
180 |
apply (case_tac n, simp) |
15229 | 181 |
apply (simp add: root_def) |
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
182 |
apply (rule someI2 [of _ r], safe) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
183 |
apply (auto simp del: realpow_Suc dest: power_inject_base) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
184 |
*) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
185 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
186 |
lemma sqrt_eqI: "[|r\<twosuperior> = a; 0 \<le> r|] ==> sqrt a = r" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
187 |
apply (unfold sqrt_def root_def) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
188 |
apply (rule someI2 [of _ r], auto) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
189 |
apply (auto simp add: numeral_2_eq_2 simp del: realpow_Suc |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
190 |
dest: power_inject_base) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
191 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
192 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
193 |
lemma real_sqrt_mult_distrib: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
194 |
"[| 0 \<le> x; 0 \<le> y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
195 |
apply (rule sqrt_eqI) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
196 |
apply (simp add: power_mult_distrib) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
197 |
apply (simp add: zero_le_mult_iff real_sqrt_ge_zero) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
198 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
199 |
|
15229 | 200 |
lemma real_sqrt_mult_distrib2: |
201 |
"[|0\<le>x; 0\<le>y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)" |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
202 |
by (auto intro: real_sqrt_mult_distrib simp add: order_le_less) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
203 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
204 |
lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
205 |
by (auto intro!: real_sqrt_ge_zero) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
206 |
|
15229 | 207 |
lemma real_sqrt_sum_squares_mult_ge_zero [simp]: |
208 |
"0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))" |
|
15077
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
209 |
by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
210 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
211 |
lemma real_sqrt_sum_squares_mult_squared_eq [simp]: |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
212 |
"sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
213 |
by (auto simp add: real_sqrt_pow2_iff zero_le_mult_iff simp del: realpow_Suc) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
214 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
215 |
lemma real_sqrt_abs [simp]: "sqrt(x\<twosuperior>) = \<bar>x\<bar>" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
216 |
apply (rule abs_realpow_two [THEN subst]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
217 |
apply (rule real_sqrt_abs_abs [THEN subst]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
218 |
apply (subst real_pow_sqrt_eq_sqrt_pow) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
219 |
apply (auto simp add: numeral_2_eq_2 abs_mult) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
220 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
221 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
222 |
lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \<bar>x\<bar>" |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
223 |
apply (rule realpow_two [THEN subst]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
224 |
apply (subst numeral_2_eq_2 [symmetric]) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
225 |
apply (rule real_sqrt_abs) |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
226 |
done |
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
227 |
|
89840837108e
converting Hyperreal/Transcendental to Isar script
paulson
parents:
15013
diff
changeset
|
228 |
lemma real_sqrt_pow2_gt_zero: "0 < x ==> 0 < (sqrt x)\<twosuperior>" |