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