--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Happen_within.thy Tue Jan 24 00:20:09 2012 +0000
@@ -0,0 +1,126 @@
+theory Happen_within
+imports Main Moment
+begin
+
+(*
+ lemma
+ fixes P :: "('a list) \<Rightarrow> bool"
+ and Q :: "('a list) \<Rightarrow> bool"
+ and k :: nat
+ and f :: "('a list) \<Rightarrow> nat"
+ assumes "\<And> s t. \<lbrakk>P s; \<not> Q s; P (t@s); k < length t\<rbrakk> \<Longrightarrow> f (t@s) < f s"
+ shows "\<And> s t. \<lbrakk> P s; P(t @ s); f(s) * k < length t\<rbrakk> \<Longrightarrow> Q (t@s)"
+ sorry
+*)
+
+text {*
+ The following two notions are introduced to improve the situation.
+ *}
+
+definition all_future :: "(('a list) \<Rightarrow> bool) \<Rightarrow> (('a list) \<Rightarrow> bool) \<Rightarrow> ('a list) \<Rightarrow> bool"
+where "all_future G R s = (\<forall> t. G (t@s) \<longrightarrow> R t)"
+
+definition happen_within :: "(('a list) \<Rightarrow> bool) \<Rightarrow> (('a list) \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> ('a list) \<Rightarrow> bool"
+where "happen_within G R k s = all_future G (\<lambda> t. k < length t \<longrightarrow>
+ (\<exists> i \<le> k. R (moment i t @ s) \<and> G (moment i t @ s))) s"
+
+lemma happen_within_intro:
+ fixes P :: "('a list) \<Rightarrow> bool"
+ and Q :: "('a list) \<Rightarrow> bool"
+ and k :: nat
+ and f :: "('a list) \<Rightarrow> nat"
+ assumes
+ lt_k: "0 < k"
+ and step: "\<And> s. \<lbrakk>P s; \<not> Q s\<rbrakk> \<Longrightarrow> happen_within P (\<lambda> s'. f s' < f s) k s"
+ shows "\<And> s. P s \<Longrightarrow> happen_within P Q ((f s + 1) * k) s"
+proof -
+ fix s
+ assume "P s"
+ thus "happen_within P Q ((f s + 1) * k) s"
+ proof(induct n == "f s + 1" arbitrary:s rule:nat_less_induct)
+ fix s
+ assume ih [rule_format]: "\<forall>m<f s + 1. \<forall>x. m = f x + 1 \<longrightarrow> P x
+ \<longrightarrow> happen_within P Q ((f x + 1) * k) x"
+ and ps: "P s"
+ show "happen_within P Q ((f s + 1) * k) s"
+ proof(cases "Q s")
+ case True
+ show ?thesis
+ proof -
+ { fix t
+ from True and ps have "0 \<le> ((f s + 1)*k) \<and> Q (moment 0 t @ s) \<and> P (moment 0 t @ s)" by auto
+ hence "\<exists>i\<le>(f s + 1) * k. Q (moment i t @ s) \<and> P (moment i t @ s)" by auto
+ } thus ?thesis by (auto simp: happen_within_def all_future_def)
+ qed
+ next
+ case False
+ from step [OF ps False] have kk: "happen_within P (\<lambda>s'. f s' < f s) k s" .
+ show ?thesis
+ proof -
+ { fix t
+ assume pts: "P (t @ s)" and ltk: "(f s + 1) * k < length t"
+ from ltk have lt_k_lt: "k < length t" by auto
+ with kk pts obtain i
+ where le_ik: "i \<le> k"
+ and lt_f: "f (moment i t @ s) < f s"
+ and p_m: "P (moment i t @ s)"
+ by (auto simp:happen_within_def all_future_def)
+ from ih [of "f (moment i t @ s) + 1" "(moment i t @ s)", OF _ _ p_m] and lt_f
+ have hw: "happen_within P Q ((f (moment i t @ s) + 1) * k) (moment i t @ s)" by auto
+ have "(\<exists>j\<le>(f s + 1) * k. Q (moment j t @ s) \<and> P (moment j t @ s))" (is "\<exists> j. ?T j")
+ proof -
+ let ?t = "restm i t"
+ have eq_t: "t = ?t @ moment i t" by (simp add:moment_restm_s)
+ have h1: "P (restm i t @ moment i t @ s)"
+ proof -
+ from pts and eq_t have "P ((restm i t @ moment i t) @ s)" by simp
+ thus ?thesis by simp
+ qed
+ moreover have h2: "(f (moment i t @ s) + 1) * k < length (restm i t)"
+ proof -
+ have h: "\<And> x y z. (x::nat) \<le> y \<Longrightarrow> x * z \<le> y * z" by simp
+ from lt_f have "(f (moment i t @ s) + 1) \<le> f s " by simp
+ from h [OF this, of k]
+ have "(f (moment i t @ s) + 1) * k \<le> f s * k" .
+ moreover from le_ik have "\<dots> \<le> ((f s) * k + k - i)" by simp
+ moreover from le_ik lt_k_lt and ltk have "(f s) * k + k - i < length t - i" by simp
+ moreover have "length (restm i t) = length t - i" using length_restm by metis
+ ultimately show ?thesis by simp
+ qed
+ from hw [unfolded happen_within_def all_future_def, rule_format, OF h1 h2]
+ obtain m where le_m: "m \<le> (f (moment i t @ s) + 1) * k"
+ and q_m: "Q (moment m ?t @ moment i t @ s)"
+ and p_m: "P (moment m ?t @ moment i t @ s)" by auto
+ have eq_mm: "moment m ?t @ moment i t @ s = (moment (m+i) t)@s"
+ proof -
+ have "moment m (restm i t) @ moment i t = moment (m + i) t"
+ using moment_plus_split by metis
+ thus ?thesis by simp
+ qed
+ let ?j = "m + i"
+ have "?T ?j"
+ proof -
+ have "m + i \<le> (f s + 1) * k"
+ proof -
+ have h: "\<And> x y z. (x::nat) \<le> y \<Longrightarrow> x * z \<le> y * z" by simp
+ from lt_f have "(f (moment i t @ s) + 1) \<le> f s " by simp
+ from h [OF this, of k]
+ have "(f (moment i t @ s) + 1) * k \<le> f s * k" .
+ with le_m have "m \<le> f s * k" by simp
+ hence "m + i \<le> f s * k + i" by simp
+ with le_ik show ?thesis by simp
+ qed
+ moreover from eq_mm q_m have " Q (moment (m + i) t @ s)" by metis
+ moreover from eq_mm p_m have " P (moment (m + i) t @ s)" by metis
+ ultimately show ?thesis by blast
+ qed
+ thus ?thesis by blast
+ qed
+ } thus ?thesis by (simp add:happen_within_def all_future_def firstn.simps)
+ qed
+ qed
+ qed
+qed
+
+end
+