6 Some examples for Presburger Arithmetic |
6 Some examples for Presburger Arithmetic |
7 *) |
7 *) |
8 |
8 |
9 theory PresburgerEx = Main: |
9 theory PresburgerEx = Main: |
10 |
10 |
11 theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x" |
11 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x" |
12 by presburger |
12 by presburger |
13 |
13 |
14 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==> |
14 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==> |
15 (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)" |
15 (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
16 by presburger |
16 by presburger |
17 |
17 |
18 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==> |
18 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==> |
19 2 dvd (y::int) ==> (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)" |
19 2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
20 by presburger |
20 by presburger |
21 |
21 |
22 theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x "; |
22 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "; |
23 by presburger |
23 by presburger |
24 |
24 |
25 theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2"; |
25 text{*Very slow: about 55 seconds on a 1.8GHz machine.*} |
|
26 theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"; |
26 by presburger |
27 by presburger |
27 |
28 |
28 theorem "EX (x::int). 0 < x" by presburger |
29 theorem "\<exists>(x::int). 0 < x" by presburger |
29 |
30 |
30 theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger |
31 theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger |
31 |
32 |
32 theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger |
33 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" by presburger |
33 |
34 |
34 theorem |
35 theorem |
35 "EX (x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by presburger |
36 "\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" by presburger |
36 |
37 |
37 theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
38 theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
38 by presburger |
39 by presburger |
39 |
40 |
40 theorem "ALL (x::int). b < x --> a <= x" |
41 theorem "\<forall>(x::int). b < x --> a \<le> x" |
41 apply (presburger no_quantify) |
42 apply (presburger no_quantify) |
42 oops |
43 oops |
43 |
44 |
44 theorem "ALL (x::int). b < x --> a <= x" |
45 theorem "\<forall>(x::int). b < x --> a \<le> x" |
45 apply (presburger no_quantify) |
46 apply (presburger no_quantify) |
46 oops |
47 oops |
47 |
48 |
48 theorem "~ (EX (x::int). False)" |
49 theorem "~ (\<exists>(x::int). False)" |
49 by presburger |
50 by presburger |
50 |
51 |
51 theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x" |
52 theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x" |
52 apply (presburger no_quantify) |
53 apply (presburger no_quantify) |
53 oops |
54 oops |
54 |
55 |
55 theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger |
56 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger |
56 |
57 |
57 theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger |
58 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger |
58 |
59 |
59 theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger |
60 theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" by presburger |
60 |
61 |
61 theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger |
62 theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger |
62 |
63 |
63 theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger |
64 theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger |
64 |
65 |
65 theorem "~ (ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y+1))| (EX (q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
66 theorem "~ (\<forall>(x::int). |
|
67 ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | |
|
68 (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) |
|
69 --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
66 by presburger |
70 by presburger |
67 |
71 |
68 theorem |
72 theorem |
69 "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" |
73 "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
70 by presburger |
74 by presburger |
71 |
75 |
72 theorem |
76 theorem |
73 "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger |
77 "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
|
78 by presburger |
74 |
79 |
75 theorem |
80 theorem |
76 "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" by presburger |
81 "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
|
82 by presburger |
77 |
83 |
78 theorem |
84 theorem |
79 "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" |
85 "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
80 by presburger |
86 by presburger |
81 |
87 |
82 theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
88 text{*Very slow: about 80 seconds on a 1.8GHz machine.*} |
|
89 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
83 |
90 |
84 theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
91 theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
85 |
92 |
86 end |
93 end |