36 lemma abs_minus_one: "abs (- (1::real)) = 1" |
36 lemma abs_minus_one: "abs (- (1::real)) = 1" |
37 by simp |
37 by simp |
38 |
38 |
39 lemma real_mult_le_le_mono1a: |
39 lemma real_mult_le_le_mono1a: |
40 "(0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
40 "(0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
41 by (simp add: real_mult_le_mono2) |
41 by (simp add: mult_left_mono) |
42 |
42 |
43 lemma real_mult_le_le_mono2: |
43 text{*The next two results are needlessly weak*} |
44 "(0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z" |
|
45 proof - |
|
46 assume "(0::real) \<le> z" "x \<le> y" |
|
47 hence "x < y \<or> x = y" by (auto simp add: order_le_less) |
|
48 thus ?thesis |
|
49 proof |
|
50 assume "x < y" |
|
51 show ?thesis by (rule real_mult_le_less_mono1) (simp!) |
|
52 next |
|
53 assume "x = y" |
|
54 thus ?thesis by simp |
|
55 qed |
|
56 qed |
|
57 |
|
58 lemma real_mult_less_le_anti: |
44 lemma real_mult_less_le_anti: |
59 "z < (0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x" |
45 "z < (0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x" |
60 proof - |
46 by (simp add: mult_left_mono_neg order_less_imp_le) |
61 assume "z < 0" "x \<le> y" |
|
62 hence "0 < - z" by simp |
|
63 hence "0 \<le> - z" by (rule order_less_imp_le) |
|
64 hence "x * (- z) \<le> y * (- z)" |
|
65 by (rule real_mult_le_le_mono2) |
|
66 hence "- (x * z) \<le> - (y * z)" |
|
67 by (simp only: real_mult_minus_eq2) |
|
68 thus ?thesis by (simp only: real_mult_commute) |
|
69 qed |
|
70 |
47 |
71 lemma real_mult_less_le_mono: |
48 lemma real_mult_less_le_mono: |
72 "(0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
49 "(0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
73 proof - |
50 by (simp add: mult_left_mono order_less_imp_le) |
74 assume "0 < z" "x \<le> y" |
|
75 have "0 \<le> z" by (rule order_less_imp_le) |
|
76 hence "x * z \<le> y * z" |
|
77 by (rule real_mult_le_le_mono2) |
|
78 thus ?thesis by (simp only: real_mult_commute) |
|
79 qed |
|
80 |
51 |
81 lemma real_mult_inv_right1: "(x::real) \<noteq> 0 \<Longrightarrow> x * inverse x = 1" |
52 lemma real_mult_inv_right1: "(x::real) \<noteq> 0 \<Longrightarrow> x * inverse x = 1" |
82 by simp |
53 by simp |
83 |
54 |
84 lemma real_mult_inv_left1: "(x::real) \<noteq> 0 \<Longrightarrow> inverse x * x = 1" |
55 lemma real_mult_inv_left1: "(x::real) \<noteq> 0 \<Longrightarrow> inverse x * x = 1" |
85 by simp |
56 by simp |
86 |
57 |
87 lemma real_le_mult_order1a: |
58 lemma real_le_mult_order1a: |
88 "(0::real) \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y" |
59 "(0::real) \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y" |
89 by (simp add: real_0_le_mult_iff) |
60 by (simp add: zero_le_mult_iff) |
90 |
61 |
91 lemma real_mult_diff_distrib: |
62 lemma real_mult_diff_distrib: |
92 "a * (- x - (y::real)) = - a * x - a * y" |
63 "a * (- x - (y::real)) = - a * x - a * y" |
93 proof - |
64 proof - |
94 have "- x - y = - x + - y" by simp |
65 have "- x - y = - x + - y" by simp |
95 also have "a * ... = a * - x + a * - y" |
66 also have "a * ... = a * - x + a * - y" |
96 by (simp only: real_add_mult_distrib2) |
67 by (simp only: right_distrib) |
97 also have "... = - a * x - a * y" |
68 also have "... = - a * x - a * y" |
98 by simp |
69 by simp |
99 finally show ?thesis . |
70 finally show ?thesis . |
100 qed |
71 qed |
101 |
72 |
102 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y" |
73 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y" |
103 proof - |
74 proof - |
104 have "x - y = x + - y" by simp |
75 have "x - y = x + - y" by simp |
105 also have "a * ... = a * x + a * - y" |
76 also have "a * ... = a * x + a * - y" |
106 by (simp only: real_add_mult_distrib2) |
77 by (simp only: right_distrib) |
107 also have "... = a * x - a * y" |
78 also have "... = a * x - a * y" |
108 by simp |
79 by simp |
109 finally show ?thesis . |
80 finally show ?thesis . |
110 qed |
81 qed |
111 |
82 |