(*  Title:      HOL/ex/PresburgerEx.thy
    Author:     Amine Chaieb, TU Muenchen
*)

section ‹Some examples for Presburger Arithmetic›

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) ==>
  (∃(x::int). 2*x = y) & (∃(k::int). 3*k = z)"
  by presburger

theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==>
  2 dvd (y::int) ==> (∃(x::int). 2*x = y) & (∃(k::int). 3*k = z)"
  by presburger

theorem "∀(x::nat). ∃(y::nat). (0::nat) ≤ 5 --> y = 5 + x "
  by presburger

text‹Slow: about 7 seconds on a 1.6GHz machine.›
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) (y::int) (z::int). 4*x + (-6::int)*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) = (∀(y::int). x ≠ 2*y+1) |
             (∃(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))"span>
  by presburger

theorem "∀(i::int). 8 ≤ i --> (∃x y. 0 ≤ x & 0 ≤ y & 3 * x + 5 * y = i)"n>
  by presburger

theorem "∃(j::int). ∀i. j ≤ i --> (∃x y. 0 ≤ x & 0 ≤ y & 3 * x + 5 * y = i)"</span>
  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‹This following theorem proves that all solutions to the
  relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
  9. The example was brought to our attention by John
 . It does does not require Presburger arithmetic but merely
 -free linear arithmetic and holds for the rationals as well.

 : it takes (in 2006) over 4.2 minutes!›

lemma "[ x3 = ∣x2∣ - x1; x4 = ∣x3∣ - x2; x5 = ∣x4∣ - x3;
         x6 = ∣x5∣ - x4; x7 = ∣x6∣ - x5; x8 = ∣x7∣ - x6;
         x9 = ∣x8∣ - x7; x10 = ∣x9∣ - x8; x11 = ∣x10∣ - x9 ]
 ==> x1 = x10 & x2 = (x11::int)"
by arith

end