# 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"