(* Title: HOL/ex/PresburgerEx.thy Author: Amine Chaieb, TU Muenchen
*)
section \<open>Some examples for Presburger Arithmetic\<close>
theory PresburgerEx imports Main begin
lemma"\m n ja ia. \\ m \ j; \ (n::nat) \ i; (e::nat) \ 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
theorem"!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
(\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" by presburger
theorem"!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==>
2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" by presburger
theorem"\(x::nat). \(y::nat). (0::nat) \ 5 --> y = 5 + x " by presburger
text\<open>Slow: about 7 seconds on a 1.6GHz machine.\<close> theorem"\(x::nat). \(y::nat). y = 5 + x | x div 6 + 1= 2" by presburger
theorem"\(x::int). 0 < x" by presburger
theorem"\(x::int) y. x < y --> 2 * x + 1 < 2 * y" by presburger
theorem"\(x::int) y. 2 * x + 1 \ 2 * y" by presburger
theorem"\(x::int) y. 0 < x & 0 \ y & 3 * x - 5 * y = 1" by presburger
theorem"\(x::int). b < x --> a \ x" apply (presburger elim) oops
theorem"~ (\(x::int). False)" by presburger
theorem"\(x::int). (a::int) < 3 * x --> b < 3 * x" apply (presburger elim) oops
theorem"\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" by presburger
theorem"\(x::int). (2 dvd x) --> (\(y::int). x = 2*y)" by presburger
theorem"\(x::int). (2 dvd x) = (\(y::int). x = 2*y)" by presburger
theorem"\(x::int). ((2 dvd x) = (\(y::int). x \ 2*y + 1))" by presburger
theorem"~ (\(x::int).
((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
(\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
--> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" by presburger
theorem"~ (\(i::int). 4 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" by presburger
theorem"\(i::int). 8 \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" by presburger
theorem"\(j::int). \i. j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i)" by presburger
theorem"~ (\j (i::int). j \ i --> (\x y. 0 \ x & 0 \ y & 3 * x + 5 * y = i))" by presburger
theorem"(\m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" by presburger
text\<open>This following theorem proves that all solutions to the
recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
period 9. The example was brought to our attention by John
Harrison. It does does not require Presburger arithmetic but merely
quantifier-free linear arithmetic and holds for the rationals as well.
Warning: it takes (in 2006) over 4.2 minutes!\<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
