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