1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/PresburgerEx.thy	Tue Mar 25 09:50:53 2003 +0100
     1.3 @@ -0,0 +1,86 @@
     1.4 +(*  Title:      HOL/ex/PresburgerEx.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Some examples for Presburger Arithmetic
    1.10 +*)
    1.11 +
    1.12 +theory PresburgerEx = Main:
    1.13 +
    1.14 +theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x"
    1.15 +  by presburger
    1.16 +
    1.17 +theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
    1.18 +  (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
    1.19 +  by presburger
    1.20 +
    1.21 +theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
    1.22 +  2 dvd (y::int) ==> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
    1.23 +  by presburger
    1.24 +
    1.25 +theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x ";
    1.26 +  by presburger
    1.27 +
    1.28 +theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2";
    1.29 +  by presburger
    1.30 +
    1.31 +theorem "EX (x::int). 0 < x" by presburger
    1.32 +
    1.33 +theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
    1.34 + 
    1.35 +theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger
    1.36 + 
    1.37 +theorem
    1.38 +   "EX (x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1" by presburger
    1.39 +
    1.40 +theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
    1.41 +  by presburger
    1.42 +
    1.43 +theorem "ALL (x::int). b < x --> a <= x"
    1.44 +  apply (presburger no_quantify)
    1.45 +  oops
    1.46 +
    1.47 +theorem "ALL (x::int). b < x --> a <= x"
    1.48 +  apply (presburger no_quantify)
    1.49 +  oops
    1.50 +
    1.51 +theorem "~ (EX (x::int). False)"
    1.52 +  by presburger
    1.53 +
    1.54 +theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x"
    1.55 +  apply (presburger no_quantify)
    1.56 +  oops
    1.57 +
    1.58 +theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger 
    1.59 +
    1.60 +theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger 
    1.61 +
    1.62 +theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger 
    1.63 +  
    1.64 +theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger 
    1.65 +
    1.66 +theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger 
    1.67 +
    1.68 +theorem "~ (ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y+1))| (EX (q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
    1.69 +  by presburger
    1.70 + 
    1.71 +theorem 
    1.72 +   "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
    1.73 +  by presburger
    1.74 +
    1.75 +theorem
    1.76 +    "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger
    1.77 +   
    1.78 +theorem
    1.79 +   "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" by presburger
    1.80 +
    1.81 +theorem
    1.82 +   "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
    1.83 +  by presburger
    1.84 +
    1.85 +theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
    1.86 +
    1.87 +theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
    1.88 +
    1.89 +end
    1.90 \ No newline at end of file

     2.1 --- a/src/HOL/ex/ROOT.ML	Tue Mar 25 09:49:45 2003 +0100
     2.2 +++ b/src/HOL/ex/ROOT.ML	Tue Mar 25 09:50:53 2003 +0100
     2.3 @@ -23,6 +23,7 @@
     2.4  time_use     "cla.ML";
     2.5  time_use     "mesontest.ML";
     2.6  time_use_thy "mesontest2";
     2.7 +time_use_thy "PresburgerEx";
     2.8  time_use_thy "BT";
     2.9  time_use_thy "AVL";
    2.10  time_use_thy "InSort";