diff -r db196b066b97 -r 1dc801552dfd Moment.thy
--- a/Moment.thy	Tue Jan 12 08:35:36 2016 +0800
+++ b/Moment.thy	Wed Jan 13 13:20:45 2016 +0000
@@ -2,108 +2,18 @@
 imports Main
 begin
 
-fun firstn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "firstn 0 s = []" |
-  "firstn (Suc n) [] = []" |
-  "firstn (Suc n) (e#s) = e#(firstn n s)"
-
-lemma upto_map_plus: "map (op + k) [i..j] = [i+k..j+k]"
-proof(induct "[i..j]" arbitrary:i j rule:length_induct)
-  case (1 i j)
-  thus ?case
-  proof(cases "i \<le> j")
-    case True
-    hence le_k: "i + k \<le> j + k" by simp
-    show ?thesis (is "?L = ?R")
-    proof -
-      have "?L  = (k + i) # map (op + k) [i + 1..j]"
-         by (simp add: upto_rec1[OF True])
-      moreover have "?R = (i + k) # [i + k + 1..j + k]"
-        by (simp add: upto_rec1[OF le_k])
-      moreover have "map (op + k) [i + 1..j] = [i + k + 1..j + k]"
-      proof -
-        have h: "i + k + 1 = (i + 1) + k" by simp
-        show ?thesis
-        proof(unfold h, rule 1[rule_format])
-          show "length [i + 1..j] < length [i..j]"
-            using upto_rec1[OF True] by simp
-        qed simp
-      qed
-      ultimately show ?thesis by simp
-    qed
-  qed auto
-qed
+definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where "moment n s = rev (take n (rev s))"
 
-lemma firstn_alt_def:
-  "firstn n s = map (\<lambda> i. s!(nat i)) [0..(int (min (length s) n)) - 1]"
-proof(induct n arbitrary:s)
-  case (0 s)
-  thus ?case by auto
-next
-  case (Suc n s)
-  thus ?case (is "?L = ?R")
-  proof(cases s)
-    case Nil
-    thus ?thesis by simp
-  next
-    case (Cons e es)
-    with Suc 
-    have "?L =  e # map (\<lambda>i. es ! nat i) [0..int (min (length es) n) - 1]"
-      by simp
-    also have "... = map (\<lambda>i. (e # es) ! nat i) [0..int (min (length es) n)]"
-      (is "?L1 = ?R1")
-    proof -
-      have "?R1 =   e # map (\<lambda>i. (e # es) ! nat i) 
-                            [1..int (min (length es) n)]" 
-      proof -
-        have "[0..int (min (length es) n)] = 0#[1..int (min (length es) n)]"
-          by (simp add: upto.simps)
-        thus ?thesis by simp
-      qed
-      also have "... = ?L1" (is "_#?L2 = _#?R2")
-      proof -
-        have "?L2 = ?R2"
-        proof -
-          have "map (\<lambda>i. (e # es) ! nat i) [1..int (min (length es) n)] =  
-                map ((\<lambda>i. (e # es) ! nat i) \<circ> op + 1) [0..int (min (length es) n) - 1]" 
-          proof -
-            have "[1..int (min (length es) n)] = 
-                             map (op + 1) [0..int (min (length es) n) - 1]"
-                     by (unfold upto_map_plus, simp)
-            thus ?thesis by simp
-          qed
-          also have "... = map (\<lambda>i. es ! nat i) [0..int (min (length es) n) - 1]"
-          proof(rule map_cong)
-            fix x
-            assume "x \<in> set [0..int (min (length es) n) - 1]"
-            thus "((\<lambda>i. (e # es) ! nat i) \<circ> op + 1) x = es ! nat x"
-              by (metis atLeastLessThan_iff atLeastLessThan_upto 
-                    comp_apply local.Cons nat_0_le nat_int nth_Cons_Suc of_nat_Suc)
-          qed auto
-          finally show ?thesis .
-        qed
-        thus ?thesis by simp
-      qed
-      finally show ?thesis by simp
-    qed
-    also have "... = ?R"
-      by (unfold Cons, simp)
-    finally show ?thesis .
-  qed
-qed
-
-fun restn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where "restn n s = rev (firstn (length s - n) (rev s))"
-
-definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where "moment n s = rev (firstn n (rev s))"
+value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
 
 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where "restm n s = rev (restn n (rev s))"
+where "restm n s = rev (drop n (rev s))"
+
+value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
 
 definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where "from_to i j s = firstn (j - i) (restn i s)"
+  where "from_to i j s = take (j - i) (drop i s)"
 
 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where "down_to j i s = rev (from_to i j (rev s))"
@@ -111,324 +21,60 @@
 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]"
 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]"
 
-lemma length_eq_elim_l: "\<lbrakk>length xs = length ys; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs"
-  by auto
-
-lemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs"
-  by simp
-
-lemma firstn_nil [simp]: "firstn n [] = []"
-  by (cases n, simp+)
-
-
 value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ 
        from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]"
 
-lemma firstn_le: "\<And> n s'. n \<le> length s \<Longrightarrow> firstn n (s@s') = firstn n s"
-proof (induct s, simp)
-  fix a s n s'
-  assume ih: "\<And>n s'. n \<le> length s \<Longrightarrow> firstn n (s @ s') = firstn n s"
-  and le_n: " n \<le> length (a # s)"
-  show "firstn n ((a # s) @ s') = firstn n (a # s)"
-  proof(cases n, simp)
-    fix k
-    assume eq_n: "n = Suc k"
-    with le_n have "k \<le> length s" by auto
-    from ih [OF this] and eq_n
-    show "firstn n ((a # s) @ s') = firstn n (a # s)" by auto
-  qed
-qed
 
-lemma firstn_ge [simp]: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s"
-proof(induct s, simp)
-  fix a s n
-  assume ih: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s"
-    and le: "length (a # s) \<le> n"
-  show "firstn n (a # s) = a # s"
-  proof(cases n)
-    assume eq_n: "n = 0" with le show ?thesis by simp
-  next
-    fix k
-    assume eq_n: "n = Suc k"
-    with le have le_k: "length s \<le> k" by simp
-    from ih [OF this] have "firstn k s = s" .
-    from eq_n and this
-    show ?thesis by simp
-  qed
-qed
-
-lemma firstn_eq [simp]: "firstn (length s) s = s"
-  by simp
+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 firstn_restn_s: "(firstn n (s::'a list)) @ (restn n s) = s"
-proof(induct n arbitrary:s, simp)
-  fix n s
-  assume ih: "\<And>t. firstn n (t::'a list) @ restn n t = t"
-  show "firstn (Suc n) (s::'a list) @ restn (Suc n) s = s"
-  proof(cases s, simp)
-    fix x xs
-    assume eq_s: "s = x#xs"
-    show "firstn (Suc n) s @ restn (Suc n) s = s"
-    proof -
-      have "firstn (Suc n) s @ restn (Suc n) s =  x # (firstn n xs @ restn n xs)"
-      proof -
-        from eq_s have "firstn (Suc n) s =  x # firstn n xs" by simp
-        moreover have "restn (Suc n) s = restn n xs"
-        proof -
-          from eq_s have "restn (Suc n) s = rev (firstn (length xs - n) (rev xs @ [x]))" by simp
-          also have "\<dots> = restn n xs"
-          proof -
-            have "(firstn (length xs - n) (rev xs @ [x])) = (firstn (length xs - n) (rev xs))"
-              by(rule firstn_le, simp)
-            hence "rev (firstn (length xs - n) (rev xs @ [x])) = 
-              rev (firstn (length xs - n) (rev xs))" by simp
-            also have "\<dots> = rev (firstn (length (rev xs) - n) (rev xs))" by simp
-            finally show ?thesis by simp
-          qed
-          finally show ?thesis by simp
-        qed
-        ultimately show ?thesis by simp
-      qed with ih eq_s show ?thesis by simp
-    qed
-  qed
-qed
-
-lemma moment_restm_s: "(restm n s)@(moment n s) = s"
-proof -
-  have " rev  ((firstn n (rev s)) @ (restn n (rev s))) = s" (is "rev ?x = s")
-  proof -
-    have "?x = rev s" by (simp only:firstn_restn_s)
-    thus ?thesis by auto
-  qed
-  thus ?thesis 
-    by (auto simp:restm_def moment_def)
-qed
-
-declare restn.simps [simp del] firstn.simps[simp del]
+declare drop.simps [simp del] 
 
-lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"
-proof(induct n arbitrary:s, simp add:firstn.simps)
-  case (Suc k)
-  assume ih: "\<And> s. length (s::'a list) \<le> k \<Longrightarrow> length (firstn k s) = length s"
-  and le: "length s \<le> Suc k"
-  show ?case
-  proof(cases s)
-    case Nil
-    from Nil show ?thesis by simp
-  next
-    case (Cons x xs)
-    from le and Cons have "length xs \<le> k" by simp
-    from ih [OF this] have "length (firstn k xs) = length xs" .
-    moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" 
-      by (simp add:firstn.simps)
-    moreover note Cons
-    ultimately show ?thesis by simp
-  qed
-qed
-
-lemma length_firstn_le: "n \<le> length s \<Longrightarrow> length (firstn n s) = n"
-proof(induct n arbitrary:s, simp add:firstn.simps)
-  case (Suc k)
-  assume ih: "\<And>s. k \<le> length (s::'a list) \<Longrightarrow> length (firstn k s) = k"
-    and le: "Suc k \<le> length s"
-  show ?case
-  proof(cases s)
-    case Nil
-    from Nil and le show ?thesis by auto
-  next
-    case (Cons x xs)
-    from le and Cons have "k \<le> length xs" by simp
-    from ih [OF this] have "length (firstn k xs) = k" .
-    moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" 
-      by (simp add:firstn.simps)
-    ultimately show ?thesis by simp
-  qed
-qed
-
-lemma app_firstn_restn: 
-  fixes s1 s2
-  shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)"
-proof(rule length_eq_elim_l)
-  have "length s1 \<le> length (s1 @ s2)" by simp
-  from length_firstn_le [OF this]
-  show "length s1 = length (firstn (length s1) (s1 @ s2))" by simp
-next
-  from firstn_restn_s 
-  show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)"
-    by metis
-qed
-
+lemma length_take_le: 
+  "n \<le> length s \<Longrightarrow> length (take n s) = n"
+by (metis length_take min.absorb2)
 
 lemma length_moment_le:
-  fixes k s
   assumes le_k: "k \<le> length s"
   shows "length (moment k s) = k"
-proof -
-  have "length (rev (firstn k (rev s))) = k"
-  proof -
-    have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp
-    also have "\<dots> = k" 
-    proof(rule length_firstn_le)
-      from le_k show "k \<le> length (rev s)" by simp
-    qed
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:moment_def)
-qed
-
-lemma app_moment_restm: 
-  fixes s1 s2
-  shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)"
-proof(rule length_eq_elim_r)
-  have "length s2 \<le> length (s1 @ s2)" by simp
-  from length_moment_le [OF this]
-  show "length s2 = length (moment (length s2) (s1 @ s2))" by simp
-next
-  from moment_restm_s 
-  show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)"
-    by metis
-qed
+using le_k unfolding moment_def by auto
 
 lemma length_moment_ge:
-  fixes k s
   assumes le_k: "length s \<le> k"
   shows "length (moment k s) = (length s)"
-proof -
-  have "length (rev (firstn k (rev s))) = length s"
-  proof -
-    have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp
-    also have "\<dots> = length s" 
-    proof -
-      have "\<dots> = length (rev s)"
-      proof(rule length_firstn_ge)
-        from le_k show "length (rev s) \<le> k" by simp
-      qed
-      also have "\<dots> = length s" by simp
-      finally show ?thesis .
-    qed
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:moment_def)
-qed
+using assms unfolding moment_def by simp
 
-lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"
-proof(cases "n \<le> length s")
-  case True
-  from length_firstn_le [OF True] show ?thesis by auto
-next
-  case False
-  from False have "length s \<le> n" by simp
-  from firstn_ge [OF this] show ?thesis by auto
-qed
+lemma length_take: 
+  "(length (take n s) = length s) \<or> (length (take n s) = n)"
+by (metis length_take min_def)
 
-lemma firstn_conc: 
-  fixes m n
+lemma take_conc: 
   assumes le_mn: "m \<le> n"
-  shows "firstn m s = firstn m (firstn n  s)"
-proof(cases "m \<le> length s")
-  case True
-  have "s = (firstn n s) @ (restn n s)" by (simp add:firstn_restn_s)
-  hence "firstn m s = firstn m \<dots>" by simp
-  also have "\<dots> = firstn m (firstn n s)" 
-  proof -
-    from length_firstn [of n s]
-    have "m \<le> length (firstn n s)"
-    proof
-      assume "length (firstn n s) = length s" with True show ?thesis by simp
-    next
-      assume "length (firstn n s) = n " with le_mn show ?thesis by simp
-    qed
-    from firstn_le [OF this, of "restn n s"]
-    show ?thesis .
-  qed
-  finally show ?thesis by simp
-next
-  case False
-  from False and le_mn have "length s \<le> n"  by simp
-  from firstn_ge [OF this] show ?thesis by simp
-qed
-
-lemma restn_conc: 
-  fixes i j k s
-  assumes eq_k: "j + i = k"
-  shows "restn k s = restn j (restn i s)"
-proof -
-  have "(firstn (length s - k) (rev s)) =
-        (firstn (length (rev (firstn (length s - i) (rev s))) - j) 
-                            (rev (rev (firstn (length s - i) (rev s)))))"
-  proof  -
-    have "(firstn (length s - k) (rev s)) =
-            (firstn (length (rev (firstn (length s - i) (rev s))) - j) 
-                                           (firstn (length s - i) (rev s)))"
-    proof -
-      have " (length (rev (firstn (length s - i) (rev s))) - j) = length s - k"
-      proof -
-        have "(length (rev (firstn (length s - i) (rev s))) - j) = (length s - i) - j"
-        proof -
-          have "(length (rev (firstn (length s - i) (rev s))) - j) = 
-                                         length ((firstn (length s - i) (rev s))) - j"
-            by simp
-          also have "\<dots> = length ((firstn (length (rev s) - i) (rev s))) - j" by simp
-          also have "\<dots> = (length (rev s) - i) - j" 
-          proof -
-            have "length ((firstn (length (rev s) - i) (rev s))) = (length (rev s) - i)"
-              by (rule length_firstn_le, simp)
-            thus ?thesis by simp
-          qed
-          also have "\<dots> = (length s - i) - j" by simp
-          finally show ?thesis .
-        qed
-        with eq_k show ?thesis by auto
-      qed
-      moreover have "(firstn (length s - k) (rev s)) =
-                             (firstn (length s - k) (firstn (length s - i) (rev s)))"
-      proof(rule firstn_conc)
-        from eq_k show "length s - k \<le> length s - i" by simp
-      qed
-      ultimately show ?thesis by simp
-    qed
-    thus ?thesis by simp
-  qed
-  thus ?thesis by (simp only:restn.simps)
-qed
+  shows "take m s = take m (take n  s)"
+using assms by (metis min.absorb1 take_take) 
 
 (*
 value "down_to 2 0 [5, 4, 3, 2, 1, 0]"
 value "moment 2 [5, 4, 3, 2, 1, 0]"
 *)
 
-lemma from_to_firstn: "from_to 0 k s = firstn k s"
-by (simp add:from_to_def restn.simps)
+lemma from_to_take: "from_to 0 k s = take k s"
+by (simp add:from_to_def drop.simps)
 
 lemma moment_app [simp]:
-  assumes 
-  ile: "i \<le> length s"
+  assumes ile: "i \<le> length s"
   shows "moment i (s'@s) = moment i s"
-proof -
-  have "moment i (s'@s) = rev (firstn i (rev (s'@s)))" by (simp add:moment_def)
-  moreover have "firstn i (rev (s'@s)) = firstn i (rev s @ rev s')" by simp
-  moreover have "\<dots> = firstn i (rev s)"
-  proof(rule firstn_le)
-    have "length (rev s) = length s" by simp
-    with ile show "i \<le> length (rev s)" by simp
-  qed
-  ultimately show ?thesis by (simp add:moment_def)
-qed
+using assms unfolding moment_def by simp
 
 lemma moment_eq [simp]: "moment (length s) (s'@s) = s"
-proof -
-  have "length s \<le> length s" by simp
-  from moment_app [OF this, of s'] 
-  have " moment (length s) (s' @ s) = moment (length s) s" .
-  moreover have "\<dots> = s" by (simp add:moment_def)
-  ultimately show ?thesis by simp
-qed
+  unfolding moment_def by simp
 
 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"
   by (unfold moment_def, simp)
 
 lemma moment_zero [simp]: "moment 0 s = []"
-  by (simp add:moment_def firstn.simps)
+  by (simp add:moment_def)
 
 lemma p_split_gen: 
   "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow>
@@ -537,6 +183,62 @@
     by auto
 qed
 
+(*
+value "from_to 2 5 [0, 1, 2, 3, 4]"
+value "drop 2  [0, 1, 2, 3, 4]"
+*)
+
+(*
+lemma down_to_moment: "down_to k 0 s = moment k s"
+proof -
+  have "rev (from_to 0 k (rev s)) = rev (take k (rev s))" 
+    using from_to_take by metis
+  thus ?thesis by (simp add:down_to_def moment_def)
+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_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 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"
+using assms
+unfolding down_to_def from_to_def
+by (simp)
+
+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 a: "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"
+    unfolding down_to_def from_to_def rev_append[symmetric]
+    apply(simp del: rev_append)
+    by (metis One_nat_def Suc_eq_plus1_left add.commute take_add)
+  ultimately have eq_me: "moment (Suc i) t = e # (moment i t)"
+    by(simp add: moment_def down_to_def from_to_def)
+  from that [OF this] show ?thesis .
+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+)
@@ -573,293 +275,4 @@
   qed
 qed
 
-lemma from_to_conc:
-  fixes i j k s
-  assumes le_ij: "i \<le> j"
-  and le_jk: "j \<le> k"
-  shows "from_to i j s @ from_to j k s = from_to i k s"
-proof -
-  let ?ris = "restn i s"
-  have "firstn (j - i) (restn i s) @ firstn (k - j) (restn j s) =
-         firstn (k - i) (restn i s)" (is "?x @ ?y = ?z")
-  proof -
-    let "firstn (k-j) ?u" = "?y"
-    let ?rst = " restn (k - j) (restn (j - i) ?ris)"
-    let ?rst' = "restn (k - i) ?ris"
-    have "?u = restn (j-i) ?ris"
-    proof(rule restn_conc)
-      from le_ij show "j - i + i = j" by simp
-    qed
-    hence "?x @ ?y = ?x @ firstn (k-j) (restn (j-i) ?ris)" by simp
-    moreover have "firstn (k - j) (restn (j - i) (restn i s)) @ ?rst = 
-                      restn (j-i) ?ris" by (simp add:firstn_restn_s)
-    ultimately have "?x @ ?y @ ?rst = ?x @ (restn (j-i) ?ris)" by simp
-    also have "\<dots> = ?ris" by (simp add:firstn_restn_s)
-    finally have "?x @ ?y @ ?rst = ?ris" .
-    moreover have "?z @ ?rst = ?ris"
-    proof -
-      have "?z @ ?rst' = ?ris" by (simp add:firstn_restn_s)
-      moreover have "?rst' = ?rst"
-      proof(rule restn_conc)
-        from le_ij le_jk show "k - j + (j - i) = k - i" by auto
-      qed
-      ultimately show ?thesis by simp
-    qed
-    ultimately have "?x @ ?y @ ?rst = ?z @ ?rst" by simp
-    thus ?thesis by auto    
-  qed
-  thus ?thesis by (simp only:from_to_def)
-qed
-
-lemma down_to_conc:
-  fixes i j k s
-  assumes le_ij: "i \<le> j"
-  and le_jk: "j \<le> k"
-  shows "down_to k j s @ down_to j i s = down_to k i s"
-proof -
-  have "rev (from_to j k (rev s)) @ rev (from_to i j (rev s)) = rev (from_to i k (rev s))"
-    (is "?L = ?R")
-  proof -
-    have "?L = rev (from_to i j (rev s) @ from_to j k (rev s))" by simp
-    also have "\<dots> = ?R" (is "rev ?x = rev ?y")
-    proof -
-      have "?x = ?y" by (rule from_to_conc[OF le_ij le_jk])
-      thus ?thesis by simp
-    qed
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:down_to_def)
-qed
-
-lemma restn_ge:
-  fixes s k
-  assumes le_k: "length s \<le> k"
-  shows "restn k s = []"
-proof -
-  from firstn_restn_s [of k s, symmetric] have "s = (firstn k s) @ (restn k s)" .
-  hence "length s = length \<dots>" by simp
-  also have "\<dots> = length (firstn k s) + length (restn k s)" by simp
-  finally have "length s = ..." by simp
-  moreover from length_firstn_ge and le_k 
-  have "length (firstn k s) = length s" by simp
-  ultimately have "length (restn k s) = 0" by auto
-  thus ?thesis by auto
-qed
-
-lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []"
-proof(simp only:from_to_def)
-  assume "length s \<le> k"
-  from restn_ge [OF this] 
-  show "firstn (j - k) (restn k s) = []" by simp
-qed
-
-(*
-value "from_to 2 5 [0, 1, 2, 3, 4]"
-value "restn 2  [0, 1, 2, 3, 4]"
-*)
-
-lemma from_to_restn: 
-  fixes k j s
-  assumes le_j: "length s \<le> j"
-  shows "from_to k j s = restn k s"
-proof -
-  have "from_to 0 k s @ from_to k j s = from_to 0 j s"
-  proof(cases "k \<le> j")
-    case True
-    from from_to_conc True show ?thesis by auto
-  next
-    case False
-    from False le_j have lek: "length s \<le>  k" by auto
-    from from_to_ge [OF this] have "from_to k j s = []" .
-    hence "from_to 0 k s @ from_to k j s = from_to 0 k s" by simp
-    also have "\<dots> = s"
-    proof -
-      from from_to_firstn [of k s]
-      have "\<dots> = firstn k s" .
-      also have "\<dots> = s" by (rule firstn_ge [OF lek])
-      finally show ?thesis .
-    qed
-    finally have "from_to 0 k s @ from_to k j s = s" .
-    moreover have "from_to 0 j s = s"
-    proof -
-      have "from_to 0 j s = firstn j s" by (simp add:from_to_firstn)
-      also have "\<dots> = s"
-      proof(rule firstn_ge)
-        from le_j show "length s \<le> j " by simp
-      qed
-      finally show ?thesis .
-    qed
-    ultimately show ?thesis by auto
-  qed
-  also have "\<dots> = s" 
-  proof -
-    from from_to_firstn have "\<dots> = firstn j s" .
-    also have "\<dots> = s"
-    proof(rule firstn_ge)
-      from le_j show "length s \<le> j" by simp
-    qed
-    finally show ?thesis .
-  qed
-  finally have "from_to 0 k s @ from_to k j s = s" .
-  moreover have "from_to 0 k s @ restn k s = s"
-  proof -
-    from from_to_firstn [of k s]
-    have "from_to 0 k s = firstn k s" .
-    thus ?thesis by (simp add:firstn_restn_s)
-  qed
-  ultimately have "from_to 0 k s @ from_to k j s  = 
-                    from_to 0 k s @ restn k s" by simp
-  thus ?thesis by auto
-qed
-
-lemma down_to_moment: "down_to k 0 s = moment k s"
-proof -
-  have "rev (from_to 0 k (rev s)) = rev (firstn k (rev s))" 
-    using from_to_firstn by metis
-  thus ?thesis by (simp add:down_to_def moment_def)
-qed
-
-lemma down_to_restm:
-  assumes le_s: "length s \<le> j"
-  shows "down_to j k s = restm k s"
-proof -
-  have "rev (from_to k j (rev s)) = rev (restn k (rev s))" (is "?L = ?R")
-  proof -
-    from le_s have "length (rev s) \<le> j" by simp
-    from from_to_restn [OF this, of k] show ?thesis by simp
-  qed
-  thus ?thesis by (simp add:down_to_def restm_def)
-qed
-
-lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s"
-proof -
-  have "moment (m + i) s = down_to (m+i) 0 s" using down_to_moment by metis
-  also have "\<dots> = (down_to (m+i) i s) @ (down_to i 0 s)" 
-    by(rule down_to_conc[symmetric], auto)
-  finally show ?thesis .
-qed
-
-lemma length_restn: "length (restn i s) = length s - i"
-proof(cases "i \<le> length s")
-  case True
-  from length_firstn_le [OF this] have "length (firstn i s) = i" .
-  moreover have "length s = length (firstn i s) + length (restn i s)"
-  proof -
-    have "s = firstn i s @ restn i s" using firstn_restn_s by metis
-    hence "length s = length \<dots>" by simp
-    thus ?thesis by simp
-  qed
-  ultimately show ?thesis by simp
-next 
-  case False
-  hence "length s \<le> i" by simp
-  from restn_ge [OF this] have "restn i s = []" .
-  with False show ?thesis by simp
-qed
-
-lemma length_from_to_in:
-  fixes i j s
-  assumes le_ij: "i \<le> j"
-  and le_j: "j \<le> length s"
-  shows "length (from_to i j s) = j - i"
-proof -
-  have "from_to 0 j s = from_to 0 i s @ from_to i j s"
-    by (rule from_to_conc[symmetric, OF _ le_ij], simp)
-  moreover have "length (from_to 0 j s) = j"
-  proof -
-    have "from_to 0 j s = firstn j s" using from_to_firstn by metis
-    moreover have "length \<dots> = j" by (rule length_firstn_le [OF le_j])
-    ultimately show ?thesis by simp
-  qed
-  moreover have "length (from_to 0 i s) = i"
-  proof -
-    have "from_to 0 i s = firstn i s" using from_to_firstn by metis
-    moreover have "length \<dots> = i" 
-    proof (rule length_firstn_le)
-      from le_ij le_j show "i \<le> length s" by simp
-    qed
-    ultimately show ?thesis by simp
-  qed
-  ultimately show ?thesis by auto
-qed
-
-lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)"
-proof(cases "m+i \<le> length s")
-  case True
-  have "restn i s = from_to i (m+i) s @ from_to (m+i) (length s) s"
-  proof -
-    have "restn i s = from_to i (length s) s"
-      by(rule from_to_restn[symmetric], simp)
-    also have "\<dots> = from_to i (m+i) s @ from_to (m+i) (length s) s"
-      by(rule from_to_conc[symmetric, OF _ True], simp)
-    finally show ?thesis .
-  qed
-  hence "firstn m (restn i s) = firstn m \<dots>" by simp
-  moreover have "\<dots> = firstn (length (from_to i (m+i) s)) 
-                    (from_to i (m+i) s @ from_to (m+i) (length s) s)"
-  proof -
-    have "length (from_to i (m+i) s) = m"
-    proof -
-      have "length (from_to i (m+i) s) = (m+i) - i"
-        by(rule length_from_to_in [OF _ True], simp)
-      thus ?thesis by simp
-    qed
-    thus ?thesis by simp
-  qed
-  ultimately show ?thesis using app_firstn_restn by metis
-next
-  case False
-  hence "length s \<le> m + i" by simp
-  from from_to_restn [OF this]
-  have "from_to i (m + i) s = restn i s" .
-  moreover have "firstn m (restn i s) = restn i s" 
-  proof(rule firstn_ge)
-    show "length (restn i s) \<le> m"
-    proof -
-      have "length (restn i s) = length s - i" using length_restn by metis
-      with False show ?thesis by simp
-    qed
-  qed
-  ultimately show ?thesis by simp
-qed
-
-lemma down_to_moment_restm:
-  fixes m i s
-  shows "down_to (m + i) i s = moment m (restm i s)"
-  by (simp add:firstn_restn_from_to down_to_def moment_def restm_def)
-
-lemma moment_plus_split:
-  fixes m i s
-  shows "moment (m + i) s = moment m (restm i s) @ moment i s"
-proof -
-  from moment_split [of m i s]
-  have "moment (m + i) s = down_to (m + i) i s @ down_to i 0 s" .
-  also have "\<dots> = down_to (m+i) i s @ moment i s" using down_to_moment by simp
-  also from down_to_moment_restm have "\<dots> = moment m (restm i s) @ moment i s"
-    by simp
-  finally show ?thesis .
-qed
-
-lemma length_restm: "length (restm i s) = length s - i"
-proof -
-  have "length (rev (restn i (rev s))) = length s - i" (is "?L = ?R")
-  proof -
-    have "?L = length (restn i (rev s))" by simp
-    also have "\<dots>  = length (rev s) - i" using length_restn by metis
-    also have "\<dots> = ?R" by simp
-    finally show ?thesis .
-  qed
-  thus ?thesis by (simp add:restm_def)
-qed
-
-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
-  with app_moment_restm[of t s]
-  have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp
-  with moment_app show ?thesis by auto
-qed
-
 end