2496 by (cut_inst_tac [("x","x")] sin_cos_squared_add3 1); |
2496 by (cut_inst_tac [("x","x")] sin_cos_squared_add3 1); |
2497 by Auto_tac; |
2497 by Auto_tac; |
2498 qed "cos_one_sin_zero"; |
2498 qed "cos_one_sin_zero"; |
2499 |
2499 |
2500 (*-------------------------------------------------------------------------------*) |
2500 (*-------------------------------------------------------------------------------*) |
2501 (* Add continuity checker in backup of theory? *) |
2501 (* A few extra theorems *) |
2502 (*-------------------------------------------------------------------------------*) |
2502 (*-------------------------------------------------------------------------------*) |
2503 |
2503 |
|
2504 Goal "[| 0 <= x; x < y |] ==> root(Suc n) x < root(Suc n) y"; |
|
2505 by (ftac order_le_less_trans 1); |
|
2506 by (assume_tac 1); |
|
2507 by (forw_inst_tac [("n1","n")] (real_root_pow_pos2 RS ssubst) 1); |
|
2508 by (rotate_tac 1 1); |
|
2509 by (assume_tac 1); |
|
2510 by (forw_inst_tac [("n1","n")] (real_root_pow_pos RS ssubst) 1); |
|
2511 by (rotate_tac 3 1 THEN assume_tac 1); |
|
2512 by (dres_inst_tac [("y","root (Suc n) y ^ Suc n")] order_less_imp_le 1 ); |
|
2513 by (forw_inst_tac [("n","n")] real_root_pos_pos_le 1); |
|
2514 by (forw_inst_tac [("n","n")] real_root_pos_pos 1); |
|
2515 by (dres_inst_tac [("x","root (Suc n) x"), |
|
2516 ("y","root (Suc n) y")] realpow_increasing 1); |
|
2517 by (assume_tac 1 THEN assume_tac 1); |
|
2518 by (dres_inst_tac [("x","root (Suc n) x")] order_le_imp_less_or_eq 1); |
|
2519 by Auto_tac; |
|
2520 by (dres_inst_tac [("f","%x. x ^ (Suc n)")] arg_cong 1); |
|
2521 by (auto_tac (claset(),simpset() addsimps [real_root_pow_pos2] |
|
2522 delsimps [realpow_Suc])); |
|
2523 qed "real_root_less_mono"; |
|
2524 |
|
2525 Goal "[| 0 <= x; x <= y |] ==> root(Suc n) x <= root(Suc n) y"; |
|
2526 by (dres_inst_tac [("y","y")] order_le_imp_less_or_eq 1 ); |
|
2527 by (auto_tac (claset() addDs [real_root_less_mono] |
|
2528 addIs [order_less_imp_le],simpset())); |
|
2529 qed "real_root_le_mono"; |
|
2530 |
|
2531 Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"; |
|
2532 by (auto_tac (claset() addIs [real_root_less_mono],simpset())); |
|
2533 by (rtac ccontr 1 THEN dtac real_leI 1); |
|
2534 by (dres_inst_tac [("x","y"),("n","n")] real_root_le_mono 1); |
|
2535 by Auto_tac; |
|
2536 qed "real_root_less_iff"; |
|
2537 Addsimps [real_root_less_iff]; |
|
2538 |
|
2539 Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x <= root(Suc n) y) = (x <= y)"; |
|
2540 by (auto_tac (claset() addIs [real_root_le_mono],simpset())); |
|
2541 by (simp_tac (simpset() addsimps [real_le_def]) 1); |
|
2542 by Auto_tac; |
|
2543 by (dres_inst_tac [("x","y"),("n","n")] real_root_less_mono 1); |
|
2544 by Auto_tac; |
|
2545 qed "real_root_le_iff"; |
|
2546 Addsimps [real_root_le_iff]; |
|
2547 |
|
2548 Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"; |
|
2549 by (auto_tac (claset() addSIs [real_le_anti_sym],simpset())); |
|
2550 by (res_inst_tac [("n1","n")] (real_root_le_iff RS iffD1) 1); |
|
2551 by (res_inst_tac [("n1","n")] (real_root_le_iff RS iffD1) 4); |
|
2552 by Auto_tac; |
|
2553 qed "real_root_eq_iff"; |
|
2554 Addsimps [real_root_eq_iff]; |
|
2555 |
|
2556 Goal "[| 0 <= x; 0 <= y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"; |
|
2557 by (auto_tac (claset() addDs [real_root_pos2], |
|
2558 simpset() delsimps [realpow_Suc])); |
|
2559 qed "real_root_pos_unique"; |
|
2560 |
|
2561 Goal "[| 0 <= x; 0 <= y |]\ |
|
2562 \ ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"; |
|
2563 by (rtac real_root_pos_unique 1); |
|
2564 by (auto_tac (claset() addSIs [real_root_pos_pos_le],simpset() |
|
2565 addsimps [realpow_mult,real_0_le_mult_iff, |
|
2566 real_root_pow_pos2] delsimps [realpow_Suc])); |
|
2567 qed "real_root_mult"; |
|
2568 |
|
2569 Goal "0 <= x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"; |
|
2570 by (rtac real_root_pos_unique 1); |
|
2571 by (auto_tac (claset() addIs [real_root_pos_pos_le],simpset() |
|
2572 addsimps [realpow_inverse RS sym,real_root_pow_pos2] |
|
2573 delsimps [realpow_Suc])); |
|
2574 qed "real_root_inverse"; |
|
2575 |
|
2576 Goalw [real_divide_def] |
|
2577 "[| 0 <= x; 0 <= y |] \ |
|
2578 \ ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)"; |
|
2579 by (auto_tac (claset(),simpset() addsimps [real_root_mult, |
|
2580 real_root_inverse])); |
|
2581 qed "real_root_divide"; |
|
2582 |
|
2583 Goalw [sqrt_def] "[| 0 <= x; x < y |] ==> sqrt(x) < sqrt(y)"; |
|
2584 by (auto_tac (claset() addIs [real_root_less_mono],simpset())); |
|
2585 qed "real_sqrt_less_mono"; |
|
2586 |
|
2587 Goalw [sqrt_def] "[| 0 <= x; x <= y |] ==> sqrt(x) <= sqrt(y)"; |
|
2588 by (auto_tac (claset() addIs [real_root_le_mono],simpset())); |
|
2589 qed "real_sqrt_le_mono"; |
|
2590 |
|
2591 Goalw [sqrt_def] "[| 0 <= x; 0 <= y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"; |
|
2592 by Auto_tac; |
|
2593 qed "real_sqrt_less_iff"; |
|
2594 Addsimps [real_sqrt_less_iff]; |
|
2595 |
|
2596 Goalw [sqrt_def] "[| 0 <= x; 0 <= y |] ==> (sqrt(x) <= sqrt(y)) = (x <= y)"; |
|
2597 by Auto_tac; |
|
2598 qed "real_sqrt_le_iff"; |
|
2599 Addsimps [real_sqrt_le_iff]; |
|
2600 |
|
2601 Goalw [sqrt_def] "[| 0 <= x; 0 <= y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"; |
|
2602 by Auto_tac; |
|
2603 qed "real_sqrt_eq_iff"; |
|
2604 Addsimps [real_sqrt_eq_iff]; |
|
2605 |
|
2606 Goal "(sqrt(x ^ 2 + y ^ 2) < 1) = (x ^ 2 + y ^ 2 < 1)"; |
|
2607 by (rtac (real_sqrt_one RS subst) 1); |
|
2608 by (Step_tac 1); |
|
2609 by (rtac real_sqrt_less_mono 2); |
|
2610 by (dtac (rotate_prems 2 (real_sqrt_less_iff RS iffD1)) 1); |
|
2611 by Auto_tac; |
|
2612 qed "real_sqrt_sos_less_one_iff"; |
|
2613 Addsimps [real_sqrt_sos_less_one_iff]; |
|
2614 |
|
2615 Goal "(sqrt(x ^ 2 + y ^ 2) = 1) = (x ^ 2 + y ^ 2 = 1)"; |
|
2616 by (rtac (real_sqrt_one RS subst) 1); |
|
2617 by (Step_tac 1); |
|
2618 by (dtac (rotate_prems 2 (real_sqrt_eq_iff RS iffD1)) 1); |
|
2619 by Auto_tac; |
|
2620 qed "real_sqrt_sos_eq_one_iff"; |
|
2621 Addsimps [real_sqrt_sos_eq_one_iff]; |
|
2622 |
|
2623 Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r"; |
|
2624 by (real_div_undefined_case_tac "r=0" 1); |
|
2625 by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac)); |
|
2626 qed "real_divide_square_eq"; |
|
2627 Addsimps [real_divide_square_eq]; |
|
2628 |
|
2629 (*-------------------------------------------------------------------------------*) |
|
2630 (* More theorems about sqrt, transcendental functions etc. needed in Complex.ML *) |
|
2631 (*-------------------------------------------------------------------------------*) |
|
2632 |
|
2633 |
|
2634 goal Real.thy "2 = Suc (Suc 0)"; |
|
2635 by (Simp_tac 1); |
|
2636 qed "two_eq_Suc_Suc"; |
|
2637 |
|
2638 val realpow_num_two = CLAIM "2 = Suc(Suc 0)"; |
|
2639 |
|
2640 Goal "x ^ 2 = x * (x::real)"; |
|
2641 by (auto_tac (claset(),simpset() addsimps [CLAIM "2 = Suc(Suc 0)"])); |
|
2642 qed "realpow_two_eq_mult"; |
|
2643 |
|
2644 Goalw [real_divide_def] |
|
2645 "0 < x ==> 0 <= x/(sqrt (x * x + y * y))"; |
|
2646 by (ftac ((real_sqrt_sum_squares_ge1 RSN (2,order_less_le_trans)) |
|
2647 RS (CLAIM "0 < x ==> 0 < inverse (x::real)")) 1); |
|
2648 by (rtac (real_mult_order RS order_less_imp_le) 1); |
|
2649 by (auto_tac (claset(),simpset() addsimps [realpow_num_two])); |
|
2650 qed "lemma_real_divide_sqrt"; |
|
2651 |
|
2652 Goal "0 < x ==> -(1::real) <= x/(sqrt (x * x + y * y))"; |
|
2653 by (rtac real_le_trans 1); |
|
2654 by (rtac lemma_real_divide_sqrt 2); |
|
2655 by Auto_tac; |
|
2656 qed "lemma_real_divide_sqrt_ge_minus_one"; |
|
2657 |
|
2658 Goal "x < 0 ==> 0 < sqrt (x * x + y * y)"; |
|
2659 by (rtac real_sqrt_gt_zero 1); |
|
2660 by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1); |
|
2661 by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); |
|
2662 qed "real_sqrt_sum_squares_gt_zero1"; |
|
2663 |
|
2664 Goal "0 < x ==> 0 < sqrt (x * x + y * y)"; |
|
2665 by (rtac real_sqrt_gt_zero 1); |
|
2666 by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1); |
|
2667 by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); |
|
2668 qed "real_sqrt_sum_squares_gt_zero2"; |
|
2669 |
|
2670 Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; |
|
2671 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
|
2672 by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero2, |
|
2673 real_sqrt_sum_squares_gt_zero1],simpset() addsimps [realpow_num_two])); |
|
2674 qed "real_sqrt_sum_squares_gt_zero3"; |
|
2675 |
|
2676 Goal "y ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; |
|
2677 by (dres_inst_tac [("y","x")] real_sqrt_sum_squares_gt_zero3 1); |
|
2678 by (auto_tac (claset(),simpset() addsimps [real_add_commute])); |
|
2679 qed "real_sqrt_sum_squares_gt_zero3a"; |
|
2680 |
|
2681 Goal "sqrt(x ^ 2 + y ^ 2) = x ==> y = 0"; |
|
2682 by (rtac ccontr 1); |
|
2683 by (forw_inst_tac [("x","x")] real_sum_squares_not_zero2 1); |
|
2684 by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1); |
|
2685 by (forw_inst_tac [("x","x"),("y","y")] real_sum_square_gt_zero2 1); |
|
2686 by (dtac real_sqrt_gt_zero_pow2 1); |
|
2687 by Auto_tac; |
|
2688 qed "real_sqrt_sum_squares_eq_cancel"; |
|
2689 Addsimps [real_sqrt_sum_squares_eq_cancel]; |
|
2690 |
|
2691 Goal "sqrt(x ^ 2 + y ^ 2) = y ==> x = 0"; |
|
2692 by (res_inst_tac [("x","y")] real_sqrt_sum_squares_eq_cancel 1); |
|
2693 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); |
|
2694 qed "real_sqrt_sum_squares_eq_cancel2"; |
|
2695 Addsimps [real_sqrt_sum_squares_eq_cancel2]; |
|
2696 |
|
2697 Goal "x < 0 ==> x/(sqrt (x * x + y * y)) <= 1"; |
|
2698 by (dtac (ARITH_PROVE "x < 0 ==> (0::real) < -x") 1); |
|
2699 by (dres_inst_tac [("y","y")] |
|
2700 lemma_real_divide_sqrt_ge_minus_one 1); |
|
2701 by (dtac (ARITH_PROVE "x <= y ==> -y <= -(x::real)") 1); |
|
2702 by Auto_tac; |
|
2703 qed "lemma_real_divide_sqrt_le_one"; |
|
2704 |
|
2705 Goal "x < 0 ==> -(1::real) <= x/(sqrt (x * x + y * y))"; |
|
2706 by (case_tac "y = 0" 1); |
|
2707 by Auto_tac; |
|
2708 by (ftac abs_minus_eqI2 1); |
|
2709 by (auto_tac (claset(),simpset() addsimps [real_minus_inverse])); |
|
2710 by (rtac order_less_imp_le 1); |
|
2711 by (res_inst_tac [("z1","sqrt(x * x + y * y)")] |
|
2712 (real_mult_less_iff1 RS iffD1) 1); |
|
2713 by (forw_inst_tac [("y2","y")] |
|
2714 (real_sqrt_sum_squares_gt_zero1 RS real_not_refl2 |
|
2715 RS not_sym) 2); |
|
2716 by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero1], |
|
2717 simpset() addsimps real_mult_ac)); |
|
2718 by (rtac (ARITH_PROVE "-x < y ==> -y < (x::real)") 1); |
|
2719 by (cut_inst_tac [("x","-x"),("y","y")] real_sqrt_sum_squares_ge1 1); |
|
2720 by (dtac real_le_imp_less_or_eq 1); |
|
2721 by (Step_tac 1); |
|
2722 by (asm_full_simp_tac (simpset() addsimps [realpow_num_two]) 1); |
|
2723 by (dtac (sym RS real_sqrt_sum_squares_eq_cancel) 1); |
|
2724 by Auto_tac; |
|
2725 qed "lemma_real_divide_sqrt_ge_minus_one2"; |
|
2726 |
|
2727 Goal "0 < x ==> x/(sqrt (x * x + y * y)) <= 1"; |
|
2728 by (dtac (ARITH_PROVE "0 < x ==> -x < (0::real)") 1); |
|
2729 by (dres_inst_tac [("y","y")] |
|
2730 lemma_real_divide_sqrt_ge_minus_one2 1); |
|
2731 by (dtac (ARITH_PROVE "x <= y ==> -y <= -(x::real)") 1); |
|
2732 by Auto_tac; |
|
2733 qed "lemma_real_divide_sqrt_le_one2"; |
|
2734 (* was qed "lemma_real_mult_self_rinv_sqrt_squared5" *) |
|
2735 |
|
2736 Goal "-(1::real)<= x / sqrt (x * x + y * y)"; |
|
2737 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
|
2738 by (Step_tac 1); |
|
2739 by (rtac lemma_real_divide_sqrt_ge_minus_one2 1); |
|
2740 by (rtac lemma_real_divide_sqrt_ge_minus_one 3); |
|
2741 by Auto_tac; |
|
2742 qed "cos_x_y_ge_minus_one"; |
|
2743 Addsimps [cos_x_y_ge_minus_one]; |
|
2744 |
|
2745 Goal "-(1::real)<= y / sqrt (x * x + y * y)"; |
|
2746 by (cut_inst_tac [("x","y"),("y","x")] cos_x_y_ge_minus_one 1); |
|
2747 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); |
|
2748 qed "cos_x_y_ge_minus_one1a"; |
|
2749 Addsimps [cos_x_y_ge_minus_one1a, |
|
2750 simplify (simpset()) cos_x_y_ge_minus_one1a]; |
|
2751 |
|
2752 Goal "x / sqrt (x * x + y * y) <= 1"; |
|
2753 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
|
2754 by (Step_tac 1); |
|
2755 by (rtac lemma_real_divide_sqrt_le_one 1); |
|
2756 by (rtac lemma_real_divide_sqrt_le_one2 3); |
|
2757 by Auto_tac; |
|
2758 qed "cos_x_y_le_one"; |
|
2759 Addsimps [cos_x_y_le_one]; |
|
2760 |
|
2761 Goal "y / sqrt (x * x + y * y) <= 1"; |
|
2762 by (cut_inst_tac [("x","y"),("y","x")] cos_x_y_le_one 1); |
|
2763 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1); |
|
2764 qed "cos_x_y_le_one2"; |
|
2765 Addsimps [cos_x_y_le_one2]; |
|
2766 |
|
2767 Addsimps [[cos_x_y_ge_minus_one,cos_x_y_le_one] MRS cos_arcos]; |
|
2768 Addsimps [[cos_x_y_ge_minus_one,cos_x_y_le_one] MRS arcos_bounded]; |
|
2769 |
|
2770 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS cos_arcos]; |
|
2771 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS arcos_bounded]; |
|
2772 |
|
2773 Goal "-(1::real) <= abs(x) / sqrt (x * x + y * y)"; |
|
2774 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
|
2775 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
|
2776 by (dtac lemma_real_divide_sqrt_ge_minus_one 1 THEN Force_tac 1); |
|
2777 qed "cos_rabs_x_y_ge_minus_one"; |
|
2778 |
|
2779 Addsimps [cos_rabs_x_y_ge_minus_one, |
|
2780 simplify (simpset()) cos_rabs_x_y_ge_minus_one]; |
|
2781 |
|
2782 Goal "abs(x) / sqrt (x * x + y * y) <= 1"; |
|
2783 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
|
2784 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
|
2785 by (dtac lemma_real_divide_sqrt_ge_minus_one2 1 THEN Force_tac 1); |
|
2786 qed "cos_rabs_x_y_le_one"; |
|
2787 Addsimps [cos_rabs_x_y_le_one]; |
|
2788 |
|
2789 Addsimps [[cos_rabs_x_y_ge_minus_one,cos_rabs_x_y_le_one] MRS cos_arcos]; |
|
2790 Addsimps [[cos_rabs_x_y_ge_minus_one,cos_rabs_x_y_le_one] MRS arcos_bounded]; |
|
2791 |
|
2792 Goal "-pi < 0"; |
|
2793 by (Simp_tac 1); |
|
2794 qed "minus_pi_less_zero"; |
|
2795 Addsimps [minus_pi_less_zero]; |
|
2796 Addsimps [minus_pi_less_zero RS order_less_imp_le]; |
|
2797 |
|
2798 Goal "[| -(1::real) <= y; y <= 1 |] ==> -pi <= arcos y"; |
|
2799 by (rtac real_le_trans 1); |
|
2800 by (rtac arcos_lbound 2); |
|
2801 by Auto_tac; |
|
2802 qed "arcos_ge_minus_pi"; |
|
2803 |
|
2804 Addsimps [[cos_x_y_ge_minus_one,cos_x_y_le_one] MRS arcos_ge_minus_pi]; |
|
2805 |
|
2806 (* How tedious! *) |
|
2807 Goal "[| x + (y::real) ~= 0; 1 - z = x/(x + y) \ |
|
2808 \ |] ==> z = y/(x + y)"; |
|
2809 by (res_inst_tac [("c1","x + y")] (real_mult_right_cancel RS iffD1) 1); |
|
2810 by (forw_inst_tac [("c1","x + y")] (real_mult_right_cancel RS iffD2) 2); |
|
2811 by (assume_tac 2); |
|
2812 by (rotate_tac 2 2); |
|
2813 by (dtac (real_mult_assoc RS subst) 2); |
|
2814 by (rotate_tac 2 2); |
|
2815 by (ftac (real_mult_inv_left RS subst) 2); |
|
2816 by (assume_tac 2); |
|
2817 by (thin_tac "(1 - z) * (x + y) = x /(x + y) * (x + y)" 2); |
|
2818 by (thin_tac "1 - z = x /(x + y)" 2); |
|
2819 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc])); |
|
2820 by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2, |
|
2821 real_diff_mult_distrib])); |
|
2822 qed "lemma_divide_rearrange"; |
|
2823 |
|
2824 Goal "[| 0 < x * x + y * y; \ |
|
2825 \ 1 - sin xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2 \ |
|
2826 \ |] ==> sin xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2"; |
|
2827 by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset() |
|
2828 addsimps [realpow_divide,real_sqrt_gt_zero_pow2, |
|
2829 realpow_two_eq_mult RS sym])); |
|
2830 qed "lemma_cos_sin_eq"; |
|
2831 |
|
2832 Goal "[| 0 < x * x + y * y; \ |
|
2833 \ 1 - cos xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2 \ |
|
2834 \ |] ==> cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2"; |
|
2835 by (auto_tac (claset(),simpset() addsimps [realpow_divide, |
|
2836 real_sqrt_gt_zero_pow2,realpow_two_eq_mult RS sym])); |
|
2837 by (rtac (real_add_commute RS subst) 1); |
|
2838 by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset())); |
|
2839 qed "lemma_sin_cos_eq"; |
|
2840 |
|
2841 Goal "[| x ~= 0; \ |
|
2842 \ cos xa = x / sqrt (x * x + y * y) \ |
|
2843 \ |] ==> sin xa = y / sqrt (x * x + y * y) | \ |
|
2844 \ sin xa = - y / sqrt (x * x + y * y)"; |
|
2845 by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1); |
|
2846 by (forw_inst_tac [("y","y")] real_sum_square_gt_zero 1); |
|
2847 by (asm_full_simp_tac (simpset() addsimps [cos_squared_eq]) 1); |
|
2848 by (subgoal_tac "sin xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2" 1); |
|
2849 by (rtac lemma_cos_sin_eq 2); |
|
2850 by (Force_tac 2); |
|
2851 by (Asm_full_simp_tac 2); |
|
2852 by (auto_tac (claset(),simpset() addsimps [realpow_two_disj,realpow_num_two] |
|
2853 delsimps [realpow_Suc])); |
|
2854 qed "sin_x_y_disj"; |
|
2855 |
|
2856 (* |
|
2857 Goal "(x / sqrt (x * x + y * y)) ^ 2 = (x * x) / (x * x + y * y)"; |
|
2858 by Auto_tac; |
|
2859 val lemma = result(); |
|
2860 Addsimps [lemma]; |
|
2861 |
|
2862 Goal "(x / sqrt (x * x + y * y)) * (x / sqrt (x * x + y * y)) = \ |
|
2863 \ (x * x) / (x * x + y * y)"; |
|
2864 val lemma_too = result(); |
|
2865 Addsimps [lemma_too]; |
|
2866 *) |
|
2867 |
|
2868 Goal "y ~= 0 ==> x / sqrt (x * x + y * y) ~= -(1::real)"; |
|
2869 by Auto_tac; |
|
2870 by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1); |
|
2871 by (auto_tac (claset(),simpset() addsimps [realpow_divide, |
|
2872 realpow_two_eq_mult RS sym])); |
|
2873 by (forw_inst_tac [("x","x")] real_sum_squares_not_zero2 1); |
|
2874 by (asm_full_simp_tac (HOL_ss addsimps [realpow_two_eq_mult RS sym]) 1); |
|
2875 by (forw_inst_tac [("c1","x ^ 2 + y ^ 2")] |
|
2876 (real_mult_right_cancel RS iffD2) 1); |
|
2877 by (assume_tac 1); |
|
2878 by (dres_inst_tac [("y","x ^ 2 + y ^ 2"),("x","x ^ 2")] |
|
2879 (CLAIM "y ~= (0::real) ==> (x/y) * y= x") 1); |
|
2880 by Auto_tac; |
|
2881 qed "cos_not_eq_minus_one"; |
|
2882 |
|
2883 Goalw [arcos_def] |
|
2884 "arcos (x / sqrt (x * x + y * y)) = pi ==> y = 0"; |
|
2885 by (rtac ccontr 1); |
|
2886 by (rtac swap 1 THEN assume_tac 2); |
|
2887 by (rtac (([cos_x_y_ge_minus_one,cos_x_y_le_one] MRS cos_total) RS |
|
2888 ((CLAIM "EX! x. P x ==> EX x. P x") RS someI2_ex)) 1); |
|
2889 by (auto_tac (claset() addDs [cos_not_eq_minus_one],simpset())); |
|
2890 qed "arcos_eq_pi_cancel"; |
|
2891 |
|
2892 Goalw [real_divide_def] "x ~= 0 ==> x / sqrt (x * x + y * y) ~= 0"; |
|
2893 by (forw_inst_tac [("y3","y")] (real_sqrt_sum_squares_gt_zero3 |
|
2894 RS real_not_refl2 RS not_sym RS real_inverse_not_zero) 1); |
|
2895 by (auto_tac (claset(),simpset() addsimps [realpow_two_eq_mult])); |
|
2896 qed "lemma_cos_not_eq_zero"; |
|
2897 |
|
2898 Goal "[| x ~= 0; \ |
|
2899 \ sin xa = y / sqrt (x * x + y * y) \ |
|
2900 \ |] ==> cos xa = x / sqrt (x * x + y * y) | \ |
|
2901 \ cos xa = - x / sqrt (x * x + y * y)"; |
|
2902 by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1); |
|
2903 by (forw_inst_tac [("y","y")] real_sum_square_gt_zero 1); |
|
2904 by (asm_full_simp_tac (simpset() addsimps [sin_squared_eq] |
|
2905 delsimps [realpow_Suc]) 1); |
|
2906 by (subgoal_tac "cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2" 1); |
|
2907 by (rtac lemma_sin_cos_eq 2); |
|
2908 by (Force_tac 2); |
|
2909 by (Asm_full_simp_tac 2); |
|
2910 by (auto_tac (claset(),simpset() addsimps [realpow_two_disj, |
|
2911 realpow_num_two] delsimps [realpow_Suc])); |
|
2912 qed "cos_x_y_disj"; |
|
2913 |
|
2914 Goal "0 < y ==> - y / sqrt (x * x + y * y) < 0"; |
|
2915 by (case_tac "x = 0" 1); |
|
2916 by (auto_tac (claset(),simpset() addsimps [abs_eqI2])); |
|
2917 by (dres_inst_tac [("y","y")] real_sqrt_sum_squares_gt_zero3 1); |
|
2918 by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff, |
|
2919 real_divide_def,realpow_two_eq_mult])); |
|
2920 qed "real_sqrt_divide_less_zero"; |
|
2921 |
|
2922 Goal "[| x ~= 0; 0 < y |] ==> EX r a. x = r * cos a & y = r * sin a"; |
|
2923 by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1); |
|
2924 by (res_inst_tac [("x","arcos(x / sqrt (x * x + y * y))")] exI 1); |
|
2925 by Auto_tac; |
|
2926 by (dres_inst_tac [("y2","y")] (real_sqrt_sum_squares_gt_zero3 |
|
2927 RS real_not_refl2 RS not_sym) 1); |
|
2928 by (auto_tac (claset(),simpset() addsimps [realpow_two_eq_mult])); |
|
2929 by (rewtac arcos_def); |
|
2930 by (cut_inst_tac [("x1","x"),("y1","y")] ([cos_x_y_ge_minus_one,cos_x_y_le_one] |
|
2931 MRS cos_total) 1); |
|
2932 by (rtac someI2_ex 1 THEN Blast_tac 1); |
|
2933 by (thin_tac |
|
2934 "EX! xa. 0 <= xa & xa <= pi & cos xa = x / sqrt (x * x + y * y)" 1); |
|
2935 by (ftac sin_x_y_disj 1 THEN Blast_tac 1); |
|
2936 by (dres_inst_tac [("y2","y")] (real_sqrt_sum_squares_gt_zero3 |
|
2937 RS real_not_refl2 RS not_sym) 1); |
|
2938 by (auto_tac (claset(),simpset() addsimps [realpow_two_eq_mult])); |
|
2939 by (dtac sin_ge_zero 1 THEN assume_tac 1); |
|
2940 by (dres_inst_tac [("x","x")] real_sqrt_divide_less_zero 1 THEN Auto_tac); |
|
2941 qed "polar_ex1"; |
|
2942 |
|
2943 Goal "x * x = -(y * y) ==> y = (0::real)"; |
|
2944 by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset())); |
|
2945 qed "real_sum_squares_cancel2a"; |
|
2946 |
|
2947 Goal "[| x ~= 0; y < 0 |] ==> EX r a. x = r * cos a & y = r * sin a"; |
|
2948 by (cut_inst_tac [("R1.0","0"),("R2.0","x")] real_linear 1); |
|
2949 by Auto_tac; |
|
2950 by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1); |
|
2951 by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1); |
|
2952 by (auto_tac (claset() addDs [real_sum_squares_cancel2a], |
|
2953 simpset() addsimps [realpow_two_eq_mult])); |
|
2954 by (rewtac arcsin_def); |
|
2955 by (cut_inst_tac [("x1","x"),("y1","y")] ([cos_x_y_ge_minus_one1a, |
|
2956 cos_x_y_le_one2] MRS sin_total) 1); |
|
2957 by (rtac someI2_ex 1 THEN Blast_tac 1); |
|
2958 by (thin_tac "EX! xa. - (pi/2) <= xa & \ |
|
2959 \ xa <= pi/2 & sin xa = y / sqrt (x * x + y * y)" 1); |
|
2960 by (ftac ((CLAIM "0 < x ==> (x::real) ~= 0") RS cos_x_y_disj) 1 THEN Blast_tac 1); |
|
2961 by Auto_tac; |
|
2962 by (dtac cos_ge_zero 1 THEN Force_tac 1); |
|
2963 by (dres_inst_tac [("x","y")] real_sqrt_divide_less_zero 1); |
|
2964 by (auto_tac (claset(),simpset() addsimps [real_add_commute])); |
|
2965 by (dtac (ARITH_PROVE "(y::real) < 0 ==> 0 < - y") 1); |
|
2966 by (dtac (CLAIM "x < (0::real) ==> x ~= 0" RS polar_ex1) 1 THEN assume_tac 1); |
|
2967 by (REPEAT(etac exE 1)); |
|
2968 by (res_inst_tac [("x","r")] exI 1); |
|
2969 by (res_inst_tac [("x","-a")] exI 1); |
|
2970 by Auto_tac; |
|
2971 qed "polar_ex2"; |
|
2972 |
|
2973 Goal "EX r a. x = r * cos a & y = r * sin a"; |
|
2974 by (case_tac "x = 0" 1); |
|
2975 by Auto_tac; |
|
2976 by (res_inst_tac [("x","y")] exI 1); |
|
2977 by (res_inst_tac [("x","pi/2")] exI 1 THEN Auto_tac); |
|
2978 by (cut_inst_tac [("R1.0","0"),("R2.0","y")] real_linear 1); |
|
2979 by Auto_tac; |
|
2980 by (res_inst_tac [("x","x")] exI 2); |
|
2981 by (res_inst_tac [("x","0")] exI 2 THEN Auto_tac); |
|
2982 by (ALLGOALS(blast_tac (claset() addIs [polar_ex1,polar_ex2]))); |
|
2983 qed "polar_Ex"; |
|
2984 |
|
2985 Goal "abs x <= sqrt (x ^ 2 + y ^ 2)"; |
|
2986 by (res_inst_tac [("n","1")] realpow_increasing 1); |
|
2987 by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc RS sym])); |
|
2988 by (simp_tac (simpset() addsimps [two_eq_Suc_Suc]) 1); |
|
2989 qed "real_sqrt_ge_abs1"; |
|
2990 |
|
2991 Goal "abs y <= sqrt (x ^ 2 + y ^ 2)"; |
|
2992 by (rtac (real_add_commute RS subst) 1); |
|
2993 by (rtac real_sqrt_ge_abs1 1); |
|
2994 qed "real_sqrt_ge_abs2"; |
|
2995 Addsimps [real_sqrt_ge_abs1,real_sqrt_ge_abs2]; |
|
2996 |
|
2997 Goal "0 < sqrt 2"; |
|
2998 by (auto_tac (claset() addIs [real_sqrt_gt_zero],simpset())); |
|
2999 qed "real_sqrt_two_gt_zero"; |
|
3000 Addsimps [real_sqrt_two_gt_zero]; |
|
3001 |
|
3002 Goal "0 <= sqrt 2"; |
|
3003 by (auto_tac (claset() addIs [real_sqrt_ge_zero],simpset())); |
|
3004 qed "real_sqrt_two_ge_zero"; |
|
3005 Addsimps [real_sqrt_two_ge_zero]; |
|
3006 |
|
3007 Goal "1 < sqrt 2"; |
|
3008 by (res_inst_tac [("y","7/5")] order_less_le_trans 1); |
|
3009 by (res_inst_tac [("n","1")] realpow_increasing 2); |
|
3010 by (auto_tac (claset(),simpset() addsimps [real_sqrt_gt_zero_pow2,two_eq_Suc_Suc RS sym] |
|
3011 delsimps [realpow_Suc])); |
|
3012 by (simp_tac (simpset() addsimps [two_eq_Suc_Suc]) 1); |
|
3013 qed "real_sqrt_two_gt_one"; |
|
3014 Addsimps [real_sqrt_two_gt_one]; |
|
3015 |
|
3016 Goal "0 < u ==> u / sqrt 2 < u"; |
|
3017 by (res_inst_tac [("z1","inverse u")] (real_mult_less_iff1 RS iffD1) 1); |
|
3018 by Auto_tac; |
|
3019 by (res_inst_tac [("z1","sqrt 2")] (real_mult_less_iff1 RS iffD1) 1); |
|
3020 by Auto_tac; |
|
3021 qed "lemma_real_divide_sqrt_less"; |
|
3022 |
|
3023 (* needed for infinitely close relation over the nonstandard complex numbers *) |
|
3024 Goal "[| 0 < u; x < u/2; y < u/2; 0 <= x; 0 <= y |] ==> sqrt (x ^ 2 + y ^ 2) < u"; |
|
3025 by (res_inst_tac [("y","u/sqrt 2")] order_le_less_trans 1); |
|
3026 by (etac lemma_real_divide_sqrt_less 2); |
|
3027 by (res_inst_tac [("n","1")] realpow_increasing 1); |
|
3028 by (auto_tac (claset(),simpset() addsimps [real_0_le_divide_iff,realpow_divide, |
|
3029 real_sqrt_gt_zero_pow2,two_eq_Suc_Suc RS sym] delsimps [realpow_Suc])); |
|
3030 by (res_inst_tac [("t","u ^ 2")] (real_sum_of_halves RS subst) 1); |
|
3031 by (rtac real_add_le_mono 1); |
|
3032 by (auto_tac (claset(),simpset() delsimps [realpow_Suc])); |
|
3033 by (ALLGOALS(rtac ((CLAIM "(2::real) ^ 2 = 4") RS subst))); |
|
3034 by (ALLGOALS(rtac (realpow_mult RS subst))); |
|
3035 by (ALLGOALS(rtac realpow_le)); |
|
3036 by Auto_tac; |
|
3037 qed "lemma_sqrt_hcomplex_capprox"; |
|
3038 |
|
3039 Addsimps [real_sqrt_sum_squares_ge_zero RS abs_eqI1]; |
|
3040 |
|
3041 (* A few theorems involving ln and derivatives, etc *) |
|
3042 |
|
3043 Goal "DERIV ln z :> l ==> DERIV (%x. exp (ln x)) z :> exp (ln z) * l"; |
|
3044 by (etac DERIV_fun_exp 1); |
|
3045 qed "lemma_DERIV_ln"; |
|
3046 |
|
3047 Goal "0 < z ==> ( *f* (%x. exp (ln x))) z = z"; |
|
3048 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
3049 by (auto_tac (claset(),simpset() addsimps [starfun, |
|
3050 hypreal_zero_def,hypreal_less])); |
|
3051 qed "STAR_exp_ln"; |
|
3052 |
|
3053 Goal "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e"; |
|
3054 by (res_inst_tac [("z1","-e")] (hypreal_add_right_cancel_less RS iffD1) 1); |
|
3055 by (auto_tac (claset() addIs [Infinitesimal_less_SReal],simpset())); |
|
3056 qed "hypreal_add_Infinitesimal_gt_zero"; |
|
3057 |
|
3058 Goalw [nsderiv_def,NSLIM_def] "0 < z ==> NSDERIV (%x. exp (ln x)) z :> 1"; |
|
3059 by Auto_tac; |
|
3060 by (rtac ccontr 1); |
|
3061 by (subgoal_tac "0 < hypreal_of_real z + h" 1); |
|
3062 by (dtac STAR_exp_ln 1); |
|
3063 by (rtac hypreal_add_Infinitesimal_gt_zero 2); |
|
3064 by (dtac (CLAIM "h ~= 0 ==> h/h = (1::hypreal)") 1); |
|
3065 by (auto_tac (claset(),simpset() addsimps [exp_ln_iff RS sym] |
|
3066 delsimps [exp_ln_iff])); |
|
3067 qed "NSDERIV_exp_ln_one"; |
|
3068 |
|
3069 Goal "0 < z ==> DERIV (%x. exp (ln x)) z :> 1"; |
|
3070 by (auto_tac (claset() addIs [NSDERIV_exp_ln_one], |
|
3071 simpset() addsimps [NSDERIV_DERIV_iff RS sym])); |
|
3072 qed "DERIV_exp_ln_one"; |
|
3073 |
|
3074 Goal "[| 0 < z; DERIV ln z :> l |] ==> exp (ln z) * l = 1"; |
|
3075 by (rtac DERIV_unique 1); |
|
3076 by (rtac lemma_DERIV_ln 1); |
|
3077 by (rtac DERIV_exp_ln_one 2); |
|
3078 by Auto_tac; |
|
3079 qed "lemma_DERIV_ln2"; |
|
3080 |
|
3081 Goal "[| 0 < z; DERIV ln z :> l |] ==> l = 1/(exp (ln z))"; |
|
3082 by (res_inst_tac [("c1","exp(ln z)")] (real_mult_left_cancel RS iffD1) 1); |
|
3083 by (auto_tac (claset() addIs [lemma_DERIV_ln2],simpset())); |
|
3084 qed "lemma_DERIV_ln3"; |
|
3085 |
|
3086 Goal "[| 0 < z; DERIV ln z :> l |] ==> l = 1/z"; |
|
3087 by (res_inst_tac [("t","z")] (exp_ln_iff RS iffD2 RS subst) 1); |
|
3088 by (auto_tac (claset() addIs [lemma_DERIV_ln3],simpset())); |
|
3089 qed "lemma_DERIV_ln4"; |
|
3090 |
|
3091 (* need to rename second isCont_inverse *) |
|
3092 |
|
3093 Goal "[| 0 < d; ALL z. abs(z - x) <= d --> g(f(z)) = z; \ |
|
3094 \ ALL z. abs(z - x) <= d --> isCont f z |] \ |
|
3095 \ ==> isCont g (f x)"; |
|
3096 by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1); |
|
3097 by (Step_tac 1); |
|
3098 by (dres_inst_tac [("d1.0","r")] real_lbound_gt_zero 1); |
|
3099 by (assume_tac 1 THEN Step_tac 1); |
|
3100 by (subgoal_tac "ALL z. abs(z - x) <= e --> (g(f z) = z)" 1); |
|
3101 by (Force_tac 2); |
|
3102 by (subgoal_tac "ALL z. abs(z - x) <= e --> isCont f z" 1); |
|
3103 by (Force_tac 2); |
|
3104 by (dres_inst_tac [("d","e")] isCont_inj_range 1); |
|
3105 by (assume_tac 2 THEN assume_tac 1); |
|
3106 by (Step_tac 1); |
|
3107 by (res_inst_tac [("x","ea")] exI 1); |
|
3108 by Auto_tac; |
|
3109 by (rotate_tac 4 1); |
|
3110 by (dres_inst_tac [("x","f(x) + xa")] spec 1); |
|
3111 by Auto_tac; |
|
3112 by (dtac sym 1 THEN Auto_tac); |
|
3113 by (arith_tac 1); |
|
3114 qed "isCont_inv_fun"; |
|
3115 |
|
3116 (* |
|
3117 Goalw [isCont_def] |
|
3118 "[| isCont f x; f x ~= 0 |] ==> isCont (%x. inverse (f x)) x"; |
|
3119 by (blast_tac (claset() addIs [LIM_inverse]) 1); |
|
3120 qed "isCont_inverse"; |
|
3121 *) |
|
3122 |
|
3123 |
|
3124 Goal "[| 0 < d; \ |
|
3125 \ ALL z. abs(z - x) <= d --> g(f(z)) = z; \ |
|
3126 \ ALL z. abs(z - x) <= d --> isCont f z |] \ |
|
3127 \ ==> EX e. 0 < (e::real) & \ |
|
3128 \ (ALL y. 0 < abs(y - f(x::real)) & abs(y - f(x)) < e --> f(g(y)) = y)"; |
|
3129 by (dtac isCont_inj_range 1); |
|
3130 by (assume_tac 2 THEN assume_tac 1); |
|
3131 by Auto_tac; |
|
3132 by (res_inst_tac [("x","e")] exI 1 THEN Auto_tac); |
|
3133 by (rotate_tac 2 1); |
|
3134 by (dres_inst_tac [("x","y")] spec 1 THEN Auto_tac); |
|
3135 qed "isCont_inv_fun_inv"; |
|
3136 |
|
3137 |
|
3138 (* Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*) |
|
3139 Goal "[| f -- c --> l; 0 < l |] \ |
|
3140 \ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> 0 < f x)"; |
|
3141 by (auto_tac (claset(),simpset() addsimps [LIM_def])); |
|
3142 by (dres_inst_tac [("x","l/2")] spec 1); |
|
3143 by (Step_tac 1); |
|
3144 by (Force_tac 1); |
|
3145 by (res_inst_tac [("x","s")] exI 1); |
|
3146 by (Step_tac 1); |
|
3147 by (rotate_tac 2 1); |
|
3148 by (dres_inst_tac [("x","x")] spec 1); |
|
3149 by (auto_tac (claset(),HOL_ss addsimps [abs_interval_iff])); |
|
3150 by (auto_tac (claset(),simpset() addsimps [CLAIM "(l::real) + -(l/2) = l/2", |
|
3151 CLAIM "(a < f + - l) = (l + a < (f::real))"])); |
|
3152 qed "LIM_fun_gt_zero"; |
|
3153 |
|
3154 Goal "[| f -- c --> l; l < 0 |] \ |
|
3155 \ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x < 0)"; |
|
3156 by (auto_tac (claset(),simpset() addsimps [LIM_def])); |
|
3157 by (dres_inst_tac [("x","-l/2")] spec 1); |
|
3158 by (Step_tac 1); |
|
3159 by (Force_tac 1); |
|
3160 by (res_inst_tac [("x","s")] exI 1); |
|
3161 by (Step_tac 1); |
|
3162 by (rotate_tac 2 1); |
|
3163 by (dres_inst_tac [("x","x")] spec 1); |
|
3164 by (auto_tac (claset(),HOL_ss addsimps [abs_interval_iff])); |
|
3165 by (auto_tac (claset(),simpset() addsimps [CLAIM "(l::real) + -(l/2) = l/2", |
|
3166 CLAIM "(f + - l < a) = ((f::real) < l + a)"])); |
|
3167 qed "LIM_fun_less_zero"; |
|
3168 |
|
3169 |
|
3170 Goal "[| f -- c --> l; l ~= 0 |] \ |
|
3171 \ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x ~= 0)"; |
|
3172 by (cut_inst_tac [("R1.0","l"),("R2.0","0")] real_linear 1); |
|
3173 by Auto_tac; |
|
3174 by (dtac LIM_fun_less_zero 1); |
|
3175 by (dtac LIM_fun_gt_zero 3); |
|
3176 by Auto_tac; |
|
3177 by (ALLGOALS(res_inst_tac [("x","r")] exI)); |
|
3178 by Auto_tac; |
|
3179 qed "LIM_fun_not_zero"; |