9 |
9 |
10 text {* Some existing theorems are declared as extra introduction |
10 text {* Some existing theorems are declared as extra introduction |
11 or elimination rules, respectively. *} |
11 or elimination rules, respectively. *} |
12 |
12 |
13 lemmas [intro?] = isLub_isUb |
13 lemmas [intro?] = isLub_isUb |
14 lemmas [intro?] = chainD |
14 lemmas [intro?] = chainD |
15 lemmas chainE2 = chainD2 [elim_format, standard] |
15 lemmas chainE2 = chainD2 [elim_format, standard] |
16 |
16 |
17 text_raw {* \medskip *} |
|
18 text{* Lemmas about sets. *} |
|
19 |
17 |
20 lemma Int_singletonD: "[| A \<inter> B = {v}; x \<in> A; x \<in> B |] ==> x = v" |
18 text {* \medskip Lemmas about sets. *} |
|
19 |
|
20 lemma Int_singletonD: "A \<inter> B = {v} \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x = v" |
21 by (fast elim: equalityE) |
21 by (fast elim: equalityE) |
22 |
22 |
23 lemma set_less_imp_diff_not_empty: "H < E ==> \<exists>x0 \<in> E. x0 \<notin> H" |
23 lemma set_less_imp_diff_not_empty: "H < E \<Longrightarrow> \<exists>x0 \<in> E. x0 \<notin> H" |
24 by (force simp add: psubset_eq) |
24 by (auto simp add: psubset_eq) |
25 |
25 |
26 text_raw {* \medskip *} |
|
27 text{* Some lemmas about orders. *} |
|
28 |
26 |
29 lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \<noteq> y" |
27 text{* \medskip Some lemmas about orders. *} |
|
28 |
|
29 lemma lt_imp_not_eq: "x < (y::'a::order) \<Longrightarrow> x \<noteq> y" |
30 by (simp add: order_less_le) |
30 by (simp add: order_less_le) |
31 |
31 |
32 lemma le_noteq_imp_less: |
32 lemma le_noteq_imp_less: |
33 "[| x <= (r::'a::order); x \<noteq> r |] ==> x < r" |
33 "x \<le> (r::'a::order) \<Longrightarrow> x \<noteq> r \<Longrightarrow> x < r" |
34 proof - |
34 proof - |
35 assume "x <= r" and ne:"x \<noteq> r" |
35 assume "x \<le> r" and ne:"x \<noteq> r" |
36 hence "x < r | x = r" by (simp add: order_le_less) |
36 hence "x < r \<or> x = r" by (simp add: order_le_less) |
37 with ne show ?thesis by simp |
37 with ne show ?thesis by simp |
38 qed |
38 qed |
39 |
39 |
40 text_raw {* \medskip *} |
|
41 text{* Some lemmas for the reals. *} |
|
42 |
40 |
43 lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y" |
41 text {* \medskip Some lemmas for the reals. *} |
|
42 |
|
43 lemma real_add_minus_eq: "x - y = (#0::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 (- (#1::real)) = #1" |
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) <= z; x <= y |] ==> z * x <= z * y" |
50 "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
51 proof - |
51 proof - |
52 assume z: "(#0::real) <= z" and "x <= y" |
52 assume z: "(#0::real) \<le> z" and "x \<le> y" |
53 hence "x < y | x = y" by (force simp add: order_le_less) |
53 hence "x < y \<or> x = y" by (auto simp add: order_le_less) |
54 thus ?thesis |
54 thus ?thesis |
55 proof (elim disjE) |
55 proof |
56 assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp |
56 assume "x < y" show ?thesis by (rule real_mult_le_less_mono2) simp |
57 next |
57 next |
58 assume "x = y" thus ?thesis by simp |
58 assume "x = y" thus ?thesis by simp |
59 qed |
59 qed |
60 qed |
60 qed |
61 |
61 |
62 lemma real_mult_le_le_mono2: |
62 lemma real_mult_le_le_mono2: |
63 "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z" |
63 "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z" |
64 proof - |
64 proof - |
65 assume "(#0::real) <= z" "x <= y" |
65 assume "(#0::real) \<le> z" "x \<le> y" |
66 hence "x < y | x = y" by (force simp add: order_le_less) |
66 hence "x < y \<or> x = y" by (auto simp add: order_le_less) |
67 thus ?thesis |
67 thus ?thesis |
68 proof (elim disjE) |
68 proof |
69 assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp |
69 assume "x < y" |
70 next |
70 show ?thesis by (rule real_mult_le_less_mono1) (simp!) |
71 assume "x = y" thus ?thesis by simp |
71 next |
|
72 assume "x = y" |
|
73 thus ?thesis by simp |
72 qed |
74 qed |
73 qed |
75 qed |
74 |
76 |
75 lemma real_mult_less_le_anti: |
77 lemma real_mult_less_le_anti: |
76 "[| z < (#0::real); x <= y |] ==> z * y <= z * x" |
78 "z < (#0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x" |
77 proof - |
79 proof - |
78 assume "z < #0" "x <= y" |
80 assume "z < #0" "x \<le> y" |
79 hence "#0 < - z" by simp |
81 hence "#0 < - z" by simp |
80 hence "#0 <= - z" by (rule real_less_imp_le) |
82 hence "#0 \<le> - z" by (rule real_less_imp_le) |
81 hence "x * (- z) <= y * (- z)" |
83 hence "x * (- z) \<le> y * (- z)" |
82 by (rule real_mult_le_le_mono2) |
84 by (rule real_mult_le_le_mono2) |
83 hence "- (x * z) <= - (y * z)" |
85 hence "- (x * z) \<le> - (y * z)" |
84 by (simp only: real_minus_mult_eq2) |
86 by (simp only: real_minus_mult_eq2) |
85 thus ?thesis by (simp only: real_mult_commute) |
87 thus ?thesis by (simp only: real_mult_commute) |
86 qed |
88 qed |
87 |
89 |
88 lemma real_mult_less_le_mono: |
90 lemma real_mult_less_le_mono: |
89 "[| (#0::real) < z; x <= y |] ==> z * x <= z * y" |
91 "(#0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y" |
90 proof - |
92 proof - |
91 assume "#0 < z" "x <= y" |
93 assume "#0 < z" "x \<le> y" |
92 have "#0 <= z" by (rule real_less_imp_le) |
94 have "#0 \<le> z" by (rule real_less_imp_le) |
93 hence "x * z <= y * z" |
95 hence "x * z \<le> y * z" |
94 by (rule real_mult_le_le_mono2) |
96 by (rule real_mult_le_le_mono2) |
95 thus ?thesis by (simp only: real_mult_commute) |
97 thus ?thesis by (simp only: real_mult_commute) |
96 qed |
98 qed |
97 |
99 |
98 lemma real_inverse_gt_zero1: "#0 < (x::real) ==> #0 < inverse x" |
100 lemma real_inverse_gt_zero1: "#0 < (x::real) \<Longrightarrow> #0 < inverse x" |
99 proof - |
101 proof - |
100 assume "#0 < x" |
102 assume "#0 < x" |
101 have "0 < x" by simp |
103 have "0 < x" by simp |
102 hence "0 < inverse x" by (rule real_inverse_gt_zero) |
104 hence "0 < inverse x" by (rule real_inverse_gt_zero) |
103 thus ?thesis by simp |
105 thus ?thesis by simp |
104 qed |
106 qed |
105 |
107 |
106 lemma real_mult_inv_right1: "(x::real) \<noteq> #0 ==> x * inverse x = #1" |
108 lemma real_mult_inv_right1: "(x::real) \<noteq> #0 \<Longrightarrow> x * inverse x = #1" |
107 by simp |
109 by simp |
108 |
110 |
109 lemma real_mult_inv_left1: "(x::real) \<noteq> #0 ==> inverse x * x = #1" |
111 lemma real_mult_inv_left1: "(x::real) \<noteq> #0 \<Longrightarrow> inverse x * x = #1" |
110 by simp |
112 by simp |
111 |
113 |
112 lemma real_le_mult_order1a: |
114 lemma real_le_mult_order1a: |
113 "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y" |
115 "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y" |
114 proof - |
116 proof - |
115 assume "#0 <= x" "#0 <= y" |
117 assume "#0 \<le> x" "#0 \<le> y" |
116 have "[|0 <= x; 0 <= y|] ==> 0 <= x * y" |
118 have "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y" |
117 by (rule real_le_mult_order) |
119 by (rule real_le_mult_order) |
118 thus ?thesis by (simp!) |
120 thus ?thesis by (simp!) |
119 qed |
121 qed |
120 |
122 |
121 lemma real_mult_diff_distrib: |
123 lemma real_mult_diff_distrib: |
122 "a * (- x - (y::real)) = - a * x - a * y" |
124 "a * (- x - (y::real)) = - a * x - a * y" |
123 proof - |
125 proof - |
124 have "- x - y = - x + - y" by simp |
126 have "- x - y = - x + - y" by simp |
125 also have "a * ... = a * - x + a * - y" |
127 also have "a * ... = a * - x + a * - y" |
126 by (simp only: real_add_mult_distrib2) |
128 by (simp only: real_add_mult_distrib2) |
127 also have "... = - a * x - a * y" |
129 also have "... = - a * x - a * y" |
128 by simp |
130 by simp |
129 finally show ?thesis . |
131 finally show ?thesis . |
130 qed |
132 qed |
131 |
133 |
132 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y" |
134 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y" |
133 proof - |
135 proof - |
134 have "x - y = x + - y" by simp |
136 have "x - y = x + - y" by simp |
135 also have "a * ... = a * x + a * - y" |
137 also have "a * ... = a * x + a * - y" |
136 by (simp only: real_add_mult_distrib2) |
138 by (simp only: real_add_mult_distrib2) |
137 also have "... = a * x - a * y" |
139 also have "... = a * x - a * y" |
138 by simp |
140 by simp |
139 finally show ?thesis . |
141 finally show ?thesis . |
140 qed |
142 qed |
141 |
143 |
142 lemma real_minus_le: "- (x::real) <= y ==> - y <= x" |
144 lemma real_minus_le: "- (x::real) \<le> y \<Longrightarrow> - y \<le> x" |
143 by simp |
145 by simp |
144 |
146 |
145 lemma real_diff_ineq_swap: |
147 lemma real_diff_ineq_swap: |
146 "(d::real) - b <= c + a ==> - a - b <= c - d" |
148 "(d::real) - b \<le> c + a \<Longrightarrow> - a - b \<le> c - d" |
147 by simp |
149 by simp |
148 |
150 |
149 end |
151 end |