--- a/Moment.thy	Thu Jan 07 22:10:06 2016 +0800
+++ b/Moment.thy	Sat Jan 09 22:19:27 2016 +0800
@@ -8,6 +8,91 @@
   "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
+
+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))"
 
@@ -23,10 +108,8 @@
 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))"
 
-(*
 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
@@ -37,10 +120,9 @@
 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)