theory Moment+
−
imports Main+
−
begin+
−
+
−
definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where "moment n s = rev (take n (rev s))"+
−
+
−
definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where "restm n s = rev (drop 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]"+
−
+
−
value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"+
−
+
−
lemma moment_restm_s: "(restm n s) @ (moment n s) = s"+
−
  unfolding restm_def moment_def+
−
by (metis append_take_drop_id rev_append rev_rev_ident)+
−
+
−
lemma length_moment_le:+
−
  assumes le_k: "k \<le> length s"+
−
  shows "length (moment k s) = k"+
−
using le_k unfolding moment_def by auto+
−
+
−
lemma length_moment_ge:+
−
  assumes le_k: "length s \<le> k"+
−
  shows "length (moment k s) = (length s)"+
−
using assms unfolding moment_def by simp+
−
+
−
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 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+
−
qed+
−
+
−
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)))"+
−
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+
−
qed+
−
+
−
lemma moment_plus_split:+
−
  shows "moment (m + i) s = moment m (restm i s) @ moment i s"+
−
unfolding moment_def restm_def+
−
by (metis add.commute rev_append rev_rev_ident take_add)+
−
+
−
lemma moment_prefix: +
−
  "(moment i t @ s) = moment (i + length s) (t @ s)"+
−
proof -+
−
  from moment_plus_split [of i "length s" "t@s"]+
−
  have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"+
−
    by auto+
−
  have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" +
−
    by (simp add: moment_def)+
−
  with moment_app show ?thesis by auto+
−
qed+
−
+
−
lemma moment_plus: +
−
  "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)"+
−
proof(induct s, simp+)+
−
  fix a s+
−
  assume ih: "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = hd (moment (Suc i) s) # moment i s"+
−
    and le_i: "i \<le> length s"+
−
  show "moment (Suc i) (a # s) = hd (moment (Suc i) (a # s)) # moment i (a # s)"+
−
  proof(cases "i= length s")+
−
    case True+
−
    hence "Suc i = length (a#s)" by simp+
−
    with moment_eq have "moment (Suc i) (a#s) = a#s" by auto+
−
    moreover have "moment i (a#s) = s"+
−
    proof -+
−
      from moment_app [OF le_i, of "[a]"]+
−
      and True show ?thesis by simp+
−
    qed+
−
    ultimately show ?thesis by auto+
−
  next+
−
    case False+
−
    from False and le_i have lti: "i < length s" by arith+
−
    hence les_i: "Suc i \<le> length s" by arith+
−
    show ?thesis +
−
    proof -+
−
      from moment_app [OF les_i, of "[a]"]+
−
      have "moment (Suc i) (a # s) = moment (Suc i) s" by simp+
−
      moreover have "moment i (a#s) = moment i s" +
−
      proof -+
−
        from lti have "i \<le> length s" by simp+
−
        from moment_app [OF this, of "[a]"] show ?thesis by simp+
−
      qed+
−
      moreover note ih [OF les_i]+
−
      ultimately show ?thesis by auto+
−
    qed+
−
  qed+
−
qed+
−
+
−
end+
−
+
−