# HG changeset patch
# User zhangx
# Date 1452704154 -28800
# Node ID 83ba2d8c859a6412e008241cd13d8eff4fc8cc22
# Parent  b0054fb0d1ce765c3cdb3a8134ffc53946b4a357
Moment.thy further simplified.

diff -r b0054fb0d1ce -r 83ba2d8c859a Moment.thy
--- a/Moment.thy	Wed Jan 13 23:39:59 2016 +0800
+++ b/Moment.thy	Thu Jan 14 00:55:54 2016 +0800
@@ -36,118 +36,66 @@
 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
+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: 
-  "\<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)))"
+  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 -
-  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
+  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)
+  using assms 
+  by (simp add:moment_def rev_take, 
+      metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
   
 lemma moment_plus:
   assumes "Suc i \<le> length s"