diff -r d5e9653fbf19 -r 43482ab31341 Moment.thy.orig
--- a/Moment.thy.orig	Wed Feb 03 21:41:42 2016 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +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))"
-
-definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where "restm n s = rev (drop 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]"
-
-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)
-
-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_plus_split:
-  shows "moment (m + i) s = moment m (restm i s) @ moment i s"
-unfolding moment_def restm_def
-by (metis add.commute rev_append rev_rev_ident take_add)
-
-lemma moment_prefix: 
-  "(moment i t @ s) = moment (i + length s) (t @ s)"
-proof -
-  from moment_plus_split [of i "length s" "t@s"]
-  have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"
-    by auto
-  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_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
-qed
-
-end
-