author wenzelm Sat Jun 25 14:25:10 2011 +0200 (2011-06-25) changeset 43542 7e2ef426c960 parent 43541 a1ed0456b7e6 child 43544 6b95bcc5c2da
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;
1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sat Jun 25 12:57:46 2011 +0200
1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sat Jun 25 14:25:10 2011 +0200
1.3 @@ -384,44 +384,6 @@
1.4      by (simp add: around_zero.simps[of "i + 1"])
1.5  qed
1.7 -lemma
1.8 -  assumes "int n <= 2 * i"
1.9 -  shows "(n mod 2 = 1 --> around_zero i ! n = (int n + 1) div 2) &
1.10 -    (n mod 2 = 0 --> around_zero i ! n = (- (int n)) div 2)"
1.11 -using assms
1.12 -proof (cases "i >= 0")
1.13 -  case False
1.14 -  with assms show ?thesis by (simp add: around_zero.simps[of i])
1.15 -next
1.16 -  case True
1.17 -  from assms show ?thesis
1.18 -  proof (induct rule:  int_ge_induct[OF True])
1.19 -    case (2 i)
1.20 -    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"
1.21 -      by arith
1.22 -    show ?case
1.23 -    proof -
1.24 -      {
1.25 -        assume "n mod 2 = 1"
1.26 -        from 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = (int n + 1) div 2"
1.27 -          unfolding around_zero.simps[of "i + 1"]
1.28 -          by (auto simp add: nth_append)
1.29 -      } moreover
1.30 -      {
1.31 -        assume a: "n mod 2 = 0"
1.32 -        have "\<forall> q q'. 2 * q \<noteq> Suc (2 * q')" by arith
1.33 -        from a 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = - int n div 2"
1.34 -          unfolding around_zero.simps[of "i + 1"]
1.35 -          by (auto simp add: nth_append)
1.36 -      }
1.37 -      ultimately show ?thesis by auto
1.38 -    qed
1.39 -   next
1.40 -     case 1
1.41 -     from 1 show ?case by (auto simp add: around_zero.simps[of 0])
1.42 -  qed
1.43 -qed
1.44 -
1.45  instantiation int :: narrowing
1.46  begin