# HG changeset patch
# User nipkow
# Date 1149767393 -7200
# Node ID fafceecebef002c7391ef7258cc722ae1f68d9a0
# Parent  9e4573eaacb3c12ee4081c706f1a43ae0ed3f9d9
added John's example

diff -r 9e4573eaacb3 -r fafceecebef0 src/HOL/ex/PresburgerEx.thy
--- a/src/HOL/ex/PresburgerEx.thy	Thu Jun 08 13:49:39 2006 +0200
+++ b/src/HOL/ex/PresburgerEx.thy	Thu Jun 08 13:49:53 2006 +0200
@@ -88,4 +88,18 @@
 theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2"
   by presburger
 
+text{* 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 5 minutes! *}
+
+lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
+         x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
+         x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
+ \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
+by arith
+
 end