src/HOL/ex/PresburgerEx.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 25801 331d8ce79ee2
child 29705 a1ecdd8cf81c
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     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
     9 imports Presburger
    10 begin
    11 
    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
    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
    17 
    18 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
    19   by presburger
    20 
    21 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
    22   (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
    23   by presburger
    24 
    25 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
    26   2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
    27   by presburger
    28 
    29 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
    30   by presburger
    31 
    32 text{*Slow: about 7 seconds on a 1.6GHz machine.*}
    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"
    37   by presburger
    38 
    39 theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
    40   by presburger
    41  
    42 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
    43   by presburger
    44  
    45 theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
    46   by presburger
    47 
    48 theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
    49   by presburger
    50 
    51 theorem "\<forall>(x::int). b < x --> a \<le> x"
    52   apply (presburger elim)
    53   oops
    54 
    55 theorem "~ (\<exists>(x::int). False)"
    56   by presburger
    57 
    58 theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
    59   apply (presburger elim)
    60   oops
    61 
    62 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
    63   by presburger 
    64 
    65 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
    66   by presburger 
    67 
    68 theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
    69   by presburger 
    70 
    71 theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
    72   by presburger 
    73 
    74 theorem "~ (\<forall>(x::int). 
    75             ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | 
    76              (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
    77              --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
    78   by presburger
    79  
    80 theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
    81   by presburger
    82 
    83 theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
    84   by presburger
    85 
    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))"
    90   by presburger
    91 
    92 text{*Slow: about 5 seconds on a 1.6GHz machine.*}
    93 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
    94   by presburger
    95 
    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 
   102 Warning: it takes (in 2006) over 4.2 minutes! *}
   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 
   110 end