diff -r 5d8ec128518b -r e3cf792db636 Attic/Moment.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Moment.thy	Tue Jun 14 15:06:16 2016 +0100
@@ -0,0 +1,105 @@
+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 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 least_idx:
+  assumes "Q (i::nat)"
+  obtains j where "j \<le> i" "Q j" "\<forall> k < j. \<not> Q k"
+  using assms
+  by (metis ex_least_nat_le le0 not_less0) 
+
+lemma duration_idx:
+  assumes "\<not> Q (i::nat)"
+  and "Q j"
+  and "i \<le> j"
+  obtains k where "i \<le> k" "k < j" "\<not> Q k" "\<forall> i'. k < i' \<and> i' \<le> j \<longrightarrow> Q i'" 
+proof -
+  let ?Q = "\<lambda> t. t \<le> j \<and> \<not> Q (j - t)"
+  have "?Q (j - i)" using assms by (simp add: assms(1)) 
+  from least_idx [of ?Q, OF this]
+  obtain l
+  where h: "l \<le> j - i" "\<not> Q (j - l)" "\<forall>k<l. \<not> (k \<le> j \<and> \<not> Q (j - k))"
+    by metis
+  let ?k = "j - l"
+  have "i \<le> ?k" using assms(3) h(1) by linarith 
+  moreover have "?k < j" by (metis assms(2) diff_le_self h(2) le_neq_implies_less) 
+  moreover have "\<not> Q ?k" by (simp add: h(2)) 
+  moreover have "\<forall> i'. ?k < i' \<and> i' \<le> j \<longrightarrow> Q i'"
+      by (metis diff_diff_cancel diff_le_self diff_less_mono2 h(3) 
+              less_imp_diff_less not_less) 
+  ultimately show ?thesis using that by metis
+qed
+
+lemma p_split_gen: 
+  assumes "Q s"
+  and "\<not> Q (moment k s)"
+  shows "(\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
+proof(cases "k \<le> length s")
+  case True
+  let ?Q = "\<lambda> t. Q (moment t s)"
+  have "?Q (length s)" using assms(1) by simp
+  from duration_idx[of ?Q, OF assms(2) this True]
+  obtain i where h: "k \<le> i" "i < length s" "\<not> Q (moment i s)"
+    "\<forall>i'. i < i' \<and> i' \<le> length s \<longrightarrow> Q (moment i' s)" by metis
+  moreover have "(\<forall> i' > i. Q (moment i' s))" using h(4) assms(1) not_less
+    by fastforce
+  ultimately show ?thesis by metis
+qed (insert assms, auto)
+
+lemma p_split: 
+  assumes qs: "Q s"
+  and nq: "\<not> Q []"
+  shows "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"
+proof -
+  from nq have "\<not> Q (moment 0 s)" by simp
+  from p_split_gen [of Q s 0, OF qs this]
+  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 
+  by (simp add:moment_def rev_take, 
+      metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
+
+lemma moment_Suc_hd:
+  assumes "Suc i \<le> length s"
+  shows "hd (moment (Suc i) s) = s!(length s - Suc i)"
+  by (simp add:moment_def rev_take, 
+      subst hd_drop_conv_nth, insert assms, auto)
+  
+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 (simp add:moment_def rev_take)
+  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
+
+end
+