38 qed |
38 qed |
39 |
39 |
40 |
40 |
41 text {* \medskip Some lemmas for the reals. *} |
41 text {* \medskip Some lemmas for the reals. *} |
42 |
42 |
43 lemma real_add_minus_eq: "x - y = (#0::real) \<Longrightarrow> x = y" |
43 lemma real_add_minus_eq: "x - y = (Numeral0::real) \<Longrightarrow> x = y" |
44 by simp |
44 by simp |
45 |
45 |
46 lemma abs_minus_one: "abs (- (#1::real)) = #1" |
46 lemma abs_minus_one: "abs (- (Numeral1::real)) = Numeral1" |
47 by simp |
47 by simp |
48 |
48 |
49 lemma real_mult_le_le_mono1a: |
49 lemma real_mult_le_le_mono1a: |
50 "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
50 "(Numeral0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
51 by (simp add: real_mult_le_mono2) |
51 by (simp add: real_mult_le_mono2) |
52 |
52 |
53 lemma real_mult_le_le_mono2: |
53 lemma real_mult_le_le_mono2: |
54 "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z" |
54 "(Numeral0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z" |
55 proof - |
55 proof - |
56 assume "(#0::real) \<le> z" "x \<le> y" |
56 assume "(Numeral0::real) \<le> z" "x \<le> y" |
57 hence "x < y \<or> x = y" by (auto simp add: order_le_less) |
57 hence "x < y \<or> x = y" by (auto simp add: order_le_less) |
58 thus ?thesis |
58 thus ?thesis |
59 proof |
59 proof |
60 assume "x < y" |
60 assume "x < y" |
61 show ?thesis by (rule real_mult_le_less_mono1) (simp!) |
61 show ?thesis by (rule real_mult_le_less_mono1) (simp!) |
64 thus ?thesis by simp |
64 thus ?thesis by simp |
65 qed |
65 qed |
66 qed |
66 qed |
67 |
67 |
68 lemma real_mult_less_le_anti: |
68 lemma real_mult_less_le_anti: |
69 "z < (#0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x" |
69 "z < (Numeral0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x" |
70 proof - |
70 proof - |
71 assume "z < #0" "x \<le> y" |
71 assume "z < Numeral0" "x \<le> y" |
72 hence "#0 < - z" by simp |
72 hence "Numeral0 < - z" by simp |
73 hence "#0 \<le> - z" by (rule order_less_imp_le) |
73 hence "Numeral0 \<le> - z" by (rule order_less_imp_le) |
74 hence "x * (- z) \<le> y * (- z)" |
74 hence "x * (- z) \<le> y * (- z)" |
75 by (rule real_mult_le_le_mono2) |
75 by (rule real_mult_le_le_mono2) |
76 hence "- (x * z) \<le> - (y * z)" |
76 hence "- (x * z) \<le> - (y * z)" |
77 by (simp only: real_minus_mult_eq2) |
77 by (simp only: real_minus_mult_eq2) |
78 thus ?thesis by (simp only: real_mult_commute) |
78 thus ?thesis by (simp only: real_mult_commute) |
79 qed |
79 qed |
80 |
80 |
81 lemma real_mult_less_le_mono: |
81 lemma real_mult_less_le_mono: |
82 "(#0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
82 "(Numeral0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
83 proof - |
83 proof - |
84 assume "#0 < z" "x \<le> y" |
84 assume "Numeral0 < z" "x \<le> y" |
85 have "#0 \<le> z" by (rule order_less_imp_le) |
85 have "Numeral0 \<le> z" by (rule order_less_imp_le) |
86 hence "x * z \<le> y * z" |
86 hence "x * z \<le> y * z" |
87 by (rule real_mult_le_le_mono2) |
87 by (rule real_mult_le_le_mono2) |
88 thus ?thesis by (simp only: real_mult_commute) |
88 thus ?thesis by (simp only: real_mult_commute) |
89 qed |
89 qed |
90 |
90 |
91 lemma real_inverse_gt_zero1: "#0 < (x::real) \<Longrightarrow> #0 < inverse x" |
91 lemma real_inverse_gt_zero1: "Numeral0 < (x::real) \<Longrightarrow> Numeral0 < inverse x" |
92 proof - |
92 proof - |
93 assume "#0 < x" |
93 assume "Numeral0 < x" |
94 have "0 < x" by simp |
94 have "0 < x" by simp |
95 hence "0 < inverse x" by (rule real_inverse_gt_zero) |
95 hence "0 < inverse x" by (rule real_inverse_gt_zero) |
96 thus ?thesis by simp |
96 thus ?thesis by simp |
97 qed |
97 qed |
98 |
98 |
99 lemma real_mult_inv_right1: "(x::real) \<noteq> #0 \<Longrightarrow> x * inverse x = #1" |
99 lemma real_mult_inv_right1: "(x::real) \<noteq> Numeral0 \<Longrightarrow> x * inverse x = Numeral1" |
100 by simp |
100 by simp |
101 |
101 |
102 lemma real_mult_inv_left1: "(x::real) \<noteq> #0 \<Longrightarrow> inverse x * x = #1" |
102 lemma real_mult_inv_left1: "(x::real) \<noteq> Numeral0 \<Longrightarrow> inverse x * x = Numeral1" |
103 by simp |
103 by simp |
104 |
104 |
105 lemma real_le_mult_order1a: |
105 lemma real_le_mult_order1a: |
106 "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y" |
106 "(Numeral0::real) \<le> x \<Longrightarrow> Numeral0 \<le> y \<Longrightarrow> Numeral0 \<le> x * y" |
107 by (simp add: real_0_le_mult_iff) |
107 by (simp add: real_0_le_mult_iff) |
108 |
108 |
109 lemma real_mult_diff_distrib: |
109 lemma real_mult_diff_distrib: |
110 "a * (- x - (y::real)) = - a * x - a * y" |
110 "a * (- x - (y::real)) = - a * x - a * y" |
111 proof - |
111 proof - |