src/HOL/Hyperreal/Transcendental.thy
 changeset 15085 5693a977a767 parent 15081 32402f5624d1 child 15086 e6a2a98d5ef5
equal inserted replaced
15084:07f7b158ef32 15085:5693a977a767
`     6 *)`
`     6 *)`
`     7 `
`     7 `
`     8 header{*Power Series, Transcendental Functions etc.*}`
`     8 header{*Power Series, Transcendental Functions etc.*}`
`     9 `
`     9 `
`    10 theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:`
`    10 theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:`
`    13 `
`    11 `
`    14 constdefs`
`    12 constdefs`
`    15     root :: "[nat,real] => real"`
`    13     root :: "[nat,real] => real"`
`    16     "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"`
`    14     "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"`
`    17 `
`    15 `
`   662 apply (auto intro!: summable_sums)`
`   660 apply (auto intro!: summable_sums)`
`   663 apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)`
`   661 apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside)`
`   664 apply (auto simp add: add_commute)`
`   662 apply (auto simp add: add_commute)`
`   665 apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) `
`   663 apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) `
`   666 apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)`
`   664 apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)`
`   667 apply (rule sums_unique [symmetric])`
`   665 apply (rule sums_unique)`
`   668 apply (simp add: diff_def divide_inverse add_ac mult_ac)`
`   666 apply (simp add: diff_def divide_inverse add_ac mult_ac)`
`   669 apply (rule LIM_zero_cancel)`
`   667 apply (rule LIM_zero_cancel)`
`   670 apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)`
`   668 apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)`
`   671  prefer 2 apply (blast intro: termdiffs_aux) `
`   669  prefer 2 apply (blast intro: termdiffs_aux) `
`   672 apply (simp add: LIM_def, safe)`
`   670 apply (simp add: LIM_def, safe)`
`   688                right_diff_distrib [symmetric])`
`   686                right_diff_distrib [symmetric])`
`   689 apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)`
`   687 apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult)`
`   690 apply (simp add: sums_summable [THEN suminf_mult2])`
`   688 apply (simp add: sums_summable [THEN suminf_mult2])`
`   691 apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)`
`   689 apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)`
`   692 apply assumption`
`   690 apply assumption`
`   694 apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)`
`   691 apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)`
`   695 apply (rule_tac f = suminf in arg_cong)`
`   692 apply (rule_tac f = suminf in arg_cong)`
`   696 apply (rule ext)`
`   693 apply (rule ext)`
`   697 apply (simp add: diff_def right_distrib add_ac mult_ac)`
`   694 apply (simp add: diff_def right_distrib add_ac mult_ac)`
`   698 done`
`   695 done`
`  1266 done`
`  1263 done`
`  1267 `
`  1264 `
`  1268 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"`
`  1265 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"`
`  1269 apply (cut_tac x = x and y = y in sin_cos_add)`
`  1266 apply (cut_tac x = x and y = y in sin_cos_add)`
`  1270 apply (auto dest!: real_sum_squares_cancel_a `
`  1267 apply (auto dest!: real_sum_squares_cancel_a `
`  1271             simp add: numeral_2_eq_2 simp del: sin_cos_add)`
`  1268             simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)`
`  1272 done`
`  1269 done`
`  1273 `
`  1270 `
`  1274 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"`
`  1271 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"`
`  1275 apply (cut_tac x = x and y = y in sin_cos_add)`
`  1272 apply (cut_tac x = x and y = y in sin_cos_add)`
`  1276 apply (auto dest!: real_sum_squares_cancel_a`
`  1273 apply (auto dest!: real_sum_squares_cancel_a`
`  1277             simp add: numeral_2_eq_2 simp del: sin_cos_add)`
`  1274             simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)`
`  1278 done`
`  1275 done`
`  1279 `
`  1276 `
`  1280 lemma lemma_DERIV_sin_cos_minus: "\<forall>x.  `
`  1277 lemma lemma_DERIV_sin_cos_minus:`
`  1281           DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"`
`  1278     "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"`
`  1282 apply (safe, rule lemma_DERIV_subst)`
`  1279 apply (safe, rule lemma_DERIV_subst)`
`  1283 apply (best intro!: DERIV_intros intro: DERIV_chain2) `
`  1280 apply (best intro!: DERIV_intros intro: DERIV_chain2) `
`  1284 apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)`
`  1281 apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)`
`  1285 done`
`  1282 done`
`  1286 `
`  1283 `
`  1287 lemma sin_cos_minus [simp]: "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"`
`  1284 lemma sin_cos_minus [simp]: `
`  1288 apply (cut_tac y = 0 and x = x in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])`
`  1285     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"`
`       `
`  1286 apply (cut_tac y = 0 and x = x `
`       `
`  1287        in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])`
`  1289 apply (auto simp add: numeral_2_eq_2)`
`  1288 apply (auto simp add: numeral_2_eq_2)`
`  1290 done`
`  1289 done`
`  1291 `
`  1290 `
`  1292 lemma sin_minus [simp]: "sin (-x) = -sin(x)"`
`  1291 lemma sin_minus [simp]: "sin (-x) = -sin(x)"`
`  1293 apply (cut_tac x = x in sin_cos_minus)`
`  1292 apply (cut_tac x = x in sin_cos_minus)`
`  1294 apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus)`
`  1293 apply (auto dest!: real_sum_squares_cancel_a `
`       `
`  1294        simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus)`
`  1295 done`
`  1295 done`
`  1296 `
`  1296 `
`  1297 lemma cos_minus [simp]: "cos (-x) = cos(x)"`
`  1297 lemma cos_minus [simp]: "cos (-x) = cos(x)"`
`  1298 apply (cut_tac x = x in sin_cos_minus)`
`  1298 apply (cut_tac x = x in sin_cos_minus)`
`  1299 apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus)`
`  1299 apply (auto dest!: real_sum_squares_cancel_a `
`       `
`  1300                    simp add: numeral_2_eq_2 simp del: sin_cos_minus)`
`  1300 done`
`  1301 done`
`  1301 `
`  1302 `
`  1302 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"`
`  1303 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"`
`  1303 apply (unfold real_diff_def)`
`  1304 apply (unfold real_diff_def)`
`  1304 apply (simp (no_asm) add: sin_add)`
`  1305 apply (simp (no_asm) add: sin_add)`
`  1366 apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")`
`  1367 apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")`
`  1367 apply (simp only: mult_less_cancel_left, simp)`
`  1368 apply (simp only: mult_less_cancel_left, simp)`
`  1368 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])`
`  1369 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])`
`  1369 apply (subgoal_tac "x*x < 2*3", simp) `
`  1370 apply (subgoal_tac "x*x < 2*3", simp) `
`  1370 apply (rule mult_strict_mono)`
`  1371 apply (rule mult_strict_mono)`
`  1371 apply (auto simp add: real_of_nat_Suc simp del: fact_Suc)`
`  1372 apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)`
`  1372 apply (subst fact_Suc)`
`  1373 apply (subst fact_Suc)`
`  1373 apply (subst fact_Suc)`
`  1374 apply (subst fact_Suc)`
`  1374 apply (subst fact_Suc)`
`  1375 apply (subst fact_Suc)`
`  1375 apply (subst fact_Suc)`
`  1376 apply (subst fact_Suc)`
`  1376 apply (subst real_of_nat_mult)`
`  1377 apply (subst real_of_nat_mult)`
`  1428 apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n))) " in order_less_trans)`
`  1429 apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n))) " in order_less_trans)`
`  1429 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)`
`  1430 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)`
`  1430 apply (simp (no_asm) add: mult_assoc del: sumr_Suc)`
`  1431 apply (simp (no_asm) add: mult_assoc del: sumr_Suc)`
`  1431 apply (rule sumr_pos_lt_pair)`
`  1432 apply (rule sumr_pos_lt_pair)`
`  1432 apply (erule sums_summable, safe)`
`  1433 apply (erule sums_summable, safe)`
`  1433 apply (simp (no_asm) add: divide_inverse mult_assoc [symmetric] del: fact_Suc)`
`  1434 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] `
`       `
`  1435             del: fact_Suc)`
`  1434 apply (rule real_mult_inverse_cancel2)`
`  1436 apply (rule real_mult_inverse_cancel2)`
`  1435 apply (rule real_of_nat_fact_gt_zero)+`
`  1437 apply (rule real_of_nat_fact_gt_zero)+`
`  1436 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)`
`  1438 apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)`
`  1437 apply (subst fact_lemma) `
`  1439 apply (subst fact_lemma) `
`  1438 apply (subst fact_Suc)`
`  1440 apply (subst fact_Suc)`
`  1690 lemma sin_zero_lemma: "[| 0 \<le> x; sin x = 0 |] ==>  `
`  1692 lemma sin_zero_lemma: "[| 0 \<le> x; sin x = 0 |] ==>  `
`  1691       \<exists>n::nat. even n & x = real n * (pi/2)"`
`  1693       \<exists>n::nat. even n & x = real n * (pi/2)"`
`  1692 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")`
`  1694 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")`
`  1693  apply (clarify, rule_tac x = "n - 1" in exI)`
`  1695  apply (clarify, rule_tac x = "n - 1" in exI)`
`  1694  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)`
`  1696  apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)`
`  1695 apply (rule cos_zero_lemma, clarify) `
`  1697 apply (rule cos_zero_lemma)`
`  1696 apply (rule minus_le_iff [THEN iffD1])  `
`  1698 apply (simp_all add: add_increasing)  `
`  1697 apply (rule_tac y=0 in order_trans, auto)`
`       `
`  1698 done`
`  1699 done`
`  1699 `
`  1700 `
`  1700 `
`  1701 `
`  1701 (* also spoilt by numeral arithmetic *)`
`  1702 (* also spoilt by numeral arithmetic *)`
`  1702 lemma cos_zero_iff: "(cos x = 0) =  `
`  1703 lemma cos_zero_iff: "(cos x = 0) =  `
`  1990         simp add: power_mult_distrib left_distrib realpow_divide tan_def `
`  1991         simp add: power_mult_distrib left_distrib realpow_divide tan_def `
`  1991                   mult_assoc power_inverse [symmetric] `
`  1992                   mult_assoc power_inverse [symmetric] `
`  1992         simp del: realpow_Suc)`
`  1993         simp del: realpow_Suc)`
`  1993 done`
`  1994 done`
`  1994 `
`  1995 `
`  1995 lemma lemma_sin_cos_eq [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  `
`  1996 text{*NEEDED??*}`
`       `
`  1997 lemma [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  `
`  1996       cos (xa + 1 / 2 * real  (m) * pi)"`
`  1998       cos (xa + 1 / 2 * real  (m) * pi)"`
`  1997 apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)`
`  1999 apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)`
`  1998 done`
`  2000 done`
`  1999 `
`  2001 `
`  2000 lemma lemma_sin_cos_eq2 [simp]: "sin (xa + real (Suc m) * pi / 2) =  `
`  2002 text{*NEEDED??*}`
`       `
`  2003 lemma [simp]: "sin (xa + real (Suc m) * pi / 2) =  `
`  2001       cos (xa + real (m) * pi / 2)"`
`  2004       cos (xa + real (m) * pi / 2)"`
`  2002 apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)`
`  2005 apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)`
`  2003 done`
`  2006 done`
`  2004 `
`  2007 `
`  2005 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"`
`  2008 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"`
`  2331 lemma lemma_sin_cos_eq:`
`  2334 lemma lemma_sin_cos_eq:`
`  2332      "[| 0 < x * x + y * y;  `
`  2335      "[| 0 < x * x + y * y;  `
`  2333          1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]`
`  2336          1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]`
`  2334       ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2"`
`  2337       ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2"`
`  2335 apply (auto simp add: realpow_divide power2_eq_square [symmetric])`
`  2338 apply (auto simp add: realpow_divide power2_eq_square [symmetric])`
`  2336 apply (rule add_commute [THEN subst])`
`  2339 apply (subst add_commute)`
`  2337 apply (rule lemma_divide_rearrange, simp)`
`  2340 apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff)`
`  2338 apply (simp add: add_commute)`
`  2341 apply (simp add: add_commute)`
`  2339 done`
`  2342 done`
`  2340 `
`  2343 `
`  2341 lemma sin_x_y_disj:`
`  2344 lemma sin_x_y_disj:`
`  2342      "[| x \<noteq> 0;  `
`  2345      "[| x \<noteq> 0;  `
`  2393 apply (drule sin_ge_zero, assumption)`
`  2396 apply (drule sin_ge_zero, assumption)`
`  2394 apply (drule_tac x = x in real_sqrt_divide_less_zero, auto)`
`  2397 apply (drule_tac x = x in real_sqrt_divide_less_zero, auto)`
`  2395 done`
`  2398 done`
`  2396 `
`  2399 `
`  2397 lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"`
`  2400 lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"`
`  2398 by (auto intro: real_sum_squares_cancel)`
`  2401 by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)`
`  2399 `
`  2402 `
`  2400 lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"`
`  2403 lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"`
`  2401 apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)`
`  2404 apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)`
`  2402 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)`
`  2405 apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)`
`  2403 apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)`
`  2406 apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)`
`  2404 apply (auto dest: real_sum_squares_cancel2a simp add: power2_eq_square)`
`  2407 apply (auto dest: real_sum_squares_cancel2a `
`       `
`  2408             simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff)`
`  2405 apply (unfold arcsin_def)`
`  2409 apply (unfold arcsin_def)`
`  2406 apply (cut_tac x1 = x and y1 = y `
`  2410 apply (cut_tac x1 = x and y1 = y `
`  2407        in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])`
`  2411        in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])`
`  2408 apply (rule someI2_ex, blast)`
`  2412 apply (rule someI2_ex, blast)`
`  2409 apply (erule_tac V = "EX! xa. - (pi/2) \<le> xa & xa \<le> pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl)`
`  2413 apply (erule_tac V = "EX! xa. - (pi/2) \<le> xa & xa \<le> pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl)`
`  2410 apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast, auto)`
`  2414 apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast)`
`       `
`  2415 apply (auto simp add: real_0_le_add_iff real_add_eq_0_iff)`
`  2411 apply (drule cos_ge_zero, force)`
`  2416 apply (drule cos_ge_zero, force)`
`  2412 apply (drule_tac x = y in real_sqrt_divide_less_zero)`
`  2417 apply (drule_tac x = y in real_sqrt_divide_less_zero)`
`  2413 apply (auto simp add: real_add_commute)`
`  2418 apply (auto simp add: add_commute)`
`  2414 apply (insert polar_ex1 [of x "-y"], simp, clarify) `
`  2419 apply (insert polar_ex1 [of x "-y"], simp, clarify) `
`  2415 apply (rule_tac x = r in exI)`
`  2420 apply (rule_tac x = r in exI)`
`  2416 apply (rule_tac x = "-a" in exI, simp) `
`  2421 apply (rule_tac x = "-a" in exI, simp) `
`  2417 done`
`  2422 done`
`  2418 `
`  2423 `
`  2537 apply (subgoal_tac "\<forall>z. \<bar>z - x\<bar> \<le> e --> isCont f z")`
`  2542 apply (subgoal_tac "\<forall>z. \<bar>z - x\<bar> \<le> e --> isCont f z")`
`  2538 prefer 2 apply force`
`  2543 prefer 2 apply force`
`  2539 apply (drule_tac d = e in isCont_inj_range)`
`  2544 apply (drule_tac d = e in isCont_inj_range)`
`  2540 prefer 2 apply (assumption, assumption, safe)`
`  2545 prefer 2 apply (assumption, assumption, safe)`
`  2541 apply (rule_tac x = ea in exI, auto)`
`  2546 apply (rule_tac x = ea in exI, auto)`
`  2542 apply (rotate_tac 4)`
`  2547 apply (drule_tac x = "f (x) + xa" and P = "%y. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)" in spec)`
`  2543 apply (drule_tac x = "f (x) + xa" in spec)`
`       `
`  2544 apply auto`
`  2548 apply auto`
`  2545 apply (drule sym, auto, arith)`
`  2549 apply (drule sym, auto, arith)`
`  2546 done`
`  2550 done`
`  2547 `
`  2551 `
`  2548 lemma isCont_inv_fun_inv:`
`  2552 lemma isCont_inv_fun_inv:`
`  2865 val arcos_ge_minus_pi = thm "arcos_ge_minus_pi";`
`  2869 val arcos_ge_minus_pi = thm "arcos_ge_minus_pi";`
`  2866 val sin_x_y_disj = thm "sin_x_y_disj";`
`  2870 val sin_x_y_disj = thm "sin_x_y_disj";`
`  2867 val cos_x_y_disj = thm "cos_x_y_disj";`
`  2871 val cos_x_y_disj = thm "cos_x_y_disj";`
`  2868 val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";`
`  2872 val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";`
`  2869 val polar_ex1 = thm "polar_ex1";`
`  2873 val polar_ex1 = thm "polar_ex1";`
`  2871 val polar_ex2 = thm "polar_ex2";`
`  2874 val polar_ex2 = thm "polar_ex2";`
`  2872 val polar_Ex = thm "polar_Ex";`
`  2875 val polar_Ex = thm "polar_Ex";`
`  2873 val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";`
`  2876 val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";`
`  2874 val real_sqrt_ge_abs2 = thm "real_sqrt_ge_abs2";`
`  2877 val real_sqrt_ge_abs2 = thm "real_sqrt_ge_abs2";`
`  2875 val real_sqrt_two_gt_zero = thm "real_sqrt_two_gt_zero";`
`  2878 val real_sqrt_two_gt_zero = thm "real_sqrt_two_gt_zero";`