diff -r e7504bfdbd50 -r b3add51e2e0f prio/Moment.thy
--- a/prio/Moment.thy	Fri Apr 13 13:12:43 2012 +0000
+++ b/prio/Moment.thy	Sun Apr 15 21:53:12 2012 +0000
@@ -112,12 +112,37 @@
 qed
 
 lemma moment_restm_s: "(restm n s)@(moment n s) = s"
-by (metis firstn_restn_s moment_def restm_def rev_append rev_rev_ident)
+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]
 
 lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"
-by (metis firstn_ge)
+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)
@@ -141,26 +166,78 @@
 lemma app_firstn_restn: 
   fixes s1 s2
   shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)"
-by (metis append_eq_conv_conj firstn_ge firstn_le firstn_restn_s le_refl)
+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_moment_le:
   fixes k s
   assumes le_k: "k \<le> length s"
   shows "length (moment k s) = k"
-by (metis assms length_firstn_le length_rev moment_def)
+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)"
-by (metis app_firstn_restn length_rev moment_def restm_def rev_append rev_rev_ident)
+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
 
 lemma length_moment_ge:
   fixes k s
   assumes le_k: "length s \<le> k"
   shows "length (moment k s) = (length s)"
-by (metis assms firstn_ge length_rev moment_def)
+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
 
 lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"
-by (metis length_firstn_ge length_firstn_le nat_le_linear)
+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 firstn_conc: 
   fixes m n
@@ -193,7 +270,45 @@
   fixes i j k s
   assumes eq_k: "j + i = k"
   shows "restn k s = restn j (restn i s)"
-by (metis app_moment_restm append_take_drop_id assms drop_drop length_drop moment_def restn.simps)
+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
 
 (*
 value "down_to 2 0 [5, 4, 3, 2, 1, 0]"
@@ -204,12 +319,28 @@
 by (simp add:from_to_def restn.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"
-by (metis assms firstn_le length_rev moment_def rev_append)
+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
 
 lemma moment_eq [simp]: "moment (length s) (s'@s) = s"
-by (metis app_moment_restm)
+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
 
 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"
   by (unfold moment_def, simp)
@@ -403,16 +534,42 @@
   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"
-by (metis down_to_def from_to_conc le_ij le_jk rev_append)
+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 = []"
-by (metis assms diff_is_0_eq moment_def moment_zero restn.simps)
+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 = []"
-by (metis firstn_nil from_to_def restn_ge)
+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]"
@@ -423,31 +580,166 @@
   fixes k j s
   assumes le_j: "length s \<le> j"
   shows "from_to k j s = restn k s"
-by (metis app_moment_restm append_Nil2 append_take_drop_id assms diff_is_0_eq' drop_take firstn_restn_s from_to_def length_drop moment_def moment_zero restn.simps)
+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"
-by (metis down_to_def from_to_firstn moment_def)
+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"
-by (metis assms down_to_def from_to_restn length_rev restm_def)
+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"
-by (metis down_to_conc down_to_moment le0 le_add1 nat_add_commute)
+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"
-by (metis diff_le_self length_firstn_le length_rev restn.simps)
+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"
-by (metis diff_le_mono from_to_def le_j length_firstn_le length_restn)
+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)"
-by (metis diff_add_inverse2 from_to_def)
+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
@@ -457,9 +749,25 @@
 lemma moment_plus_split:
   fixes m i s
   shows "moment (m + i) s = moment m (restm i s) @ moment i s"
-by (metis down_to_moment down_to_moment_restm moment_split)
+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"
-by (metis length_restn length_rev restm_def)
+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
 
 end
\ No newline at end of file