--- 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