|
1 |
|
2 theory Aux = Main + Real:; |
|
3 |
|
4 |
|
5 theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *) |
|
6 by (asm_simp add: order_less_le); |
|
7 |
|
8 lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; |
|
9 by (rule order_less_le[RS iffD1, RS conjunct2]); |
|
10 |
|
11 lemma Int_singeltonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v"; |
|
12 by (fast elim: equalityE); |
|
13 |
|
14 lemma real_add_minus_eq: "x - y = 0r ==> x = y"; |
|
15 proof -; |
|
16 assume "x - y = 0r"; |
|
17 have "x + - y = x - y"; by simp; |
|
18 also; have "... = 0r"; .; |
|
19 finally; have "x + - y = 0r"; .; |
|
20 hence "x = - (- y)"; by (rule real_add_minus_eq_minus); |
|
21 also; have "... = y"; by asm_simp; |
|
22 finally; show "x = y"; .; |
|
23 qed; |
|
24 |
|
25 lemma rabs_minus_one: "rabs (- 1r) = 1r"; |
|
26 proof -; |
|
27 have "rabs (- 1r) = - (- 1r)"; |
|
28 proof (rule rabs_minus_eqI2); |
|
29 show "-1r < 0r"; |
|
30 by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one); |
|
31 qed; |
|
32 also; have "... = 1r"; by asm_simp; |
|
33 finally; show ?thesis; by asm_simp; |
|
34 qed; |
|
35 |
|
36 axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z"; |
|
37 |
|
38 axioms real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x"; |
|
39 |
|
40 axioms real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y"; |
|
41 |
|
42 axioms real_mult_diff_distrib: "a * (- x - y) = - a * x - a * y"; |
|
43 |
|
44 axioms real_mult_diff_distrib2: "a * (x - y) = a * x - a * y"; |
|
45 |
|
46 lemma less_imp_le: "(x::real) < y ==> x <= y"; |
|
47 by (asm_simp only: real_less_imp_le); |
|
48 |
|
49 lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r"; |
|
50 proof -; |
|
51 assume "x <= (r::'a::order)"; |
|
52 assume "x ~= r"; |
|
53 then; have "x < r | x = r"; |
|
54 by (asm_simp add: order_le_less); |
|
55 then; show ?thesis; |
|
56 by asm_simp; |
|
57 qed; |
|
58 |
|
59 lemma minus_le: "- (x::real) <= y ==> - y <= x"; |
|
60 proof -; |
|
61 assume "- x <= y"; |
|
62 hence "- x < y | - x = y"; by (rule order_le_less [RS iffD1]); |
|
63 thus "-y <= x"; |
|
64 proof; |
|
65 assume "- x < y"; show ?thesis; |
|
66 proof -; |
|
67 have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); |
|
68 hence "- y < x"; by asm_simp; |
|
69 thus ?thesis; by (rule real_less_imp_le); |
|
70 qed; |
|
71 next; |
|
72 assume "- x = y"; show ?thesis; by force; |
|
73 qed; |
|
74 qed; |
|
75 |
|
76 lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)"; |
|
77 proof (rule case [of "rabs x = r"]); |
|
78 assume a: "rabs x = r"; |
|
79 show ?thesis; |
|
80 proof; |
|
81 assume "rabs x <= r"; |
|
82 show "- r <= x & x <= r"; |
|
83 proof; |
|
84 have "- x <= rabs x"; by (rule rabs_ge_minus_self); |
|
85 hence "- x <= r"; by asm_simp; |
|
86 thus "- r <= x"; by (asm_simp add : minus_le [of "x" "r"]); |
|
87 have "x <= rabs x"; by (rule rabs_ge_self); |
|
88 thus "x <= r"; by asm_simp; |
|
89 qed; |
|
90 next; |
|
91 assume "- r <= x & x <= r"; |
|
92 show "rabs x <= r"; by fast; |
|
93 qed; |
|
94 next; |
|
95 assume "rabs x ~= r"; |
|
96 show ?thesis; |
|
97 proof; |
|
98 assume "rabs x <= r"; |
|
99 have "rabs x < r"; by (rule conjI [RS real_less_le [RS iffD2]]); |
|
100 hence "- r < x & x < r"; by (rule rabs_interval_iff [RS iffD1]); |
|
101 thus "- r <= x & x <= r"; |
|
102 proof(elim conjE, intro conjI); |
|
103 assume "- r < x"; |
|
104 show "- r <= x"; by (rule real_less_imp_le); |
|
105 assume "x < r"; |
|
106 show "x <= r"; by (rule real_less_imp_le); |
|
107 qed; |
|
108 next; |
|
109 assume "- r <= x & x <= r"; |
|
110 thus "rabs x <= r"; |
|
111 proof; |
|
112 assume "- r <= x" "x <= r"; |
|
113 show ?thesis; |
|
114 proof (rule rabs_disj [RS disjE, of x]); |
|
115 assume "rabs x = x"; |
|
116 show ?thesis; by asm_simp; |
|
117 next; |
|
118 assume "rabs x = - x"; |
|
119 from minus_le [of r x]; show ?thesis; by asm_simp; |
|
120 qed; |
|
121 qed; |
|
122 qed; |
|
123 qed; |
|
124 |
|
125 lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H"; |
|
126 proof- ; |
|
127 assume "H < E "; |
|
128 have le: "H <= E"; by (rule conjunct1 [OF psubset_eq[RS iffD1]]); |
|
129 have ne: "H ~= E"; by (rule conjunct2 [OF psubset_eq[RS iffD1]]); |
|
130 with le; show ?thesis; by force; |
|
131 qed; |
|
132 |
|
133 |
|
134 end; |