src/HOL/ex/PresburgerEx.thy

--- a/src/HOL/ex/PresburgerEx.thy	Thu Sep 21 17:39:57 2006 +0200
+++ b/src/HOL/ex/PresburgerEx.thy	Thu Sep 21 19:04:12 2006 +0200
@@ -21,7 +21,7 @@
 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
   by presburger
 
-text{*Very slow: about 55 seconds on a 1.8GHz machine.*}
+text{*Slow: about 7 seconds on a 1.6GHz machine.*}
 theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"
   by presburger
 
@@ -81,20 +81,17 @@
 theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
   by presburger
 
-text{*Very slow: about 80 seconds on a 1.8GHz machine.*}
+text{*Slow: about 5 seconds on a 1.6GHz machine.*}
 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
   by presburger
 
-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! *}
+Warning: it takes (in 2006) over 4.2 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;