src/HOL/ex/PresburgerEx.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 61945 1135b8de26c3 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Title:      HOL/ex/PresburgerEx.thy
```
```     2     Author:     Amine Chaieb, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>Some examples for Presburger Arithmetic\<close>
```
```     6
```
```     7 theory PresburgerEx
```
```     8 imports Presburger
```
```     9 begin
```
```    10
```
```    11 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
```
```    12 lemma "(0::nat) < emBits mod 8 \<Longrightarrow> 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8"
```
```    13 by presburger
```
```    14 lemma "(0::nat) < emBits mod 8 \<Longrightarrow> 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8"
```
```    15 by presburger
```
```    16
```
```    17 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
```
```    18   by presburger
```
```    19
```
```    20 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
```
```    21   (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
```
```    22   by presburger
```
```    23
```
```    24 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
```
```    25   2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
```
```    26   by presburger
```
```    27
```
```    28 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
```
```    29   by presburger
```
```    30
```
```    31 text\<open>Slow: about 7 seconds on a 1.6GHz machine.\<close>
```
```    32 theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"
```
```    33   by presburger
```
```    34
```
```    35 theorem "\<exists>(x::int). 0 < x"
```
```    36   by presburger
```
```    37
```
```    38 theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
```
```    39   by presburger
```
```    40
```
```    41 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
```
```    42   by presburger
```
```    43
```
```    44 theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
```
```    45   by presburger
```
```    46
```
```    47 theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
```
```    48   by presburger
```
```    49
```
```    50 theorem "\<forall>(x::int). b < x --> a \<le> x"
```
```    51   apply (presburger elim)
```
```    52   oops
```
```    53
```
```    54 theorem "~ (\<exists>(x::int). False)"
```
```    55   by presburger
```
```    56
```
```    57 theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
```
```    58   apply (presburger elim)
```
```    59   oops
```
```    60
```
```    61 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
```
```    62   by presburger
```
```    63
```
```    64 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
```
```    65   by presburger
```
```    66
```
```    67 theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
```
```    68   by presburger
```
```    69
```
```    70 theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
```
```    71   by presburger
```
```    72
```
```    73 theorem "~ (\<forall>(x::int).
```
```    74             ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
```
```    75              (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
```
```    76              --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
```
```    77   by presburger
```
```    78
```
```    79 theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
```
```    80   by presburger
```
```    81
```
```    82 theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
```
```    83   by presburger
```
```    84
```
```    85 theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
```
```    86   by presburger
```
```    87
```
```    88 theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
```
```    89   by presburger
```
```    90
```
```    91 text\<open>Slow: about 5 seconds on a 1.6GHz machine.\<close>
```
```    92 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
```
```    93   by presburger
```
```    94
```
```    95 text\<open>This following theorem proves that all solutions to the
```
```    96 recurrence relation \$x_{i+2} = |x_{i+1}| - x_i\$ are periodic with
```
```    97 period 9.  The example was brought to our attention by John
```
```    98 Harrison. It does does not require Presburger arithmetic but merely
```
```    99 quantifier-free linear arithmetic and holds for the rationals as well.
```
```   100
```
```   101 Warning: it takes (in 2006) over 4.2 minutes!\<close>
```
```   102
```
```   103 lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
```
```   104          x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
```
```   105          x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
```
```   106  \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
```
```   107 by arith
```
```   108
```
```   109 end
```