27 LIM_add |
27 LIM_add |
28 ---------------*) |
28 ---------------*) |
29 Goalw [LIM_def] |
29 Goalw [LIM_def] |
30 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
30 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"; |
31 by (Clarify_tac 1); |
31 by (Clarify_tac 1); |
32 by (REPEAT(dres_inst_tac [("x","r/# 2")] spec 1)); |
32 by (REPEAT(dres_inst_tac [("x","r/2")] spec 1)); |
33 by (Asm_full_simp_tac 1); |
33 by (Asm_full_simp_tac 1); |
34 by (Clarify_tac 1); |
34 by (Clarify_tac 1); |
35 by (res_inst_tac [("R1.0","s"),("R2.0","sa")] |
35 by (res_inst_tac [("R1.0","s"),("R2.0","sa")] |
36 real_linear_less2 1); |
36 real_linear_less2 1); |
37 by (res_inst_tac [("x","s")] exI 1); |
37 by (res_inst_tac [("x","s")] exI 1); |
1542 by (induct_tac "n" 1); |
1542 by (induct_tac "n" 1); |
1543 by (auto_tac (claset(), |
1543 by (auto_tac (claset(), |
1544 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
1544 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def])); |
1545 qed "Bolzano_bisect_Suc_le_snd"; |
1545 qed "Bolzano_bisect_Suc_le_snd"; |
1546 |
1546 |
1547 Goal "((x::real) = y / (# 2 * z)) = (# 2 * x = y/z)"; |
1547 Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)"; |
1548 by Auto_tac; |
1548 by Auto_tac; |
1549 by (dres_inst_tac [("f","%u. (Numeral1/# 2)*u")] arg_cong 1); |
1549 by (dres_inst_tac [("f","%u. (Numeral1/2)*u")] arg_cong 1); |
1550 by Auto_tac; |
1550 by Auto_tac; |
1551 qed "eq_divide_2_times_iff"; |
1551 qed "eq_divide_2_times_iff"; |
1552 |
1552 |
1553 Goal "a \\<le> b ==> \ |
1553 Goal "a \\<le> b ==> \ |
1554 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \ |
1554 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \ |
1555 \ (b-a) / (# 2 ^ n)"; |
1555 \ (b-a) / (2 ^ n)"; |
1556 by (induct_tac "n" 1); |
1556 by (induct_tac "n" 1); |
1557 by (auto_tac (claset(), |
1557 by (auto_tac (claset(), |
1558 simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, |
1558 simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib, |
1559 Let_def, split_def])); |
1559 Let_def, split_def])); |
1560 by (auto_tac (claset(), |
1560 by (auto_tac (claset(), |
1602 by (dtac not_P_Bolzano_bisect' 1); |
1602 by (dtac not_P_Bolzano_bisect' 1); |
1603 by (REPEAT (assume_tac 1)); |
1603 by (REPEAT (assume_tac 1)); |
1604 by (rename_tac "l" 1); |
1604 by (rename_tac "l" 1); |
1605 by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1); |
1605 by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1); |
1606 by (rewtac LIMSEQ_def); |
1606 by (rewtac LIMSEQ_def); |
1607 by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1); |
1607 by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1); |
1608 by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1); |
1608 by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1); |
1609 by (dtac real_less_half_sum 1); |
1609 by (dtac real_less_half_sum 1); |
1610 by Safe_tac; |
1610 by Safe_tac; |
1611 (*linear arithmetic bug if we just use Asm_simp_tac*) |
1611 (*linear arithmetic bug if we just use Asm_simp_tac*) |
1612 by (ALLGOALS Asm_full_simp_tac); |
1612 by (ALLGOALS Asm_full_simp_tac); |
1613 by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1); |
1613 by (dres_inst_tac [("x","fst(Bolzano_bisect P a b (no + noa))")] spec 1); |
2146 by (res_inst_tac [("c1","b - a")] (real_mult_right_cancel RS iffD1) 1); |
2146 by (res_inst_tac [("c1","b - a")] (real_mult_right_cancel RS iffD1) 1); |
2147 by (auto_tac (claset() addSDs [DERIV_const_ratio_const], |
2147 by (auto_tac (claset() addSDs [DERIV_const_ratio_const], |
2148 simpset() addsimps [real_mult_assoc])); |
2148 simpset() addsimps [real_mult_assoc])); |
2149 qed "DERIV_const_ratio_const2"; |
2149 qed "DERIV_const_ratio_const2"; |
2150 |
2150 |
2151 Goal "((a + b) /# 2 - a) = (b - a)/(# 2::real)"; |
2151 Goal "((a + b) /2 - a) = (b - a)/(2::real)"; |
2152 by Auto_tac; |
2152 by Auto_tac; |
2153 qed "real_average_minus_first"; |
2153 qed "real_average_minus_first"; |
2154 Addsimps [real_average_minus_first]; |
2154 Addsimps [real_average_minus_first]; |
2155 |
2155 |
2156 Goal "((b + a)/# 2 - a) = (b - a)/(# 2::real)"; |
2156 Goal "((b + a)/2 - a) = (b - a)/(2::real)"; |
2157 by Auto_tac; |
2157 by Auto_tac; |
2158 qed "real_average_minus_second"; |
2158 qed "real_average_minus_second"; |
2159 Addsimps [real_average_minus_second]; |
2159 Addsimps [real_average_minus_second]; |
2160 |
2160 |
2161 |
2161 |
2162 (* Gallileo's "trick": average velocity = av. of end velocities *) |
2162 (* Gallileo's "trick": average velocity = av. of end velocities *) |
2163 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \ |
2163 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \ |
2164 \ ==> v((a + b)/# 2) = (v a + v b)/# 2"; |
2164 \ ==> v((a + b)/2) = (v a + v b)/2"; |
2165 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1); |
2165 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1); |
2166 by Auto_tac; |
2166 by Auto_tac; |
2167 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1); |
2167 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1); |
2168 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2); |
2168 by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2); |
2169 by (dtac real_less_half_sum 1); |
2169 by (dtac real_less_half_sum 1); |