2584 lemma length_down_to_in: 

  2585   assumes le_ij: "i \<le> j"

  2586     and le_js: "j \<le> length s"

  2587   shows "length (down_to j i s) = j - i"

  2588 proof -

  2589   have "length (down_to j i s) = length (from_to i j (rev s))"

  2590     by (unfold down_to_def, auto)

  2591   also have "\<dots> = j - i"

  2592   proof(rule length_from_to_in[OF le_ij])

  2593     from le_js show "j \<le> length (rev s)" by simp

  2594   qed

  2595   finally show ?thesis .

  2596 qed

  2597 

  2598 

  2599 lemma moment_head: 

  2600   assumes le_it: "Suc i \<le> length t"

  2601   obtains e where "moment (Suc i) t = e#moment i t"

  2602 proof -

  2603   have "i \<le> Suc i" by simp

  2604   from length_down_to_in [OF this le_it]

  2605   have "length (down_to (Suc i) i t) = 1" by auto

  2606   then obtain e where "down_to (Suc i) i t = [e]"

  2607     apply (cases "(down_to (Suc i) i t)") by auto

  2608   moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"

  2609     by (rule down_to_conc[symmetric], auto)

  2610   ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"

  2611     by (auto simp:down_to_moment)

  2612   from that [OF this] show ?thesis .

  2613 qed