--- a/Moment.thy Thu Jan 14 00:55:54 2016 +0800
+++ b/Moment.thy Thu Jan 14 03:29:22 2016 +0000
@@ -8,20 +8,6 @@
value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
value "moment 2 [5, 4, 3, 2, 1, 0::int]"
-(*
-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"
shows "moment i (s' @ s) = moment i s"