--- a/PIPBasics.thy	Tue Jan 12 08:35:36 2016 +0800
+++ b/PIPBasics.thy	Wed Jan 13 13:20:45 2016 +0000
@@ -2581,36 +2581,6 @@
   qed
 qed
 
-lemma length_down_to_in: 
-  assumes le_ij: "i \<le> j"
-    and le_js: "j \<le> length s"
-  shows "length (down_to j i s) = j - i"
-proof -
-  have "length (down_to j i s) = length (from_to i j (rev s))"
-    by (unfold down_to_def, auto)
-  also have "\<dots> = j - i"
-  proof(rule length_from_to_in[OF le_ij])
-    from le_js show "j \<le> length (rev s)" by simp
-  qed
-  finally show ?thesis .
-qed
-
-
-lemma moment_head: 
-  assumes le_it: "Suc i \<le> length t"
-  obtains e where "moment (Suc i) t = e#moment i t"
-proof -
-  have "i \<le> Suc i" by simp
-  from length_down_to_in [OF this le_it]
-  have "length (down_to (Suc i) i t) = 1" by auto
-  then obtain e where "down_to (Suc i) i t = [e]"
-    apply (cases "(down_to (Suc i) i t)") by auto
-  moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
-    by (rule down_to_conc[symmetric], auto)
-  ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
-    by (auto simp:down_to_moment)
-  from that [OF this] show ?thesis .
-qed
 
 context valid_trace
 begin