# HG changeset patch
# User wenzelm
# Date 1309004710 -7200
# Node ID 7e2ef426c9607e03c82babdc394b2b1e93ef3671
# Parent  a1ed0456b7e6abdc581dbb9f8e4a028af345fe0a
removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;

diff -r a1ed0456b7e6 -r 7e2ef426c960 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Sat Jun 25 12:57:46 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sat Jun 25 14:25:10 2011 +0200
@@ -384,44 +384,6 @@
     by (simp add: around_zero.simps[of "i + 1"])
 qed
 
-lemma
-  assumes "int n <= 2 * i"
-  shows "(n mod 2 = 1 --> around_zero i ! n = (int n + 1) div 2) &
-    (n mod 2 = 0 --> around_zero i ! n = (- (int n)) div 2)"
-using assms
-proof (cases "i >= 0")
-  case False
-  with assms show ?thesis by (simp add: around_zero.simps[of i])
-next
-  case True
-  from assms show ?thesis
-  proof (induct rule:  int_ge_induct[OF True])
-    case (2 i)
-    have i: "n < Suc (2 * nat i) \<or> n = Suc (2 * nat i) \<or> n = (2 * nat i) + 2 \<or> n > (2 * nat i) + 2"
-      by arith
-    show ?case    
-    proof -
-      {
-        assume "n mod 2 = 1"
-        from 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = (int n + 1) div 2"
-          unfolding around_zero.simps[of "i + 1"]
-          by (auto simp add: nth_append)
-      } moreover
-      {
-        assume a: "n mod 2 = 0"
-        have "\<forall> q q'. 2 * q \<noteq> Suc (2 * q')" by arith
-        from a 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = - int n div 2"
-          unfolding around_zero.simps[of "i + 1"]
-          by (auto simp add: nth_append)
-      }
-      ultimately show ?thesis by auto
-    qed
-   next
-     case 1
-     from 1 show ?case by (auto simp add: around_zero.simps[of 0])
-  qed
-qed
-
 instantiation int :: narrowing
 begin