author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14758 | af3b71a46a1c |
child 15075 | a6cd1a454751 |
permissions | -rw-r--r-- |
13880 | 1 |
(* Title: HOL/ex/PresburgerEx.thy |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb, TU Muenchen |
|
4 |
||
5 |
Some examples for Presburger Arithmetic |
|
6 |
*) |
|
7 |
||
8 |
theory PresburgerEx = Main: |
|
9 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
10 |
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x" |
13880 | 11 |
by presburger |
12 |
||
13 |
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==> |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
14 |
(\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
13880 | 15 |
by presburger |
16 |
||
17 |
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==> |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
18 |
2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
13880 | 19 |
by presburger |
20 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
21 |
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "; |
13880 | 22 |
by presburger |
23 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
24 |
text{*Very slow: about 55 seconds on a 1.8GHz machine.*} |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
25 |
theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"; |
13880 | 26 |
by presburger |
27 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
28 |
theorem "\<exists>(x::int). 0 < x" by presburger |
13880 | 29 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
30 |
theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger |
13880 | 31 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
32 |
theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" by presburger |
13880 | 33 |
|
34 |
theorem |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
35 |
"\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" by presburger |
13880 | 36 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
37 |
theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
13880 | 38 |
by presburger |
39 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
40 |
theorem "\<forall>(x::int). b < x --> a \<le> x" |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
41 |
apply (presburger (no_quantify)) |
13880 | 42 |
oops |
43 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
44 |
theorem "\<forall>(x::int). b < x --> a \<le> x" |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
45 |
apply (presburger (no_quantify)) |
13880 | 46 |
oops |
47 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
48 |
theorem "~ (\<exists>(x::int). False)" |
13880 | 49 |
by presburger |
50 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
51 |
theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x" |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14353
diff
changeset
|
52 |
apply (presburger (no_quantify)) |
13880 | 53 |
oops |
54 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
55 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger |
13880 | 56 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
57 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger |
13880 | 58 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
59 |
theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" by presburger |
13880 | 60 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
61 |
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
62 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
63 |
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" by presburger |
13880 | 64 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
65 |
theorem "~ (\<forall>(x::int). |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
66 |
((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
67 |
(\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
68 |
--> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
13880 | 69 |
by presburger |
70 |
||
71 |
theorem |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
72 |
"~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
13880 | 73 |
by presburger |
74 |
||
75 |
theorem |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
76 |
"\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
77 |
by presburger |
13880 | 78 |
|
79 |
theorem |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
80 |
"\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
81 |
by presburger |
13880 | 82 |
|
83 |
theorem |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
84 |
"~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
13880 | 85 |
by presburger |
86 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
87 |
text{*Very slow: about 80 seconds on a 1.8GHz machine.*} |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
88 |
theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
13880 | 89 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
90 |
theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger |
13880 | 91 |
|
92 |
end |