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 "\m n ja ia. \\ m \ j; \ n \ i; e \ 0; Suc j \ ja\ \ \m. \ja ia. m \ ja \ (if j = ja \ i = ia then e else 0) = 0" by presburger chaieb@23323 13 lemma "(0::nat) < emBits mod 8 \ 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8" chaieb@23323 14 by presburger chaieb@23323 15 lemma "(0::nat) < emBits mod 8 \ 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8" chaieb@23323 16 by presburger berghofe@13880 17 paulson@14353 18 theorem "(\(y::int). 3 dvd y) ==> \(x::int). b < x --> a \ 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 (\(x::int). 2*x = y) & (\(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) ==> (\(x::int). 2*x = y) & (\(k::int). 3*k = z)" berghofe@13880 27 by presburger berghofe@13880 28 webertj@15075 29 theorem "\(x::nat). \(y::nat). (0::nat) \ 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 "\(x::nat). \(y::nat). y = 5 + x | x div 6 + 1= 2" webertj@15075 34 by presburger webertj@15075 35 webertj@15075 36 theorem "\(x::int). 0 < x" berghofe@13880 37 by presburger berghofe@13880 38 webertj@15075 39 theorem "\(x::int) y. x < y --> 2 * x + 1 < 2 * y" webertj@15075 40 by presburger berghofe@13880 41 webertj@15075 42 theorem "\(x::int) y. 2 * x + 1 \ 2 * y" webertj@15075 43 by presburger berghofe@13880 44 webertj@15075 45 theorem "\(x::int) y. 0 < x & 0 \ y & 3 * x - 5 * y = 1" webertj@15075 46 by presburger berghofe@13880 47 paulson@14353 48 theorem "~ (\(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" berghofe@13880 49 by presburger berghofe@13880 50 paulson@14353 51 theorem "\(x::int). b < x --> a \ x" chaieb@23323 52 apply (presburger elim) berghofe@13880 53 oops berghofe@13880 54 paulson@14353 55 theorem "~ (\(x::int). False)" berghofe@13880 56 by presburger berghofe@13880 57 paulson@14353 58 theorem "\(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 "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" webertj@15075 63 by presburger berghofe@13880 64 webertj@15075 65 theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" webertj@15075 66 by presburger berghofe@13880 67 webertj@15075 68 theorem "\(x::int). (2 dvd x) = (\(y::int). x = 2*y)" webertj@15075 69 by presburger paulson@14353 70 webertj@15075 71 theorem "\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y + 1))" webertj@15075 72 by presburger berghofe@13880 73 paulson@14353 74 theorem "~ (\(x::int). paulson@14353 75 ((2 dvd x) = (\(y::int). x \ 2*y+1) | paulson@14353 76 (\(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 "~ (\(i::int). 4 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" berghofe@13880 81 by presburger berghofe@13880 82 webertj@15075 83 theorem "\(i::int). 8 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" paulson@14353 84 by presburger berghofe@13880 85 webertj@15075 86 theorem "\(j::int). \i. j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" webertj@15075 87 by presburger webertj@15075 88 webertj@15075 89 theorem "~ (\j (i::int). j \ i --> (\x y. 0 \ x & 0 \ 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 "(\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 "\ 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 \ nipkow@19824 107 \ x1 = x10 & x2 = (x11::int)" nipkow@19824 108 by arith nipkow@19824 109 webertj@15075 110 end