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+
−
+
−