summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 08 Jun 2006 13:49:53 +0200 | |

changeset 19824 | fafceecebef0 |

parent 19823 | 9e4573eaacb3 |

child 19825 | bb5357536621 |

added John's example

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