144 qed "real_sqrt_pow_abs"; |
144 qed "real_sqrt_pow_abs"; |
145 |
145 |
146 Goal "(~ (0::real) < x*x) = (x = 0)"; |
146 Goal "(~ (0::real) < x*x) = (x = 0)"; |
147 by Auto_tac; |
147 by Auto_tac; |
148 by (rtac ccontr 1); |
148 by (rtac ccontr 1); |
149 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
149 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
150 by Auto_tac; |
150 by Auto_tac; |
151 by (ftac (real_mult_order) 2); |
151 by (ftac (real_mult_order) 2); |
152 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 1); |
152 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 1); |
153 by Auto_tac; |
153 by Auto_tac; |
154 qed "not_real_square_gt_zero"; |
154 qed "not_real_square_gt_zero"; |
1673 |
1673 |
1674 Goal "EX! x. 0 <= x & x <= 2 & cos x = 0"; |
1674 Goal "EX! x. 0 <= x & x <= 2 & cos x = 0"; |
1675 by (subgoal_tac "EX x. 0 <= x & x <= 2 & cos x = 0" 1); |
1675 by (subgoal_tac "EX x. 0 <= x & x <= 2 & cos x = 0" 1); |
1676 by (rtac IVT2 2); |
1676 by (rtac IVT2 2); |
1677 by (auto_tac (claset() addIs [DERIV_isCont,DERIV_cos],simpset ())); |
1677 by (auto_tac (claset() addIs [DERIV_isCont,DERIV_cos],simpset ())); |
1678 by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1); |
1678 by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1); |
1679 by (rtac ccontr 1); |
1679 by (rtac ccontr 1); |
1680 by (subgoal_tac "(ALL x. cos differentiable x) & \ |
1680 by (subgoal_tac "(ALL x. cos differentiable x) & \ |
1681 \ (ALL x. isCont cos x)" 1); |
1681 \ (ALL x. isCont cos x)" 1); |
1682 by (auto_tac (claset() addIs [DERIV_cos,DERIV_isCont],simpset() |
1682 by (auto_tac (claset() addIs [DERIV_cos,DERIV_isCont],simpset() |
1683 addsimps [differentiable_def])); |
1683 addsimps [differentiable_def])); |
1896 Goal "[| - 1 <= y; y <= 1 |] ==> EX! x. 0 <= x & x <= pi & (cos x = y)"; |
1896 Goal "[| - 1 <= y; y <= 1 |] ==> EX! x. 0 <= x & x <= pi & (cos x = y)"; |
1897 by (subgoal_tac "EX x. 0 <= x & x <= pi & cos x = y" 1); |
1897 by (subgoal_tac "EX x. 0 <= x & x <= pi & cos x = y" 1); |
1898 by (rtac IVT2 2); |
1898 by (rtac IVT2 2); |
1899 by (auto_tac (claset() addIs [order_less_imp_le,DERIV_isCont,DERIV_cos], |
1899 by (auto_tac (claset() addIs [order_less_imp_le,DERIV_isCont,DERIV_cos], |
1900 simpset ())); |
1900 simpset ())); |
1901 by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1); |
1901 by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1); |
1902 by (rtac ccontr 1 THEN Auto_tac); |
1902 by (rtac ccontr 1 THEN Auto_tac); |
1903 by (dres_inst_tac [("f","cos")] Rolle 1); |
1903 by (dres_inst_tac [("f","cos")] Rolle 1); |
1904 by (dres_inst_tac [("f","cos")] Rolle 5); |
1904 by (dres_inst_tac [("f","cos")] Rolle 5); |
1905 by (auto_tac (claset() addIs [order_less_imp_le,DERIV_isCont,DERIV_cos] |
1905 by (auto_tac (claset() addIs [order_less_imp_le,DERIV_isCont,DERIV_cos] |
1906 addSDs [DERIV_cos RS DERIV_unique],simpset() addsimps [differentiable_def])); |
1906 addSDs [DERIV_cos RS DERIV_unique],simpset() addsimps [differentiable_def])); |
2169 qed "lemma_tan_total1"; |
2169 qed "lemma_tan_total1"; |
2170 |
2170 |
2171 Goal "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"; |
2171 Goal "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"; |
2172 by (cut_inst_tac [("y","y")] lemma_tan_total1 1); |
2172 by (cut_inst_tac [("y","y")] lemma_tan_total1 1); |
2173 by (Auto_tac); |
2173 by (Auto_tac); |
2174 by (cut_inst_tac [("R1.0","xa"),("R2.0","y")] real_linear 1); |
2174 by (cut_inst_tac [("x","xa"),("y","y")] linorder_less_linear 1); |
2175 by (Auto_tac); |
2175 by (Auto_tac); |
2176 by (subgoal_tac "EX z. xa < z & z < y & DERIV tan z :> 0" 1); |
2176 by (subgoal_tac "EX z. xa < z & z < y & DERIV tan z :> 0" 1); |
2177 by (subgoal_tac "EX z. y < z & z < xa & DERIV tan z :> 0" 3); |
2177 by (subgoal_tac "EX z. y < z & z < xa & DERIV tan z :> 0" 3); |
2178 by (rtac Rolle 2); |
2178 by (rtac Rolle 2); |
2179 by (rtac Rolle 7); |
2179 by (rtac Rolle 7); |
2626 by Auto_tac; |
2626 by Auto_tac; |
2627 qed "real_sqrt_sos_eq_one_iff"; |
2627 qed "real_sqrt_sos_eq_one_iff"; |
2628 Addsimps [real_sqrt_sos_eq_one_iff]; |
2628 Addsimps [real_sqrt_sos_eq_one_iff]; |
2629 |
2629 |
2630 Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r"; |
2630 Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r"; |
2631 by (real_div_undefined_case_tac "r=0" 1); |
2631 by (case_tac "r=0" 1); |
2632 by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac)); |
2632 by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac)); |
2633 qed "real_divide_square_eq"; |
2633 qed "real_divide_square_eq"; |
2634 Addsimps [real_divide_square_eq]; |
2634 Addsimps [real_divide_square_eq]; |
2635 |
2635 |
2636 (*-------------------------------------------------------------------------------*) |
2636 (*-------------------------------------------------------------------------------*) |
2673 by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1); |
2673 by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1); |
2674 by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); |
2674 by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff])); |
2675 qed "real_sqrt_sum_squares_gt_zero2"; |
2675 qed "real_sqrt_sum_squares_gt_zero2"; |
2676 |
2676 |
2677 Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; |
2677 Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; |
2678 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
2678 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
2679 by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero2, |
2679 by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero2, |
2680 real_sqrt_sum_squares_gt_zero1],simpset() addsimps [realpow_num_two])); |
2680 real_sqrt_sum_squares_gt_zero1],simpset() addsimps [realpow_num_two])); |
2681 qed "real_sqrt_sum_squares_gt_zero3"; |
2681 qed "real_sqrt_sum_squares_gt_zero3"; |
2682 |
2682 |
2683 Goal "y ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; |
2683 Goal "y ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)"; |
2739 by Auto_tac; |
2739 by Auto_tac; |
2740 qed "lemma_real_divide_sqrt_le_one2"; |
2740 qed "lemma_real_divide_sqrt_le_one2"; |
2741 (* was qed "lemma_real_mult_self_rinv_sqrt_squared5" *) |
2741 (* was qed "lemma_real_mult_self_rinv_sqrt_squared5" *) |
2742 |
2742 |
2743 Goal "-(1::real)<= x / sqrt (x * x + y * y)"; |
2743 Goal "-(1::real)<= x / sqrt (x * x + y * y)"; |
2744 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
2744 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
2745 by (Step_tac 1); |
2745 by (Step_tac 1); |
2746 by (rtac lemma_real_divide_sqrt_ge_minus_one2 1); |
2746 by (rtac lemma_real_divide_sqrt_ge_minus_one2 1); |
2747 by (rtac lemma_real_divide_sqrt_ge_minus_one 3); |
2747 by (rtac lemma_real_divide_sqrt_ge_minus_one 3); |
2748 by Auto_tac; |
2748 by Auto_tac; |
2749 qed "cos_x_y_ge_minus_one"; |
2749 qed "cos_x_y_ge_minus_one"; |
2755 qed "cos_x_y_ge_minus_one1a"; |
2755 qed "cos_x_y_ge_minus_one1a"; |
2756 Addsimps [cos_x_y_ge_minus_one1a, |
2756 Addsimps [cos_x_y_ge_minus_one1a, |
2757 simplify (simpset()) cos_x_y_ge_minus_one1a]; |
2757 simplify (simpset()) cos_x_y_ge_minus_one1a]; |
2758 |
2758 |
2759 Goal "x / sqrt (x * x + y * y) <= 1"; |
2759 Goal "x / sqrt (x * x + y * y) <= 1"; |
2760 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
2760 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
2761 by (Step_tac 1); |
2761 by (Step_tac 1); |
2762 by (rtac lemma_real_divide_sqrt_le_one 1); |
2762 by (rtac lemma_real_divide_sqrt_le_one 1); |
2763 by (rtac lemma_real_divide_sqrt_le_one2 3); |
2763 by (rtac lemma_real_divide_sqrt_le_one2 3); |
2764 by Auto_tac; |
2764 by Auto_tac; |
2765 qed "cos_x_y_le_one"; |
2765 qed "cos_x_y_le_one"; |
2776 |
2776 |
2777 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS cos_arcos]; |
2777 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS cos_arcos]; |
2778 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS arcos_bounded]; |
2778 Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS arcos_bounded]; |
2779 |
2779 |
2780 Goal "-(1::real) <= abs(x) / sqrt (x * x + y * y)"; |
2780 Goal "-(1::real) <= abs(x) / sqrt (x * x + y * y)"; |
2781 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
2781 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
2782 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
2782 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
2783 by (dtac lemma_real_divide_sqrt_ge_minus_one 1 THEN Force_tac 1); |
2783 by (dtac lemma_real_divide_sqrt_ge_minus_one 1 THEN Force_tac 1); |
2784 qed "cos_rabs_x_y_ge_minus_one"; |
2784 qed "cos_rabs_x_y_ge_minus_one"; |
2785 |
2785 |
2786 Addsimps [cos_rabs_x_y_ge_minus_one, |
2786 Addsimps [cos_rabs_x_y_ge_minus_one, |
2787 simplify (simpset()) cos_rabs_x_y_ge_minus_one]; |
2787 simplify (simpset()) cos_rabs_x_y_ge_minus_one]; |
2788 |
2788 |
2789 Goal "abs(x) / sqrt (x * x + y * y) <= 1"; |
2789 Goal "abs(x) / sqrt (x * x + y * y) <= 1"; |
2790 by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1); |
2790 by (cut_inst_tac [("x","x"),("y","0")] linorder_less_linear 1); |
2791 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
2791 by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2])); |
2792 by (dtac lemma_real_divide_sqrt_ge_minus_one2 1 THEN Force_tac 1); |
2792 by (dtac lemma_real_divide_sqrt_ge_minus_one2 1 THEN Force_tac 1); |
2793 qed "cos_rabs_x_y_le_one"; |
2793 qed "cos_rabs_x_y_le_one"; |
2794 Addsimps [cos_rabs_x_y_le_one]; |
2794 Addsimps [cos_rabs_x_y_le_one]; |
2795 |
2795 |
2950 Goal "x * x = -(y * y) ==> y = (0::real)"; |
2950 Goal "x * x = -(y * y) ==> y = (0::real)"; |
2951 by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset())); |
2951 by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset())); |
2952 qed "real_sum_squares_cancel2a"; |
2952 qed "real_sum_squares_cancel2a"; |
2953 |
2953 |
2954 Goal "[| x ~= 0; y < 0 |] ==> EX r a. x = r * cos a & y = r * sin a"; |
2954 Goal "[| x ~= 0; y < 0 |] ==> EX r a. x = r * cos a & y = r * sin a"; |
2955 by (cut_inst_tac [("R1.0","0"),("R2.0","x")] real_linear 1); |
2955 by (cut_inst_tac [("x","0"),("y","x")] linorder_less_linear 1); |
2956 by Auto_tac; |
2956 by Auto_tac; |
2957 by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1); |
2957 by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1); |
2958 by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1); |
2958 by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1); |
2959 by (auto_tac (claset() addDs [real_sum_squares_cancel2a], |
2959 by (auto_tac (claset() addDs [real_sum_squares_cancel2a], |
2960 simpset() addsimps [realpow_two_eq_mult])); |
2960 simpset() addsimps [realpow_two_eq_mult])); |
2980 Goal "EX r a. x = r * cos a & y = r * sin a"; |
2980 Goal "EX r a. x = r * cos a & y = r * sin a"; |
2981 by (case_tac "x = 0" 1); |
2981 by (case_tac "x = 0" 1); |
2982 by Auto_tac; |
2982 by Auto_tac; |
2983 by (res_inst_tac [("x","y")] exI 1); |
2983 by (res_inst_tac [("x","y")] exI 1); |
2984 by (res_inst_tac [("x","pi/2")] exI 1 THEN Auto_tac); |
2984 by (res_inst_tac [("x","pi/2")] exI 1 THEN Auto_tac); |
2985 by (cut_inst_tac [("R1.0","0"),("R2.0","y")] real_linear 1); |
2985 by (cut_inst_tac [("x","0"),("y","y")] linorder_less_linear 1); |
2986 by Auto_tac; |
2986 by Auto_tac; |
2987 by (res_inst_tac [("x","x")] exI 2); |
2987 by (res_inst_tac [("x","x")] exI 2); |
2988 by (res_inst_tac [("x","0")] exI 2 THEN Auto_tac); |
2988 by (res_inst_tac [("x","0")] exI 2 THEN Auto_tac); |
2989 by (ALLGOALS(blast_tac (claset() addIs [polar_ex1,polar_ex2]))); |
2989 by (ALLGOALS(blast_tac (claset() addIs [polar_ex1,polar_ex2]))); |
2990 qed "polar_Ex"; |
2990 qed "polar_Ex"; |
3174 qed "LIM_fun_less_zero"; |
3174 qed "LIM_fun_less_zero"; |
3175 |
3175 |
3176 |
3176 |
3177 Goal "[| f -- c --> l; l ~= 0 |] \ |
3177 Goal "[| f -- c --> l; l ~= 0 |] \ |
3178 \ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x ~= 0)"; |
3178 \ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x ~= 0)"; |
3179 by (cut_inst_tac [("R1.0","l"),("R2.0","0")] real_linear 1); |
3179 by (cut_inst_tac [("x","l"),("y","0")] linorder_less_linear 1); |
3180 by Auto_tac; |
3180 by Auto_tac; |
3181 by (dtac LIM_fun_less_zero 1); |
3181 by (dtac LIM_fun_less_zero 1); |
3182 by (dtac LIM_fun_gt_zero 3); |
3182 by (dtac LIM_fun_gt_zero 3); |
3183 by Auto_tac; |
3183 by Auto_tac; |
3184 by (ALLGOALS(res_inst_tac [("x","r")] exI)); |
3184 by (ALLGOALS(res_inst_tac [("x","r")] exI)); |