diff -r 1dc801552dfd -r 92ca2410b3d9 Moment.thy --- a/Moment.thy Wed Jan 13 13:20:45 2016 +0000 +++ b/Moment.thy Wed Jan 13 14:20:58 2016 +0000 @@ -5,36 +5,18 @@ definition moment :: "nat \ 'a list \ 'a list" where "moment n s = rev (take n (rev s))" -value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" - definition restm :: "nat \ 'a list \ 'a list" 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 \ nat \ 'a list \ 'a list" - where "from_to i j s = take (j - i) (drop i 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]" -definition down_to :: "nat \ nat \ 'a list \ '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]" - -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]" - +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) -declare drop.simps [simp del] - -lemma length_take_le: - "n \ length s \ length (take n s) = n" -by (metis length_take min.absorb2) - lemma length_moment_le: assumes le_k: "k \ length s" shows "length (moment k s) = k" @@ -45,29 +27,12 @@ shows "length (moment k s) = (length s)" using assms unfolding moment_def by simp -lemma length_take: - "(length (take n s) = length s) \ (length (take n s) = n)" -by (metis length_take min_def) - -lemma take_conc: - assumes le_mn: "m \ n" - 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_take: "from_to 0 k s = take k s" -by (simp add:from_to_def drop.simps) - lemma moment_app [simp]: assumes ile: "i \ length s" - shows "moment i (s'@s) = moment i s" + shows "moment i (s' @ s) = moment i s" using assms unfolding moment_def by simp -lemma moment_eq [simp]: "moment (length s) (s'@s) = s" +lemma moment_eq [simp]: "moment (length s) (s' @ s) = s" unfolding moment_def by simp lemma moment_ge [simp]: "length s \ n \ moment n s = s" @@ -172,7 +137,7 @@ qed lemma p_split: - "\ s Q. \Q s; \ Q []\ \ + "\Q s; \ Q []\ \ (\ i. i < length s \ \ Q (moment i s) \ (\ i' > i. Q (moment i' s)))" proof - fix s Q @@ -183,20 +148,6 @@ 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 @@ -213,32 +164,6 @@ with moment_app show ?thesis by auto qed -lemma length_down_to_in: - assumes le_ij: "i \ j" - and le_js: "j \ 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 \ length t" - obtains e where "moment (Suc i) t = e#moment i t" -proof - - have "i \ 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 \ length s \ moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" proof(induct s, simp+) @@ -276,3 +201,4 @@ qed end +