4471 by auto

  4471 by auto

  4472 

  4472 

  4473 lemma tape_of_nat_list_butlast_last:

  4473 lemma tape_of_nat_list_butlast_last:

  4474   "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y"

  4474   "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y"

  4475 apply(induct ys, simp, simp)

  4475 apply(induct ys, simp, simp)

  4477                                     tape_of_nat_list.simps)

  4477                                     tape_of_nat_list.simps)

  4479 done

  4479 done

  4480 

  4480 

  4481 lemma listsum2_append:

  4481 lemma listsum2_append:

  4482   "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> listsum2 (xs @ ys) n = listsum2 xs n"

  4482   "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> listsum2 (xs @ ys) n = listsum2 xs n"

  4483 apply(induct n)

  4483 apply(induct n)

  4516     done

  4516     done

  4517   thus "length (<xs @ [x]>) =

  4517   thus "length (<xs @ [x]>) =

  4518     Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"

  4518     Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"

  4519     apply(case_tac "xs = []")

  4519     apply(case_tac "xs = []")

  4520     apply(simp add: tape_of_nl_abv listsum2.simps 

  4520     apply(simp add: tape_of_nl_abv listsum2.simps 

  4522     apply(simp add: tape_of_nat_list_butlast_last)

  4522     apply(simp add: tape_of_nat_list_butlast_last)

  4523     using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]

  4523     using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]

  4524     apply(simp)

  4524     apply(simp)

  4525     done

  4525     done

  4526 next

  4526 next