--- a/Moment.thy~ Thu Jan 28 21:14:17 2016 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-theory Moment
-imports Main
-begin
-
-definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> '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 \<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"
-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 \<le> n \<Longrightarrow> 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:
- "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow>
- (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
-proof (induct s, simp)
- fix a s
- assume ih: "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk>
- \<Longrightarrow> \<exists>i<length s. k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall>i'>i. Q (moment i' s))"
- and nq: "\<not> Q (moment k (a # s))" and qa: "Q (a # s)"
- have le_k: "k \<le> length s"
- proof -
- { assume "length s < k"
- hence "length (a#s) \<le> k" by simp
- from moment_ge [OF this] and nq and qa
- have "False" by auto
- } thus ?thesis by arith
- qed
- have nq_k: "\<not> 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 "\<exists>i<length (a # s). k \<le> i \<and> \<not> Q (moment i (a # s)) \<and> (\<forall>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: "\<not> Q (moment i s)"
- and rst: "\<forall>i'>i. Q (moment i' s)"
- and lki: "k \<le> i" by auto
- have ?thesis
- proof -
- from lti have "i < length (a # s)" by auto
- moreover have " \<not> Q (moment i (a # s))"
- proof -
- from lti have "i \<le> (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 " (\<forall>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) \<le> 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' \<le> 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: "\<not> Q s"
- have ?thesis
- proof -
- let ?i = "length s"
- have "\<not> Q (moment ?i (a#s))"
- proof -
- have "?i \<le> length s" by simp
- from moment_app [OF this, of "[a]"]
- have "moment ?i (a#s) = moment ?i s" by simp
- moreover have "\<dots> = s" by simp
- ultimately show ?thesis using ns by auto
- qed
- moreover have "\<forall> i' > ?i. Q (moment i' (a#s))"
- proof -
- { fix i'
- assume "i' > ?i"
- hence "length (a#s) \<le> 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:
- "\<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow>
- (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
-proof -
- fix s Q
- assume qs: "Q s" and nq: "\<not> Q []"
- from nq have "\<not> Q (moment 0 s)" by simp
- from p_split_gen [of Q s 0, OF qs this]
- show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
- by auto
-qed
-
-lemma moment_Suc_tl:
- assumes "Suc i \<le> 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 \<le> length s"
- shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)"
-proof -
- have "(moment (Suc i) s) \<noteq> []"
- 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 \<le> 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 \<le> length s"
- shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)"
-proof -
- have "(moment (Suc i) s) \<noteq> []"
- 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 \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)"
-proof(induct s, simp+)
- fix a s
- assume ih: "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = hd (moment (Suc i) s) # moment i s"
- and le_i: "i \<le> 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 \<le> 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 \<le> 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
-