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