22 apply (subst mult_2) |
22 apply (subst mult_2) |
23 apply (erule add_less_le_mono) |
23 apply (erule add_less_le_mono) |
24 apply (rule two_realpow_ge_one) |
24 apply (rule two_realpow_ge_one) |
25 done |
25 done |
26 |
26 |
27 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
27 (* TODO: no longer real-specific; rename and move elsewhere *) |
|
28 lemma realpow_Suc_le_self: |
|
29 fixes r :: "'a::linordered_semidom" |
|
30 shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r" |
28 by (insert power_decreasing [of 1 "Suc n" r], simp) |
31 by (insert power_decreasing [of 1 "Suc n" r], simp) |
29 |
32 |
30 lemma realpow_minus_mult [rule_format]: |
33 (* TODO: no longer real-specific; rename and move elsewhere *) |
31 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
34 lemma realpow_minus_mult: |
32 apply (simp split add: nat_diff_split) |
35 fixes x :: "'a::monoid_mult" |
33 done |
36 shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n" |
|
37 by (simp add: power_commutes split add: nat_diff_split) |
34 |
38 |
|
39 (* TODO: no longer real-specific; rename and move elsewhere *) |
35 lemma realpow_two_diff: |
40 lemma realpow_two_diff: |
36 "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
41 fixes x :: "'a::comm_ring_1" |
|
42 shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
37 by (simp add: algebra_simps) |
43 by (simp add: algebra_simps) |
38 |
44 |
|
45 (* TODO: move elsewhere *) |
|
46 lemma add_eq_0_iff: |
|
47 fixes x y :: "'a::group_add" |
|
48 shows "x + y = 0 \<longleftrightarrow> y = - x" |
|
49 by (auto dest: minus_unique) |
|
50 |
|
51 (* TODO: no longer real-specific; rename and move elsewhere *) |
39 lemma realpow_two_disj: |
52 lemma realpow_two_disj: |
40 "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" |
53 fixes x :: "'a::idom" |
41 apply (cut_tac x = x and y = y in realpow_two_diff) |
54 shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" |
42 apply auto |
55 using realpow_two_diff [of x y] |
43 done |
56 by (auto simp add: add_eq_0_iff) |
44 |
57 |
45 |
58 |
46 subsection{* Squares of Reals *} |
59 subsection{* Squares of Reals *} |
47 |
60 |
|
61 (* FIXME: declare this [simp] for all types, or not at all *) |
48 lemma real_two_squares_add_zero_iff [simp]: |
62 lemma real_two_squares_add_zero_iff [simp]: |
49 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
63 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
50 by (rule sum_squares_eq_zero_iff) |
64 by (rule sum_squares_eq_zero_iff) |
51 |
65 |
52 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" |
66 (* TODO: no longer real-specific; rename and move elsewhere *) |
53 by simp |
67 lemma real_squared_diff_one_factored: |
|
68 fixes x :: "'a::ring_1" |
|
69 shows "x * x - 1 = (x + 1) * (x - 1)" |
|
70 by (simp add: algebra_simps) |
54 |
71 |
55 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" |
72 (* TODO: no longer real-specific; rename and move elsewhere *) |
56 by simp |
73 lemma real_mult_is_one [simp]: |
|
74 fixes x :: "'a::ring_1_no_zero_divisors" |
|
75 shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1" |
|
76 proof - |
|
77 have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0" |
|
78 by (simp add: algebra_simps) |
|
79 also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1" |
|
80 by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1]) |
|
81 finally show ?thesis . |
|
82 qed |
57 |
83 |
58 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" |
84 (* FIXME: declare this [simp] for all types, or not at all *) |
59 by (simp add: real_add_eq_0_iff [symmetric]) |
|
60 |
|
61 lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" |
|
62 by (simp add: left_distrib right_diff_distrib) |
|
63 |
|
64 lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)" |
|
65 apply auto |
|
66 apply (drule right_minus_eq [THEN iffD2]) |
|
67 apply (auto simp add: real_squared_diff_one_factored) |
|
68 done |
|
69 |
|
70 lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)" |
|
71 by simp |
|
72 |
|
73 lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)" |
|
74 by simp |
|
75 |
|
76 lemma realpow_two_sum_zero_iff [simp]: |
85 lemma realpow_two_sum_zero_iff [simp]: |
77 "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" |
86 "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" |
78 by (rule sum_power2_eq_zero_iff) |
87 by (rule sum_power2_eq_zero_iff) |
79 |
88 |
|
89 (* FIXME: declare this [simp] for all types, or not at all *) |
80 lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2" |
90 lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2" |
81 by (rule sum_power2_ge_zero) |
91 by (rule sum_power2_ge_zero) |
82 |
92 |
|
93 (* FIXME: declare this [simp] for all types, or not at all *) |
83 lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2" |
94 lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2" |
84 by (intro add_nonneg_nonneg zero_le_power2) |
95 by (intro add_nonneg_nonneg zero_le_power2) |
85 |
|
86 lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y" |
|
87 by (simp add: sum_squares_gt_zero_iff) |
|
88 |
|
89 lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y" |
|
90 by (simp add: sum_squares_gt_zero_iff) |
|
91 |
96 |
92 lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))" |
97 lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))" |
93 by (rule_tac j = 0 in real_le_trans, auto) |
98 by (rule_tac j = 0 in real_le_trans, auto) |
94 |
99 |
95 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2" |
100 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2" |
96 by (auto simp add: power2_eq_square) |
101 by (auto simp add: power2_eq_square) |
97 |
102 |
98 (* The following theorem is by Benjamin Porter *) |
103 (* The following theorem is by Benjamin Porter *) |
|
104 (* TODO: no longer real-specific; rename and move elsewhere *) |
99 lemma real_sq_order: |
105 lemma real_sq_order: |
100 fixes x::real |
106 fixes x :: "'a::linordered_semidom" |
101 assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2" |
107 assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2" |
102 shows "x \<le> y" |
108 shows "x \<le> y" |
103 proof - |
109 proof - |
104 from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)" |
110 from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)" |
105 by (simp only: numeral_2_eq_2) |
111 by (simp only: numeral_2_eq_2) |