# HG changeset patch # User chaieb # Date 1181552783 -7200 # Node ID 2274edb9a8b2132039803165c7f2fd5d2e096100 # Parent 6693a45a226c41c515ac396184dba9ad7f3ee211 Added more examples diff -r 6693a45a226c -r 2274edb9a8b2 src/HOL/ex/PresburgerEx.thy --- a/src/HOL/ex/PresburgerEx.thy Mon Jun 11 11:06:21 2007 +0200 +++ b/src/HOL/ex/PresburgerEx.thy Mon Jun 11 11:06:23 2007 +0200 @@ -5,7 +5,13 @@ header {* Some examples for Presburger Arithmetic *} -theory PresburgerEx imports Main begin +theory PresburgerEx imports Presburger begin + +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 +lemma "(0::nat) < emBits mod 8 \ 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8" +by presburger +lemma "(0::nat) < emBits mod 8 \ 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8" +by presburger theorem "(\(y::int). 3 dvd y) ==> \(x::int). b < x --> a \ x" by presburger @@ -41,14 +47,14 @@ by presburger theorem "\(x::int). b < x --> a \ x" - apply (presburger (no_quantify)) + apply (presburger elim) oops theorem "~ (\(x::int). False)" by presburger theorem "\(x::int). (a::int) < 3 * x --> b < 3 * x" - apply (presburger (no_quantify)) + apply (presburger elim) oops theorem "\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)"