author | chaieb |
Thu, 03 Jan 2008 10:27:40 +0100 | |
changeset 25801 | 331d8ce79ee2 |
parent 24402 | 382f67ffbda5 |
child 29705 | a1ecdd8cf81c |
permissions | -rw-r--r-- |
13880 | 1 |
(* Title: HOL/ex/PresburgerEx.thy |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb, TU Muenchen |
|
17388 | 4 |
*) |
13880 | 5 |
|
17388 | 6 |
header {* Some examples for Presburger Arithmetic *} |
13880 | 7 |
|
23462 | 8 |
theory PresburgerEx |
24402 | 9 |
imports Presburger |
23462 | 10 |
begin |
23323 | 11 |
|
25801 | 12 |
lemma "\<And>m n ja ia. \<lbrakk>\<not> m \<le> j; \<not> (n::nat) \<le> i; (e::nat) \<noteq> 0; Suc j \<le> ja\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>ja ia. m \<le> ja \<longrightarrow> (if j = ja \<and> i = ia then e else 0) = 0" by presburger |
23323 | 13 |
lemma "(0::nat) < emBits mod 8 \<Longrightarrow> 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8" |
14 |
by presburger |
|
15 |
lemma "(0::nat) < emBits mod 8 \<Longrightarrow> 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8" |
|
16 |
by presburger |
|
13880 | 17 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
18 |
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x" |
13880 | 19 |
by presburger |
20 |
||
21 |
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
|
22 |
(\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
13880 | 23 |
by presburger |
24 |
||
25 |
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
|
26 |
2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
13880 | 27 |
by presburger |
28 |
||
15075 | 29 |
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x " |
13880 | 30 |
by presburger |
31 |
||
20663 | 32 |
text{*Slow: about 7 seconds on a 1.6GHz machine.*} |
15075 | 33 |
theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2" |
34 |
by presburger |
|
35 |
||
36 |
theorem "\<exists>(x::int). 0 < x" |
|
13880 | 37 |
by presburger |
38 |
||
15075 | 39 |
theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" |
40 |
by presburger |
|
13880 | 41 |
|
15075 | 42 |
theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" |
43 |
by presburger |
|
13880 | 44 |
|
15075 | 45 |
theorem "\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" |
46 |
by presburger |
|
13880 | 47 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
48 |
theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
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). b < x --> a \<le> x" |
23323 | 52 |
apply (presburger elim) |
13880 | 53 |
oops |
54 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
55 |
theorem "~ (\<exists>(x::int). False)" |
13880 | 56 |
by presburger |
57 |
||
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
58 |
theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x" |
23323 | 59 |
apply (presburger elim) |
13880 | 60 |
oops |
61 |
||
15075 | 62 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" |
63 |
by presburger |
|
13880 | 64 |
|
15075 | 65 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" |
66 |
by presburger |
|
13880 | 67 |
|
15075 | 68 |
theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" |
69 |
by presburger |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
70 |
|
15075 | 71 |
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" |
72 |
by presburger |
|
13880 | 73 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
74 |
theorem "~ (\<forall>(x::int). |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13880
diff
changeset
|
75 |
((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
|
76 |
(\<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
|
77 |
--> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
13880 | 78 |
by presburger |
79 |
||
15075 | 80 |
theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
13880 | 81 |
by presburger |
82 |
||
15075 | 83 |
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
|
84 |
by presburger |
13880 | 85 |
|
15075 | 86 |
theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
87 |
by presburger |
|
88 |
||
89 |
theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
|
13880 | 90 |
by presburger |
91 |
||
20663 | 92 |
text{*Slow: about 5 seconds on a 1.6GHz machine.*} |
15075 | 93 |
theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" |
94 |
by presburger |
|
13880 | 95 |
|
19824 | 96 |
text{* This following theorem proves that all solutions to the |
97 |
recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with |
|
98 |
period 9. The example was brought to our attention by John |
|
99 |
Harrison. It does does not require Presburger arithmetic but merely |
|
100 |
quantifier-free linear arithmetic and holds for the rationals as well. |
|
101 |
||
20663 | 102 |
Warning: it takes (in 2006) over 4.2 minutes! *} |
19824 | 103 |
|
104 |
lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3; |
|
105 |
x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6; |
|
106 |
x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk> |
|
107 |
\<Longrightarrow> x1 = x10 & x2 = (x11::int)" |
|
108 |
by arith |
|
109 |
||
15075 | 110 |
end |