equal
deleted
inserted
replaced
1587 |
1587 |
1588 lemma minus_pi_half_less_zero: "-(pi/2) < 0" |
1588 lemma minus_pi_half_less_zero: "-(pi/2) < 0" |
1589 by simp |
1589 by simp |
1590 |
1590 |
1591 lemma m2pi_less_pi: "- (2 * pi) < pi" |
1591 lemma m2pi_less_pi: "- (2 * pi) < pi" |
1592 proof - |
1592 by simp |
1593 have "- (2 * pi) < 0" and "0 < pi" by auto |
|
1594 from order_less_trans[OF this] show ?thesis . |
|
1595 qed |
|
1596 |
1593 |
1597 lemma sin_pi_half [simp]: "sin(pi/2) = 1" |
1594 lemma sin_pi_half [simp]: "sin(pi/2) = 1" |
1598 apply (cut_tac x = "pi/2" in sin_cos_squared_add2) |
1595 apply (cut_tac x = "pi/2" in sin_cos_squared_add2) |
1599 apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]) |
1596 apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two]) |
1600 apply (simp add: power2_eq_1_iff) |
1597 apply (simp add: power2_eq_1_iff) |
2349 |
2346 |
2350 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2" |
2347 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2" |
2351 proof - |
2348 proof - |
2352 let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)" |
2349 let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)" |
2353 have nonneg: "0 \<le> ?c" |
2350 have nonneg: "0 \<le> ?c" |
2354 by (rule cos_ge_zero, rule order_trans [where y=0], simp_all) |
2351 by (simp add: cos_ge_zero) |
2355 have "0 = cos (pi / 4 + pi / 4)" |
2352 have "0 = cos (pi / 4 + pi / 4)" |
2356 by simp |
2353 by simp |
2357 also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>" |
2354 also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>" |
2358 by (simp only: cos_add power2_eq_square) |
2355 by (simp only: cos_add power2_eq_square) |
2359 also have "\<dots> = 2 * ?c\<twosuperior> - 1" |
2356 also have "\<dots> = 2 * ?c\<twosuperior> - 1" |