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.6  
     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
    1.47