diff -r 17305a85493d -r c495eb16beb6 Moment.thy~ --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Moment.thy~ Wed Jan 27 19:28:42 2016 +0800 @@ -0,0 +1,225 @@ +theory Moment +imports Main +begin + +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]" +value "moment 2 [5, 4, 3, 2, 1, 0::int]" + +(* +lemma length_moment_le: + assumes le_k: "k \ 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 \ k" + shows "length (moment k s) = (length s)" +using assms unfolding moment_def by simp +*) + +lemma moment_app [simp]: + assumes ile: "i \ length 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" + unfolding moment_def by simp + +lemma moment_ge [simp]: "length s \ n \ moment n s = s" + by (unfold moment_def, simp) + +lemma moment_zero [simp]: "moment 0 s = []" + by (simp add:moment_def) + +lemma p_split_gen: + "\Q s; \ Q (moment k s)\ \ + (\ i. i < length s \ k \ i \ \ Q (moment i s) \ (\ i' > i. Q (moment i' s)))" +proof (induct s, simp) + fix a s + assume ih: "\Q s; \ Q (moment k s)\ + \ \i i \ \ Q (moment i s) \ (\i'>i. Q (moment i' s))" + and nq: "\ Q (moment k (a # s))" and qa: "Q (a # s)" + have le_k: "k \ length s" + proof - + { assume "length s < k" + hence "length (a#s) \ k" by simp + from moment_ge [OF this] and nq and qa + have "False" by auto + } thus ?thesis by arith + qed + have nq_k: "\ Q (moment k s)" + proof - + have "moment k (a#s) = moment k s" + proof - + from moment_app [OF le_k, of "[a]"] show ?thesis by simp + qed + with nq show ?thesis by simp + qed + show "\i i \ \ Q (moment i (a # s)) \ (\i'>i. Q (moment i' (a # s)))" + proof - + { assume "Q s" + from ih [OF this nq_k] + obtain i where lti: "i < length s" + and nq: "\ Q (moment i s)" + and rst: "\i'>i. Q (moment i' s)" + and lki: "k \ i" by auto + have ?thesis + proof - + from lti have "i < length (a # s)" by auto + moreover have " \ Q (moment i (a # s))" + proof - + from lti have "i \ (length s)" by simp + from moment_app [OF this, of "[a]"] + have "moment i (a # s) = moment i s" by simp + with nq show ?thesis by auto + qed + moreover have " (\i'>i. Q (moment i' (a # s)))" + proof - + { + fix i' + assume lti': "i < i'" + have "Q (moment i' (a # s))" + proof(cases "length (a#s) \ i'") + case True + from True have "moment i' (a#s) = a#s" by simp + with qa show ?thesis by simp + next + case False + from False have "i' \ length s" by simp + from moment_app [OF this, of "[a]"] + have "moment i' (a#s) = moment i' s" by simp + with rst lti' show ?thesis by auto + qed + } thus ?thesis by auto + qed + moreover note lki + ultimately show ?thesis by auto + qed + } moreover { + assume ns: "\ Q s" + have ?thesis + proof - + let ?i = "length s" + have "\ Q (moment ?i (a#s))" + proof - + have "?i \ length s" by simp + from moment_app [OF this, of "[a]"] + have "moment ?i (a#s) = moment ?i s" by simp + moreover have "\ = s" by simp + ultimately show ?thesis using ns by auto + qed + moreover have "\ i' > ?i. Q (moment i' (a#s))" + proof - + { fix i' + assume "i' > ?i" + hence "length (a#s) \ i'" by simp + from moment_ge [OF this] + have " moment i' (a # s) = a # s" . + with qa have "Q (moment i' (a#s))" by simp + } thus ?thesis by auto + qed + moreover have "?i < length (a#s)" by simp + moreover note le_k + ultimately show ?thesis by auto + qed + } ultimately show ?thesis by auto + qed +qed + +lemma p_split: + "\Q s; \ Q []\ \ + (\ i. i < length s \ \ Q (moment i s) \ (\ i' > i. Q (moment i' s)))" +proof - + fix s Q + assume qs: "Q s" and nq: "\ Q []" + from nq have "\ Q (moment 0 s)" by simp + from p_split_gen [of Q s 0, OF qs this] + show "(\ i. i < length s \ \ Q (moment i s) \ (\ i' > i. Q (moment i' s)))" + by auto +qed + +lemma moment_Suc_tl: + assumes "Suc i \ length s" + shows "tl (moment (Suc i) s) = moment i s" + using assms unfolding moment_def rev_take +by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) + +lemma moment_plus: + assumes "Suc i \ length s" + shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" +proof - + have "(moment (Suc i) s) \ []" + using assms by (auto simp add: moment_def) + hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" + by auto +<<<<<<< local + 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 moment_Suc_tl: + assumes "Suc i \ length s" + shows "tl (moment (Suc i) s) = moment i s" + using assms unfolding moment_def rev_take + by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) + +lemma moment_plus': + assumes "Suc i \ length s" + shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" +proof - + have "(moment (Suc i) s) \ []" + using assms length_moment_le by fastforce + hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" + by auto + with moment_Suc_tl[OF assms] + show ?thesis by metis +qed + +lemma moment_plus: + "Suc i \ length s \ moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" +proof(induct s, simp+) + fix a s + assume ih: "Suc i \ length s \ moment (Suc i) s = hd (moment (Suc i) s) # moment i s" + and le_i: "i \ length s" + show "moment (Suc i) (a # s) = hd (moment (Suc i) (a # s)) # moment i (a # s)" + proof(cases "i= length s") + case True + hence "Suc i = length (a#s)" by simp + with moment_eq have "moment (Suc i) (a#s) = a#s" by auto + moreover have "moment i (a#s) = s" + proof - + from moment_app [OF le_i, of "[a]"] + and True show ?thesis by simp + qed + ultimately show ?thesis by auto + next + case False + from False and le_i have lti: "i < length s" by arith + hence les_i: "Suc i \ length s" by arith + show ?thesis + proof - + from moment_app [OF les_i, of "[a]"] + have "moment (Suc i) (a # s) = moment (Suc i) s" by simp + moreover have "moment i (a#s) = moment i s" + proof - + from lti have "i \ length s" by simp + from moment_app [OF this, of "[a]"] show ?thesis by simp + qed + moreover note ih [OF les_i] + ultimately show ?thesis by auto + qed + qed +======= + with moment_Suc_tl[OF assms] + show ?thesis by metis +>>>>>>> other +qed + +end +