--- a/Moment.thy	Wed Jan 13 14:20:58 2016 +0000
+++ b/Moment.thy	Wed Jan 13 15:16:59 2016 +0000
@@ -5,27 +5,22 @@
 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where "moment n s = rev (take n (rev s))"
 
-definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where "restm n s = rev (drop n (rev s))"
-
 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
 value "moment 2 [5, 4, 3, 2, 1, 0::int]"
 
-value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
-
-lemma moment_restm_s: "(restm n s) @ (moment n s) = s"
-  unfolding restm_def moment_def
-by (metis append_take_drop_id rev_append rev_rev_ident)
-
+(*
 lemma length_moment_le:
   assumes le_k: "k \<le> length s"
   shows "length (moment k s) = k"
 using le_k unfolding moment_def by auto
+*)
 
+(*
 lemma length_moment_ge:
   assumes le_k: "length s \<le> k"
   shows "length (moment k s) = (length s)"
 using assms unfolding moment_def by simp
+*)
 
 lemma moment_app [simp]:
   assumes ile: "i \<le> length s"
@@ -148,56 +143,23 @@
     by auto
 qed
 
-lemma moment_plus_split:
-  shows "moment (m + i) s = moment m (restm i s) @ moment i s"
-unfolding moment_def restm_def
-by (metis add.commute rev_append rev_rev_ident take_add)
+lemma moment_Suc_tl:
+  assumes "Suc i \<le> length s"
+  shows "tl (moment (Suc i) s) = moment i s"
+  using assms unfolding moment_def
+sorry
 
-lemma moment_prefix: 
-  "(moment i t @ s) = moment (i + length s) (t @ s)"
-proof -
-  from moment_plus_split [of i "length s" "t@s"]
-  have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"
-    by auto
-  have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" 
-    by (simp add: moment_def)
-  with moment_app show ?thesis by auto
-qed
 
-lemma moment_plus: 
-  "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)"
-proof(induct s, simp+)
-  fix a s
-  assume ih: "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = hd (moment (Suc i) s) # moment i s"
-    and le_i: "i \<le> length s"
-  show "moment (Suc i) (a # s) = hd (moment (Suc i) (a # s)) # moment i (a # s)"
-  proof(cases "i= length s")
-    case True
-    hence "Suc i = length (a#s)" by simp
-    with moment_eq have "moment (Suc i) (a#s) = a#s" by auto
-    moreover have "moment i (a#s) = s"
-    proof -
-      from moment_app [OF le_i, of "[a]"]
-      and True show ?thesis by simp
-    qed
-    ultimately show ?thesis by auto
-  next
-    case False
-    from False and le_i have lti: "i < length s" by arith
-    hence les_i: "Suc i \<le> length s" by arith
-    show ?thesis 
-    proof -
-      from moment_app [OF les_i, of "[a]"]
-      have "moment (Suc i) (a # s) = moment (Suc i) s" by simp
-      moreover have "moment i (a#s) = moment i s" 
-      proof -
-        from lti have "i \<le> length s" by simp
-        from moment_app [OF this, of "[a]"] show ?thesis by simp
-      qed
-      moreover note ih [OF les_i]
-      ultimately show ?thesis by auto
-    qed
-  qed
+lemma moment_plus:
+  assumes "Suc i \<le> length s"
+  shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)"
+proof -
+  have "(moment (Suc i) s) \<noteq> []"
+  using assms by (auto simp add: moment_def)
+  hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) #  tl (moment (Suc i) s)"
+    by auto
+  with moment_Suc_tl[OF assms]
+  show ?thesis by metis
 qed
 
 end