# HG changeset patch
# User berghofe
# Date 1048582253 -3600
# Node ID 4f7f30f6892629b7b763e18eac76fc25c09f6d48
# Parent  92c0973ac730cdc64fbdab4f1c8d4ec522bb5029
Added examples for Presburger arithmetic.

diff -r 92c0973ac730 -r 4f7f30f68926 src/HOL/ex/PresburgerEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/PresburgerEx.thy	Tue Mar 25 09:50:53 2003 +0100
@@ -0,0 +1,86 @@
+(*  Title:      HOL/ex/PresburgerEx.thy
+    ID:         $Id$
+    Author:     Amine Chaieb, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Some examples for Presburger Arithmetic
+*)
+
+theory PresburgerEx = Main:
+
+theorem "(ALL (y::int). (3 dvd y)) ==> ALL (x::int). b < x --> a <= x"
+  by presburger
+
+theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
+  (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
+  by presburger
+
+theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
+  2 dvd (y::int) ==> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
+  by presburger
+
+theorem "ALL (x::nat). EX (y::nat). (0::nat) <= 5 --> y = 5 + x ";
+  by presburger
+
+theorem "ALL (x::nat). EX (y::nat). y = 5 + x | x div 6 + 1= 2";
+  by presburger
+
+theorem "EX (x::int). 0 < x" by presburger
+
+theorem "ALL (x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
+ 
+theorem "ALL (x::int) y. ~(2 * x + 1 = 2 * y)" by presburger
+ 
+theorem
+   "EX (x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1" by presburger
+
+theorem "~ (EX (x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+  by presburger
+
+theorem "ALL (x::int). b < x --> a <= x"
+  apply (presburger no_quantify)
+  oops
+
+theorem "ALL (x::int). b < x --> a <= x"
+  apply (presburger no_quantify)
+  oops
+
+theorem "~ (EX (x::int). False)"
+  by presburger
+
+theorem "ALL (x::int). (a::int) < 3 * x --> b < 3 * x"
+  apply (presburger no_quantify)
+  oops
+
+theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger 
+
+theorem "ALL (x::int). (2 dvd x) --> (EX (y::int). x = 2*y)" by presburger 
+
+theorem "ALL (x::int). (2 dvd x) = (EX (y::int). x = 2*y)" by presburger 
+  
+theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger 
+
+theorem "ALL (x::int). ((2 dvd x) = (ALL (y::int). ~(x = 2*y + 1)))" by presburger 
+
+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))))"
+  by presburger
+ 
+theorem 
+   "~ (ALL (i::int). 4 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+  by presburger
+
+theorem
+    "ALL (i::int). 8 <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i)" by presburger
+   
+theorem
+   "EX (j::int). (ALL (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" by presburger
+
+theorem
+   "~ (ALL j (i::int). j <= i --> (EX (x::int) y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+  by presburger
+
+theorem "(EX m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
+
+theorem "(EX m::int. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
+
+end
\ No newline at end of file
diff -r 92c0973ac730 -r 4f7f30f68926 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Mar 25 09:49:45 2003 +0100
+++ b/src/HOL/ex/ROOT.ML	Tue Mar 25 09:50:53 2003 +0100
@@ -23,6 +23,7 @@
 time_use     "cla.ML";
 time_use     "mesontest.ML";
 time_use_thy "mesontest2";
+time_use_thy "PresburgerEx";
 time_use_thy "BT";
 time_use_thy "AVL";
 time_use_thy "InSort";