src/HOL/ex/PresburgerEx.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 19824 fafceecebef0 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     1 (*  Title:      HOL/ex/PresburgerEx.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Amine Chaieb, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* Some examples for Presburger Arithmetic *}
```
```     7
```
```     8 theory PresburgerEx imports Main begin
```
```     9
```
```    10 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
```
```    11   by presburger
```
```    12
```
```    13 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
```
```    14   (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
```
```    15   by presburger
```
```    16
```
```    17 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
```
```    18   2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
```
```    19   by presburger
```
```    20
```
```    21 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
```
```    22   by presburger
```
```    23
```
```    24 text{*Very slow: about 55 seconds on a 1.8GHz machine.*}
```
```    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"
```
```    29   by presburger
```
```    30
```
```    31 theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
```
```    32   by presburger
```
```    33
```
```    34 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
```
```    35   by presburger
```
```    36
```
```    37 theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
```
```    38   by presburger
```
```    39
```
```    40 theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
```
```    41   by presburger
```
```    42
```
```    43 theorem "\<forall>(x::int). b < x --> a \<le> x"
```
```    44   apply (presburger (no_quantify))
```
```    45   oops
```
```    46
```
```    47 theorem "~ (\<exists>(x::int). False)"
```
```    48   by presburger
```
```    49
```
```    50 theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
```
```    51   apply (presburger (no_quantify))
```
```    52   oops
```
```    53
```
```    54 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
```
```    55   by presburger
```
```    56
```
```    57 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
```
```    58   by presburger
```
```    59
```
```    60 theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
```
```    61   by presburger
```
```    62
```
```    63 theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
```
```    64   by presburger
```
```    65
```
```    66 theorem "~ (\<forall>(x::int).
```
```    67             ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
```
```    68              (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
```
```    69              --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
```
```    70   by presburger
```
```    71
```
```    72 theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
```
```    73   by presburger
```
```    74
```
```    75 theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
```
```    76   by presburger
```
```    77
```
```    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))"
```
```    82   by presburger
```
```    83
```
```    84 text{*Very slow: about 80 seconds on a 1.8GHz machine.*}
```
```    85 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
```
```    86   by presburger
```
```    87
```
```    88 theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2"
```
```    89   by presburger
```
```    90
```
```    91 end
```