|
1 (* Title: HOL/ex/PresburgerEx.thy |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Some examples for Presburger Arithmetic |
|
7 *) |
|
8 |
|
9 theory PresburgerEx = Main: |
|
10 |
|
11 theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x" |
|
12 by presburger |
|
13 |
|
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)" |
|
16 by presburger |
|
17 |
|
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)" |
|
20 by presburger |
|
21 |
|
22 theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x "; |
|
23 by presburger |
|
24 |
|
25 theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2"; |
|
26 by presburger |
|
27 |
|
28 theorem "EX (x::int). 0 < x" by presburger |
|
29 |
|
30 theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger |
|
31 |
|
32 theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger |
|
33 |
|
34 theorem |
|
35 "EX (x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" by presburger |
|
36 |
|
37 theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
|
38 by presburger |
|
39 |
|
40 theorem "ALL (x::int). b < x --> a <= x" |
|
41 apply (presburger no_quantify) |
|
42 oops |
|
43 |
|
44 theorem "ALL (x::int). b < x --> a <= x" |
|
45 apply (presburger no_quantify) |
|
46 oops |
|
47 |
|
48 theorem "~ (EX (x::int). False)" |
|
49 by presburger |
|
50 |
|
51 theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x" |
|
52 apply (presburger no_quantify) |
|
53 oops |
|
54 |
|
55 theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger |
|
56 |
|
57 theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger |
|
58 |
|
59 theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger |
|
60 |
|
61 theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger |
|
62 |
|
63 theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger |
|
64 |
|
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 by presburger |
|
67 |
|
68 theorem |
|
69 "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" |
|
70 by presburger |
|
71 |
|
72 theorem |
|
73 "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger |
|
74 |
|
75 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 |
|
77 |
|
78 theorem |
|
79 "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" |
|
80 by presburger |
|
81 |
|
82 theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
|
83 |
|
84 theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
|
85 |
|
86 end |