author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 15075 | a6cd1a454751 |
child 16417 | 9bc16273c2d4 |
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 |
||
15075 | 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.*} |
15075 | 25 |
theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2" |
26 |
by presburger |
|
27 |
||
28 |
theorem "\<exists>(x::int). 0 < x" |
|
13880 | 29 |
by presburger |
30 |
||
15075 | 31 |
theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" |
32 |
by presburger |
|
13880 | 33 |
|
15075 | 34 |
theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" |
35 |
by presburger |
|
13880 | 36 |
|
15075 | 37 |
theorem "\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" |
38 |
by presburger |
|
13880 | 39 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
40 |
theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
13880 | 41 |
by presburger |
42 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
43 |
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
|
44 |
apply (presburger (no_quantify)) |
13880 | 45 |
oops |
46 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
47 |
theorem "~ (\<exists>(x::int). False)" |
13880 | 48 |
by presburger |
49 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
50 |
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
|
51 |
apply (presburger (no_quantify)) |
13880 | 52 |
oops |
53 |
||
15075 | 54 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" |
55 |
by presburger |
|
13880 | 56 |
|
15075 | 57 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" |
58 |
by presburger |
|
13880 | 59 |
|
15075 | 60 |
theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" |
61 |
by presburger |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
62 |
|
15075 | 63 |
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" |
64 |
by presburger |
|
13880 | 65 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
66 |
theorem "~ (\<forall>(x::int). |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
67 |
((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
|
68 |
(\<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
|
69 |
--> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
13880 | 70 |
by presburger |
71 |
||
15075 | 72 |
theorem "~ (\<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 |
||
15075 | 75 |
theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
76 |
by presburger |
13880 | 77 |
|
15075 | 78 |
theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
79 |
by presburger |
|
80 |
||
81 |
theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
|
13880 | 82 |
by presburger |
83 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
84 |
text{*Very slow: about 80 seconds on a 1.8GHz machine.*} |
15075 | 85 |
theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" |
86 |
by presburger |
|
13880 | 87 |
|
15075 | 88 |
theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" |
89 |
by presburger |
|
13880 | 90 |
|
15075 | 91 |
end |