4 |
4 |
5 theory Dense_Linear_Order_Ex |
5 theory Dense_Linear_Order_Ex |
6 imports "../Dense_Linear_Order" |
6 imports "../Dense_Linear_Order" |
7 begin |
7 begin |
8 |
8 |
9 lemma |
9 lemma "\<exists>(y::'a::linordered_field) < 2. x + 3* y < 0 \<and> x - y > 0" |
10 "\<exists>(y::'a::{linordered_field}) <2. x + 3* y < 0 \<and> x - y >0" |
|
11 by ferrack |
10 by ferrack |
12 |
11 |
13 lemma "~ (ALL x (y::'a::{linordered_field}). x < y --> 10*x < 11*y)" |
12 lemma "\<not> (\<forall>x (y::'a::linordered_field). x < y \<longrightarrow> 10 * x < 11 * y)" |
14 by ferrack |
13 by ferrack |
15 |
14 |
16 lemma "ALL (x::'a::{linordered_field}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" |
15 lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> 10 * (x + 5 * y + -1) < 60 * y" |
17 by ferrack |
16 by ferrack |
18 |
17 |
19 lemma "EX (x::'a::{linordered_field}) y. x ~= y --> x < y" |
18 lemma "\<exists>(x::'a::linordered_field) y. x \<noteq> y \<longrightarrow> x < y" |
20 by ferrack |
19 by ferrack |
21 |
20 |
22 lemma "EX (x::'a::{linordered_field}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" |
21 lemma "\<exists>(x::'a::linordered_field) y. x \<noteq> y \<and> 10 * x \<noteq> 9 * y \<and> 10 * x < y \<longrightarrow> x < y" |
23 by ferrack |
22 by ferrack |
24 |
23 |
25 lemma "ALL (x::'a::{linordered_field}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" |
24 lemma "\<forall>(x::'a::linordered_field) y. x \<noteq> y \<and> 5 * x \<le> y \<longrightarrow> 500 * x \<le> 100 * y" |
26 by ferrack |
25 by ferrack |
27 |
26 |
28 lemma "ALL (x::'a::{linordered_field}). (EX (y::'a::{linordered_field}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" |
27 lemma "\<forall>x::'a::linordered_field. \<exists>y::'a::linordered_field. 4 * x + 3 * y \<le> 0 \<and> 4 * x + 3 * y \<ge> -1" |
29 by ferrack |
28 by ferrack |
30 |
29 |
31 lemma "ALL (x::'a::{linordered_field}) < 0. (EX (y::'a::{linordered_field}) > 0. 7*x + y > 0 & x - y <= 9)" |
30 lemma "\<forall>(x::'a::linordered_field) < 0. \<exists>(y::'a::linordered_field) > 0. 7 * x + y > 0 \<and> x - y \<le> 9" |
32 by ferrack |
31 by ferrack |
33 |
32 |
34 lemma "EX (x::'a::{linordered_field}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" |
33 lemma "\<exists>x::'a::linordered_field. 0 < x \<and> x < 1 \<longrightarrow> (\<forall>y > 1. x + y \<noteq> 1)" |
35 by ferrack |
34 by ferrack |
36 |
35 |
37 lemma "EX x. (ALL (y::'a::{linordered_field}). y < 2 --> 2*(y - x) \<le> 0 )" |
36 lemma "\<exists>x. \<forall>y::'a::linordered_field. y < 2 \<longrightarrow> 2 * (y - x) \<le> 0" |
38 by ferrack |
37 by ferrack |
39 |
38 |
40 lemma "ALL (x::'a::{linordered_field}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" |
39 lemma "\<forall>x::'a::linordered_field. x < 10 \<or> x > 20 \<or> (\<exists>y. y \<ge> 0 \<and> y \<le> 10 \<and> x + y = 20)" |
41 by ferrack |
40 by ferrack |
42 |
41 |
43 lemma "ALL (x::'a::{linordered_field}) y z. x + y < z --> y >= z --> x < 0" |
42 lemma "\<forall>(x::'a::linordered_field) y z. x + y < z \<longrightarrow> y \<ge> z \<longrightarrow> x < 0" |
44 by ferrack |
43 by ferrack |
45 |
44 |
46 lemma "EX (x::'a::{linordered_field}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" |
45 lemma "\<exists>(x::'a::linordered_field) y z. x + 7 * y < 5 * z \<and> 5 * y \<ge> 7 * z \<and> x < 0" |
47 by ferrack |
46 by ferrack |
48 |
47 |
49 lemma "ALL (x::'a::{linordered_field}) y z. abs (x + y) <= z --> (abs z = z)" |
48 lemma "\<forall>(x::'a::linordered_field) y z. \<bar>x + y\<bar> \<le> z \<longrightarrow> \<bar>z\<bar> = z" |
50 by ferrack |
49 by ferrack |
51 |
50 |
52 lemma "EX (x::'a::{linordered_field}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" |
51 lemma "\<exists>(x::'a::linordered_field) y z. x + 7 * y - 5 * z < 0 \<and> 5 * y + 7 * z + 3 * x < 0" |
53 by ferrack |
52 by ferrack |
54 |
53 |
55 lemma "ALL (x::'a::{linordered_field}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" |
54 lemma "\<forall>(x::'a::linordered_field) y z. |
|
55 (\<bar>5 * x + 3 * y + z\<bar> \<le> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<ge> - (5 * x + 3 * y + z)) \<or> |
|
56 (\<bar>5 * x + 3 * y + z\<bar> \<ge> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<le> - (5 * x + 3 * y + z))" |
56 by ferrack |
57 by ferrack |
57 |
58 |
58 lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)" |
59 lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> (\<exists>z>0. x + z = y)" |
59 by ferrack |
60 by ferrack |
60 |
61 |
61 lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)" |
62 lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> (\<exists>z>0. x + z = y)" |
62 by ferrack |
63 by ferrack |
63 |
64 |
64 lemma "ALL (x::'a::{linordered_field}) y. (EX z>0. abs (x - y) <= z )" |
65 lemma "\<forall>(x::'a::linordered_field) y. \<exists>z>0. \<bar>x - y\<bar> \<le> z" |
65 by ferrack |
66 by ferrack |
66 |
67 |
67 lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" |
68 lemma "\<exists>(x::'a::linordered_field) y. \<forall>z<0. (z < x \<longrightarrow> z \<le> y) \<and> (z > y \<longrightarrow> z \<ge> x)" |
68 by ferrack |
69 by ferrack |
69 |
70 |
70 lemma "EX (x::'a::{linordered_field}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" |
71 lemma "\<exists>(x::'a::linordered_field) y. \<forall>z\<ge>0. \<bar>3 * x + 7 * y\<bar> \<le> 2 * z + 1" |
71 by ferrack |
72 by ferrack |
72 |
73 |
73 lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" |
74 lemma "\<exists>(x::'a::linordered_field) y. \<forall>z<0. (z < x \<longrightarrow> z \<le> y) \<and> (z > y \<longrightarrow> z \<ge> x)" |
74 by ferrack |
75 by ferrack |
75 |
76 |
76 lemma "EX (x::'a::{linordered_field})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" |
77 lemma "\<exists>(x::'a::linordered_field) > 0. \<forall>y. \<exists>z. 13 * \<bar>z\<bar> \<noteq> \<bar>12 * y - x\<bar> \<and> 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z" |
77 by ferrack |
78 by ferrack |
78 |
79 |
79 lemma "EX (x::'a::{linordered_field}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))" |
80 lemma "\<exists>x::'a::linordered_field. |
|
81 \<bar>4 * x + 17\<bar> < 4 \<and> (\<forall>y. \<bar>x * 34 - 34 * y - 9\<bar> \<noteq> 0 \<longrightarrow> (\<exists>z. 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z))" |
80 by ferrack |
82 by ferrack |
81 |
83 |
82 lemma "ALL (x::'a::{linordered_field}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" |
84 lemma "\<forall>x::'a::linordered_field. \<exists>y > \<bar>23 * x - 9\<bar>. \<forall>z > \<bar>3 * y - 19 * \<bar>x\<bar>\<bar>. x + z > 2 * y" |
83 by ferrack |
85 by ferrack |
84 |
86 |
85 lemma "ALL (x::'a::{linordered_field}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" |
87 lemma "\<forall>x::'a::linordered_field. |
|
88 \<exists>y < \<bar>3 * x - 1\<bar>. \<forall>z \<ge> 3 * \<bar>x\<bar> - 1. \<bar>12 * x - 13 * y + 19 * z\<bar> > \<bar>23 * x\<bar>" |
86 by ferrack |
89 by ferrack |
87 |
90 |
88 lemma "EX (x::'a::{linordered_field}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" |
91 lemma "\<exists>x::'a::linordered_field. \<bar>x\<bar> < 100 \<and> (\<forall>y > x. (\<exists>z < 2 * y - x. 5 * x - 3 * y \<le> 7 * z))" |
89 by ferrack |
92 by ferrack |
90 |
93 |
91 lemma "ALL (x::'a::{linordered_field}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" |
94 lemma "\<forall>(x::'a::linordered_field) y z w. |
|
95 7 * x < 3 * y \<longrightarrow> 5 * y < 7 * z \<longrightarrow> z < 2 * w \<longrightarrow> 7 * (2 * w - x) > 2 * y" |
92 by ferrack |
96 by ferrack |
93 |
97 |
94 lemma "EX (x::'a::{linordered_field}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" |
98 lemma "\<exists>(x::'a::linordered_field) y z w. 5 * x + 3 * z - 17 * w + \<bar>y - 8 * x + z\<bar> \<le> 89" |
95 by ferrack |
99 by ferrack |
96 |
100 |
97 lemma "EX (x::'a::{linordered_field}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" |
101 lemma "\<exists>(x::'a::linordered_field) y z w. |
|
102 5 * x + 3 * z - 17 * w + 7 * (y - 8 * x + z) \<le> max y (7 * z - x + w)" |
98 by ferrack |
103 by ferrack |
99 |
104 |
100 lemma "EX (x::'a::{linordered_field}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" |
105 lemma "\<exists>(x::'a::linordered_field) y z w. |
|
106 min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" |
101 by ferrack |
107 by ferrack |
102 |
108 |
103 lemma "ALL (x::'a::{linordered_field}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" |
109 lemma "\<forall>(x::'a::linordered_field) y z. \<exists>w \<ge> x + y + z. w \<le> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>" |
104 by ferrack |
110 by ferrack |
105 |
111 |
106 lemma "~(ALL (x::'a::{linordered_field}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" |
112 lemma "\<not> (\<forall>x::'a::linordered_field. \<exists>y z w. |
|
113 3 * x + z * 4 = 3 * y \<and> x + y < z \<and> x > w \<and> 3 * x < w + y)" |
107 by ferrack |
114 by ferrack |
108 |
115 |
109 lemma "ALL (x::'a::{linordered_field}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" |
116 lemma "\<forall>(x::'a::linordered_field) y. \<exists>z w. \<bar>x - y\<bar> = z - w \<and> z * 1234 < 233 * x \<and> w \<noteq> y" |
110 by ferrack |
117 by ferrack |
111 |
118 |
112 lemma "ALL (x::'a::{linordered_field}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" |
119 lemma "\<forall>x::'a::linordered_field. \<exists>y z w. |
|
120 min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" |
113 by ferrack |
121 by ferrack |
114 |
122 |
115 lemma "EX (x::'a::{linordered_field}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" |
123 lemma "\<exists>(x::'a::linordered_field) y z. \<forall>w \<ge> \<bar>x + y + z\<bar>. w \<ge> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>" |
116 by ferrack |
124 by ferrack |
117 |
125 |
118 lemma "EX z. (ALL (x::'a::{linordered_field}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" |
126 lemma "\<exists>z. \<forall>(x::'a::linordered_field) y. \<exists>w \<ge> x + y + z. w \<le> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>" |
119 by ferrack |
127 by ferrack |
120 |
128 |
121 lemma "EX z. (ALL (x::'a::{linordered_field}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" |
129 lemma "\<exists>z. \<forall>(x::'a::linordered_field) < \<bar>z\<bar>. \<exists>y w. x < y \<and> x < z \<and> x > w \<and> 3 * x < w + y" |
122 by ferrack |
130 by ferrack |
123 |
131 |
124 lemma "ALL (x::'a::{linordered_field}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" |
132 lemma "\<forall>(x::'a::linordered_field) y. \<exists>z. \<forall>w. \<bar>x - y\<bar> = \<bar>z - w\<bar> \<longrightarrow> z < x \<and> w \<noteq> y" |
125 by ferrack |
133 by ferrack |
126 |
134 |
127 lemma "EX y. (ALL (x::'a::{linordered_field}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" |
135 lemma "\<exists>y. \<forall>x::'a::linordered_field. \<exists>z w. |
|
136 min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" |
128 by ferrack |
137 by ferrack |
129 |
138 |
130 lemma "EX (x::'a::{linordered_field}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" |
139 lemma "\<exists>(x::'a::linordered_field) z. \<forall>w \<ge> 13 * x - 4 * z. \<exists>y. w \<ge> \<bar>x\<bar> + \<bar>y\<bar> + z" |
131 by ferrack |
140 by ferrack |
132 |
141 |
133 lemma "EX (x::'a::{linordered_field}). (ALL y < x. (EX z > (x+y). |
142 lemma "\<exists>x::'a::linordered_field. \<forall>y < x. \<exists>z > x + y. |
134 (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" |
143 \<forall>w. 5 * w + 10 * x - z \<ge> y \<longrightarrow> w + 7 * x + 3 * z \<ge> 2 * y" |
135 by ferrack |
144 by ferrack |
136 |
145 |
137 lemma "EX (x::'a::{linordered_field}). (ALL y. (EX z > y. |
146 lemma "\<exists>x::'a::linordered_field. \<forall>y. \<exists>z > y. |
138 (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" |
147 \<forall>w. w < 13 \<longrightarrow> w + 10 * x - z \<ge> y \<longrightarrow> 5 * w + 7 * x + 13 * z \<ge> 2 * y" |
139 by ferrack |
148 by ferrack |
140 |
149 |
141 lemma "EX (x::'a::{linordered_field}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" |
150 lemma "\<exists>(x::'a::linordered_field) y z w. |
|
151 min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)" |
142 by ferrack |
152 by ferrack |
143 |
153 |
144 lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" |
154 lemma "\<forall>x::'a::linordered_field. \<exists>y. \<forall>z>19. y \<le> x + z \<and> (\<exists>w. \<bar>y - x\<bar> < w)" |
145 by ferrack |
155 by ferrack |
146 |
156 |
147 lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" |
157 lemma "\<forall>x::'a::linordered_field. \<exists>y. \<forall>z>19. y \<le> x + z \<and> (\<exists>w. \<bar>x + z\<bar> < w - y)" |
148 by ferrack |
158 by ferrack |
149 |
159 |
150 lemma "ALL (x::'a::{linordered_field}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" |
160 lemma "\<forall>x::'a::linordered_field. \<exists>y. |
|
161 \<bar>y\<bar> \<noteq> \<bar>x\<bar> \<and> (\<forall>z > max x y. \<exists>w. w \<noteq> y \<and> w \<noteq> z \<and> 3 * w - z \<ge> x + y)" |
151 by ferrack |
162 by ferrack |
152 |
163 |
153 end |
164 end |