theory Moment+
−
imports Main+
−
begin+
−
+
−
fun firstn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where+
−
  "firstn 0 s = []" |+
−
  "firstn (Suc n) [] = []" |+
−
  "firstn (Suc n) (e#s) = e#(firstn n s)"+
−
+
−
lemma upto_map_plus: "map (op + k) [i..j] = [i+k..j+k]"+
−
proof(induct "[i..j]" arbitrary:i j rule:length_induct)+
−
  case (1 i j)+
−
  thus ?case+
−
  proof(cases "i \<le> j")+
−
    case True+
−
    hence le_k: "i + k \<le> j + k" by simp+
−
    show ?thesis (is "?L = ?R")+
−
    proof -+
−
      have "?L  = (k + i) # map (op + k) [i + 1..j]"+
−
         by (simp add: upto_rec1[OF True])+
−
      moreover have "?R = (i + k) # [i + k + 1..j + k]"+
−
        by (simp add: upto_rec1[OF le_k])+
−
      moreover have "map (op + k) [i + 1..j] = [i + k + 1..j + k]"+
−
      proof -+
−
        have h: "i + k + 1 = (i + 1) + k" by simp+
−
        show ?thesis+
−
        proof(unfold h, rule 1[rule_format])+
−
          show "length [i + 1..j] < length [i..j]"+
−
            using upto_rec1[OF True] by simp+
−
        qed simp+
−
      qed+
−
      ultimately show ?thesis by simp+
−
    qed+
−
  qed auto+
−
qed+
−
+
−
lemma firstn_alt_def:+
−
  "firstn n s = map (\<lambda> i. s!(nat i)) [0..(int (min (length s) n)) - 1]"+
−
proof(induct n arbitrary:s)+
−
  case (0 s)+
−
  thus ?case by auto+
−
next+
−
  case (Suc n s)+
−
  thus ?case (is "?L = ?R")+
−
  proof(cases s)+
−
    case Nil+
−
    thus ?thesis by simp+
−
  next+
−
    case (Cons e es)+
−
    with Suc +
−
    have "?L =  e # map (\<lambda>i. es ! nat i) [0..int (min (length es) n) - 1]"+
−
      by simp+
−
    also have "... = map (\<lambda>i. (e # es) ! nat i) [0..int (min (length es) n)]"+
−
      (is "?L1 = ?R1")+
−
    proof -+
−
      have "?R1 =   e # map (\<lambda>i. (e # es) ! nat i) +
−
                            [1..int (min (length es) n)]" +
−
      proof -+
−
        have "[0..int (min (length es) n)] = 0#[1..int (min (length es) n)]"+
−
          by (simp add: upto.simps)+
−
        thus ?thesis by simp+
−
      qed+
−
      also have "... = ?L1" (is "_#?L2 = _#?R2")+
−
      proof -+
−
        have "?L2 = ?R2"+
−
        proof -+
−
          have "map (\<lambda>i. (e # es) ! nat i) [1..int (min (length es) n)] =  +
−
                map ((\<lambda>i. (e # es) ! nat i) \<circ> op + 1) [0..int (min (length es) n) - 1]" +
−
          proof -+
−
            have "[1..int (min (length es) n)] = +
−
                             map (op + 1) [0..int (min (length es) n) - 1]"+
−
                     by (unfold upto_map_plus, simp)+
−
            thus ?thesis by simp+
−
          qed+
−
          also have "... = map (\<lambda>i. es ! nat i) [0..int (min (length es) n) - 1]"+
−
          proof(rule map_cong)+
−
            fix x+
−
            assume "x \<in> set [0..int (min (length es) n) - 1]"+
−
            thus "((\<lambda>i. (e # es) ! nat i) \<circ> op + 1) x = es ! nat x"+
−
              by (metis atLeastLessThan_iff atLeastLessThan_upto +
−
                    comp_apply local.Cons nat_0_le nat_int nth_Cons_Suc of_nat_Suc)+
−
          qed auto+
−
          finally show ?thesis .+
−
        qed+
−
        thus ?thesis by simp+
−
      qed+
−
      finally show ?thesis by simp+
−
    qed+
−
    also have "... = ?R"+
−
      by (unfold Cons, simp)+
−
    finally show ?thesis .+
−
  qed+
−
qed+
−
+
−
fun restn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where "restn n s = rev (firstn (length s - n) (rev s))"+
−
+
−
definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where "moment n s = rev (firstn n (rev s))"+
−
+
−
definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where "restm n s = rev (restn n (rev s))"+
−
+
−
definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
  where "from_to i j s = firstn (j - i) (restn i s)"+
−
+
−
definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"+
−
where "down_to j i s = rev (from_to i j (rev s))"+
−
+
−
value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]"+
−
value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]"+
−
+
−
lemma length_eq_elim_l: "\<lbrakk>length xs = length ys; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs"+
−
  by auto+
−
+
−
lemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs"+
−
  by simp+
−
+
−
lemma firstn_nil [simp]: "firstn n [] = []"+
−
  by (cases n, simp+)+
−
+
−
+
−
value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ +
−
       from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]"+
−
+
−
lemma firstn_le: "\<And> n s'. n \<le> length s \<Longrightarrow> firstn n (s@s') = firstn n s"+
−
proof (induct s, simp)+
−
  fix a s n s'+
−
  assume ih: "\<And>n s'. n \<le> length s \<Longrightarrow> firstn n (s @ s') = firstn n s"+
−
  and le_n: " n \<le> length (a # s)"+
−
  show "firstn n ((a # s) @ s') = firstn n (a # s)"+
−
  proof(cases n, simp)+
−
    fix k+
−
    assume eq_n: "n = Suc k"+
−
    with le_n have "k \<le> length s" by auto+
−
    from ih [OF this] and eq_n+
−
    show "firstn n ((a # s) @ s') = firstn n (a # s)" by auto+
−
  qed+
−
qed+
−
+
−
lemma firstn_ge [simp]: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s"+
−
proof(induct s, simp)+
−
  fix a s n+
−
  assume ih: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s"+
−
    and le: "length (a # s) \<le> n"+
−
  show "firstn n (a # s) = a # s"+
−
  proof(cases n)+
−
    assume eq_n: "n = 0" with le show ?thesis by simp+
−
  next+
−
    fix k+
−
    assume eq_n: "n = Suc k"+
−
    with le have le_k: "length s \<le> k" by simp+
−
    from ih [OF this] have "firstn k s = s" .+
−
    from eq_n and this+
−
    show ?thesis by simp+
−
  qed+
−
qed+
−
+
−
lemma firstn_eq [simp]: "firstn (length s) s = s"+
−
  by simp+
−
+
−
lemma firstn_restn_s: "(firstn n (s::'a list)) @ (restn n s) = s"+
−
proof(induct n arbitrary:s, simp)+
−
  fix n s+
−
  assume ih: "\<And>t. firstn n (t::'a list) @ restn n t = t"+
−
  show "firstn (Suc n) (s::'a list) @ restn (Suc n) s = s"+
−
  proof(cases s, simp)+
−
    fix x xs+
−
    assume eq_s: "s = x#xs"+
−
    show "firstn (Suc n) s @ restn (Suc n) s = s"+
−
    proof -+
−
      have "firstn (Suc n) s @ restn (Suc n) s =  x # (firstn n xs @ restn n xs)"+
−
      proof -+
−
        from eq_s have "firstn (Suc n) s =  x # firstn n xs" by simp+
−
        moreover have "restn (Suc n) s = restn n xs"+
−
        proof -+
−
          from eq_s have "restn (Suc n) s = rev (firstn (length xs - n) (rev xs @ [x]))" by simp+
−
          also have "\<dots> = restn n xs"+
−
          proof -+
−
            have "(firstn (length xs - n) (rev xs @ [x])) = (firstn (length xs - n) (rev xs))"+
−
              by(rule firstn_le, simp)+
−
            hence "rev (firstn (length xs - n) (rev xs @ [x])) = +
−
              rev (firstn (length xs - n) (rev xs))" by simp+
−
            also have "\<dots> = rev (firstn (length (rev xs) - n) (rev xs))" by simp+
−
            finally show ?thesis by simp+
−
          qed+
−
          finally show ?thesis by simp+
−
        qed+
−
        ultimately show ?thesis by simp+
−
      qed with ih eq_s show ?thesis by simp+
−
    qed+
−
  qed+
−
qed+
−
+
−
lemma moment_restm_s: "(restm n s)@(moment n s) = s"+
−
proof -+
−
  have " rev  ((firstn n (rev s)) @ (restn n (rev s))) = s" (is "rev ?x = s")+
−
  proof -+
−
    have "?x = rev s" by (simp only:firstn_restn_s)+
−
    thus ?thesis by auto+
−
  qed+
−
  thus ?thesis +
−
    by (auto simp:restm_def moment_def)+
−
qed+
−
+
−
declare restn.simps [simp del] firstn.simps[simp del]+
−
+
−
lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"+
−
proof(induct n arbitrary:s, simp add:firstn.simps)+
−
  case (Suc k)+
−
  assume ih: "\<And> s. length (s::'a list) \<le> k \<Longrightarrow> length (firstn k s) = length s"+
−
  and le: "length s \<le> Suc k"+
−
  show ?case+
−
  proof(cases s)+
−
    case Nil+
−
    from Nil show ?thesis by simp+
−
  next+
−
    case (Cons x xs)+
−
    from le and Cons have "length xs \<le> k" by simp+
−
    from ih [OF this] have "length (firstn k xs) = length xs" .+
−
    moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" +
−
      by (simp add:firstn.simps)+
−
    moreover note Cons+
−
    ultimately show ?thesis by simp+
−
  qed+
−
qed+
−
+
−
lemma length_firstn_le: "n \<le> length s \<Longrightarrow> length (firstn n s) = n"+
−
proof(induct n arbitrary:s, simp add:firstn.simps)+
−
  case (Suc k)+
−
  assume ih: "\<And>s. k \<le> length (s::'a list) \<Longrightarrow> length (firstn k s) = k"+
−
    and le: "Suc k \<le> length s"+
−
  show ?case+
−
  proof(cases s)+
−
    case Nil+
−
    from Nil and le show ?thesis by auto+
−
  next+
−
    case (Cons x xs)+
−
    from le and Cons have "k \<le> length xs" by simp+
−
    from ih [OF this] have "length (firstn k xs) = k" .+
−
    moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" +
−
      by (simp add:firstn.simps)+
−
    ultimately show ?thesis by simp+
−
  qed+
−
qed+
−
+
−
lemma app_firstn_restn: +
−
  fixes s1 s2+
−
  shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)"+
−
proof(rule length_eq_elim_l)+
−
  have "length s1 \<le> length (s1 @ s2)" by simp+
−
  from length_firstn_le [OF this]+
−
  show "length s1 = length (firstn (length s1) (s1 @ s2))" by simp+
−
next+
−
  from firstn_restn_s +
−
  show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)"+
−
    by metis+
−
qed+
−
+
−
+
−
lemma length_moment_le:+
−
  fixes k s+
−
  assumes le_k: "k \<le> length s"+
−
  shows "length (moment k s) = k"+
−
proof -+
−
  have "length (rev (firstn k (rev s))) = k"+
−
  proof -+
−
    have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp+
−
    also have "\<dots> = k" +
−
    proof(rule length_firstn_le)+
−
      from le_k show "k \<le> length (rev s)" by simp+
−
    qed+
−
    finally show ?thesis .+
−
  qed+
−
  thus ?thesis by (simp add:moment_def)+
−
qed+
−
+
−
lemma app_moment_restm: +
−
  fixes s1 s2+
−
  shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)"+
−
proof(rule length_eq_elim_r)+
−
  have "length s2 \<le> length (s1 @ s2)" by simp+
−
  from length_moment_le [OF this]+
−
  show "length s2 = length (moment (length s2) (s1 @ s2))" by simp+
−
next+
−
  from moment_restm_s +
−
  show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)"+
−
    by metis+
−
qed+
−
+
−
lemma length_moment_ge:+
−
  fixes k s+
−
  assumes le_k: "length s \<le> k"+
−
  shows "length (moment k s) = (length s)"+
−
proof -+
−
  have "length (rev (firstn k (rev s))) = length s"+
−
  proof -+
−
    have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp+
−
    also have "\<dots> = length s" +
−
    proof -+
−
      have "\<dots> = length (rev s)"+
−
      proof(rule length_firstn_ge)+
−
        from le_k show "length (rev s) \<le> k" by simp+
−
      qed+
−
      also have "\<dots> = length s" by simp+
−
      finally show ?thesis .+
−
    qed+
−
    finally show ?thesis .+
−
  qed+
−
  thus ?thesis by (simp add:moment_def)+
−
qed+
−
+
−
lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"+
−
proof(cases "n \<le> length s")+
−
  case True+
−
  from length_firstn_le [OF True] show ?thesis by auto+
−
next+
−
  case False+
−
  from False have "length s \<le> n" by simp+
−
  from firstn_ge [OF this] show ?thesis by auto+
−
qed+
−
+
−
lemma firstn_conc: +
−
  fixes m n+
−
  assumes le_mn: "m \<le> n"+
−
  shows "firstn m s = firstn m (firstn n  s)"+
−
proof(cases "m \<le> length s")+
−
  case True+
−
  have "s = (firstn n s) @ (restn n s)" by (simp add:firstn_restn_s)+
−
  hence "firstn m s = firstn m \<dots>" by simp+
−
  also have "\<dots> = firstn m (firstn n s)" +
−
  proof -+
−
    from length_firstn [of n s]+
−
    have "m \<le> length (firstn n s)"+
−
    proof+
−
      assume "length (firstn n s) = length s" with True show ?thesis by simp+
−
    next+
−
      assume "length (firstn n s) = n " with le_mn show ?thesis by simp+
−
    qed+
−
    from firstn_le [OF this, of "restn n s"]+
−
    show ?thesis .+
−
  qed+
−
  finally show ?thesis by simp+
−
next+
−
  case False+
−
  from False and le_mn have "length s \<le> n"  by simp+
−
  from firstn_ge [OF this] show ?thesis by simp+
−
qed+
−
+
−
lemma restn_conc: +
−
  fixes i j k s+
−
  assumes eq_k: "j + i = k"+
−
  shows "restn k s = restn j (restn i s)"+
−
proof -+
−
  have "(firstn (length s - k) (rev s)) =+
−
        (firstn (length (rev (firstn (length s - i) (rev s))) - j) +
−
                            (rev (rev (firstn (length s - i) (rev s)))))"+
−
  proof  -+
−
    have "(firstn (length s - k) (rev s)) =+
−
            (firstn (length (rev (firstn (length s - i) (rev s))) - j) +
−
                                           (firstn (length s - i) (rev s)))"+
−
    proof -+
−
      have " (length (rev (firstn (length s - i) (rev s))) - j) = length s - k"+
−
      proof -+
−
        have "(length (rev (firstn (length s - i) (rev s))) - j) = (length s - i) - j"+
−
        proof -+
−
          have "(length (rev (firstn (length s - i) (rev s))) - j) = +
−
                                         length ((firstn (length s - i) (rev s))) - j"+
−
            by simp+
−
          also have "\<dots> = length ((firstn (length (rev s) - i) (rev s))) - j" by simp+
−
          also have "\<dots> = (length (rev s) - i) - j" +
−
          proof -+
−
            have "length ((firstn (length (rev s) - i) (rev s))) = (length (rev s) - i)"+
−
              by (rule length_firstn_le, simp)+
−
            thus ?thesis by simp+
−
          qed+
−
          also have "\<dots> = (length s - i) - j" by simp+
−
          finally show ?thesis .+
−
        qed+
−
        with eq_k show ?thesis by auto+
−
      qed+
−
      moreover have "(firstn (length s - k) (rev s)) =+
−
                             (firstn (length s - k) (firstn (length s - i) (rev s)))"+
−
      proof(rule firstn_conc)+
−
        from eq_k show "length s - k \<le> length s - i" by simp+
−
      qed+
−
      ultimately show ?thesis by simp+
−
    qed+
−
    thus ?thesis by simp+
−
  qed+
−
  thus ?thesis by (simp only:restn.simps)+
−
qed+
−
+
−
(*+
−
value "down_to 2 0 [5, 4, 3, 2, 1, 0]"+
−
value "moment 2 [5, 4, 3, 2, 1, 0]"+
−
*)+
−
+
−
lemma from_to_firstn: "from_to 0 k s = firstn k s"+
−
by (simp add:from_to_def restn.simps)+
−
+
−
lemma moment_app [simp]:+
−
  assumes +
−
  ile: "i \<le> length s"+
−
  shows "moment i (s'@s) = moment i s"+
−
proof -+
−
  have "moment i (s'@s) = rev (firstn i (rev (s'@s)))" by (simp add:moment_def)+
−
  moreover have "firstn i (rev (s'@s)) = firstn i (rev s @ rev s')" by simp+
−
  moreover have "\<dots> = firstn i (rev s)"+
−
  proof(rule firstn_le)+
−
    have "length (rev s) = length s" by simp+
−
    with ile show "i \<le> length (rev s)" by simp+
−
  qed+
−
  ultimately show ?thesis by (simp add:moment_def)+
−
qed+
−
+
−
lemma moment_eq [simp]: "moment (length s) (s'@s) = s"+
−
proof -+
−
  have "length s \<le> length s" by simp+
−
  from moment_app [OF this, of s'] +
−
  have " moment (length s) (s' @ s) = moment (length s) s" .+
−
  moreover have "\<dots> = s" by (simp add:moment_def)+
−
  ultimately show ?thesis by simp+
−
qed+
−
+
−
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 firstn.simps)+
−
+
−
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: +
−
  "\<And> s Q. \<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: +
−
  "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+
−
+
−
lemma from_to_conc:+
−
  fixes i j k s+
−
  assumes le_ij: "i \<le> j"+
−
  and le_jk: "j \<le> k"+
−
  shows "from_to i j s @ from_to j k s = from_to i k s"+
−
proof -+
−
  let ?ris = "restn i s"+
−
  have "firstn (j - i) (restn i s) @ firstn (k - j) (restn j s) =+
−
         firstn (k - i) (restn i s)" (is "?x @ ?y = ?z")+
−
  proof -+
−
    let "firstn (k-j) ?u" = "?y"+
−
    let ?rst = " restn (k - j) (restn (j - i) ?ris)"+
−
    let ?rst' = "restn (k - i) ?ris"+
−
    have "?u = restn (j-i) ?ris"+
−
    proof(rule restn_conc)+
−
      from le_ij show "j - i + i = j" by simp+
−
    qed+
−
    hence "?x @ ?y = ?x @ firstn (k-j) (restn (j-i) ?ris)" by simp+
−
    moreover have "firstn (k - j) (restn (j - i) (restn i s)) @ ?rst = +
−
                      restn (j-i) ?ris" by (simp add:firstn_restn_s)+
−
    ultimately have "?x @ ?y @ ?rst = ?x @ (restn (j-i) ?ris)" by simp+
−
    also have "\<dots> = ?ris" by (simp add:firstn_restn_s)+
−
    finally have "?x @ ?y @ ?rst = ?ris" .+
−
    moreover have "?z @ ?rst = ?ris"+
−
    proof -+
−
      have "?z @ ?rst' = ?ris" by (simp add:firstn_restn_s)+
−
      moreover have "?rst' = ?rst"+
−
      proof(rule restn_conc)+
−
        from le_ij le_jk show "k - j + (j - i) = k - i" by auto+
−
      qed+
−
      ultimately show ?thesis by simp+
−
    qed+
−
    ultimately have "?x @ ?y @ ?rst = ?z @ ?rst" by simp+
−
    thus ?thesis by auto    +
−
  qed+
−
  thus ?thesis by (simp only:from_to_def)+
−
qed+
−
+
−
lemma down_to_conc:+
−
  fixes i j k s+
−
  assumes le_ij: "i \<le> j"+
−
  and le_jk: "j \<le> k"+
−
  shows "down_to k j s @ down_to j i s = down_to k i s"+
−
proof -+
−
  have "rev (from_to j k (rev s)) @ rev (from_to i j (rev s)) = rev (from_to i k (rev s))"+
−
    (is "?L = ?R")+
−
  proof -+
−
    have "?L = rev (from_to i j (rev s) @ from_to j k (rev s))" by simp+
−
    also have "\<dots> = ?R" (is "rev ?x = rev ?y")+
−
    proof -+
−
      have "?x = ?y" by (rule from_to_conc[OF le_ij le_jk])+
−
      thus ?thesis by simp+
−
    qed+
−
    finally show ?thesis .+
−
  qed+
−
  thus ?thesis by (simp add:down_to_def)+
−
qed+
−
+
−
lemma restn_ge:+
−
  fixes s k+
−
  assumes le_k: "length s \<le> k"+
−
  shows "restn k s = []"+
−
proof -+
−
  from firstn_restn_s [of k s, symmetric] have "s = (firstn k s) @ (restn k s)" .+
−
  hence "length s = length \<dots>" by simp+
−
  also have "\<dots> = length (firstn k s) + length (restn k s)" by simp+
−
  finally have "length s = ..." by simp+
−
  moreover from length_firstn_ge and le_k +
−
  have "length (firstn k s) = length s" by simp+
−
  ultimately have "length (restn k s) = 0" by auto+
−
  thus ?thesis by auto+
−
qed+
−
+
−
lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []"+
−
proof(simp only:from_to_def)+
−
  assume "length s \<le> k"+
−
  from restn_ge [OF this] +
−
  show "firstn (j - k) (restn k s) = []" by simp+
−
qed+
−
+
−
(*+
−
value "from_to 2 5 [0, 1, 2, 3, 4]"+
−
value "restn 2  [0, 1, 2, 3, 4]"+
−
*)+
−
+
−
lemma from_to_restn: +
−
  fixes k j s+
−
  assumes le_j: "length s \<le> j"+
−
  shows "from_to k j s = restn k s"+
−
proof -+
−
  have "from_to 0 k s @ from_to k j s = from_to 0 j s"+
−
  proof(cases "k \<le> j")+
−
    case True+
−
    from from_to_conc True show ?thesis by auto+
−
  next+
−
    case False+
−
    from False le_j have lek: "length s \<le>  k" by auto+
−
    from from_to_ge [OF this] have "from_to k j s = []" .+
−
    hence "from_to 0 k s @ from_to k j s = from_to 0 k s" by simp+
−
    also have "\<dots> = s"+
−
    proof -+
−
      from from_to_firstn [of k s]+
−
      have "\<dots> = firstn k s" .+
−
      also have "\<dots> = s" by (rule firstn_ge [OF lek])+
−
      finally show ?thesis .+
−
    qed+
−
    finally have "from_to 0 k s @ from_to k j s = s" .+
−
    moreover have "from_to 0 j s = s"+
−
    proof -+
−
      have "from_to 0 j s = firstn j s" by (simp add:from_to_firstn)+
−
      also have "\<dots> = s"+
−
      proof(rule firstn_ge)+
−
        from le_j show "length s \<le> j " by simp+
−
      qed+
−
      finally show ?thesis .+
−
    qed+
−
    ultimately show ?thesis by auto+
−
  qed+
−
  also have "\<dots> = s" +
−
  proof -+
−
    from from_to_firstn have "\<dots> = firstn j s" .+
−
    also have "\<dots> = s"+
−
    proof(rule firstn_ge)+
−
      from le_j show "length s \<le> j" by simp+
−
    qed+
−
    finally show ?thesis .+
−
  qed+
−
  finally have "from_to 0 k s @ from_to k j s = s" .+
−
  moreover have "from_to 0 k s @ restn k s = s"+
−
  proof -+
−
    from from_to_firstn [of k s]+
−
    have "from_to 0 k s = firstn k s" .+
−
    thus ?thesis by (simp add:firstn_restn_s)+
−
  qed+
−
  ultimately have "from_to 0 k s @ from_to k j s  = +
−
                    from_to 0 k s @ restn k s" by simp+
−
  thus ?thesis by auto+
−
qed+
−
+
−
lemma down_to_moment: "down_to k 0 s = moment k s"+
−
proof -+
−
  have "rev (from_to 0 k (rev s)) = rev (firstn k (rev s))" +
−
    using from_to_firstn by metis+
−
  thus ?thesis by (simp add:down_to_def moment_def)+
−
qed+
−
+
−
lemma down_to_restm:+
−
  assumes le_s: "length s \<le> j"+
−
  shows "down_to j k s = restm k s"+
−
proof -+
−
  have "rev (from_to k j (rev s)) = rev (restn k (rev s))" (is "?L = ?R")+
−
  proof -+
−
    from le_s have "length (rev s) \<le> j" by simp+
−
    from from_to_restn [OF this, of k] show ?thesis by simp+
−
  qed+
−
  thus ?thesis by (simp add:down_to_def restm_def)+
−
qed+
−
+
−
lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s"+
−
proof -+
−
  have "moment (m + i) s = down_to (m+i) 0 s" using down_to_moment by metis+
−
  also have "\<dots> = (down_to (m+i) i s) @ (down_to i 0 s)" +
−
    by(rule down_to_conc[symmetric], auto)+
−
  finally show ?thesis .+
−
qed+
−
+
−
lemma length_restn: "length (restn i s) = length s - i"+
−
proof(cases "i \<le> length s")+
−
  case True+
−
  from length_firstn_le [OF this] have "length (firstn i s) = i" .+
−
  moreover have "length s = length (firstn i s) + length (restn i s)"+
−
  proof -+
−
    have "s = firstn i s @ restn i s" using firstn_restn_s by metis+
−
    hence "length s = length \<dots>" by simp+
−
    thus ?thesis by simp+
−
  qed+
−
  ultimately show ?thesis by simp+
−
next +
−
  case False+
−
  hence "length s \<le> i" by simp+
−
  from restn_ge [OF this] have "restn i s = []" .+
−
  with False show ?thesis by simp+
−
qed+
−
+
−
lemma length_from_to_in:+
−
  fixes i j s+
−
  assumes le_ij: "i \<le> j"+
−
  and le_j: "j \<le> length s"+
−
  shows "length (from_to i j s) = j - i"+
−
proof -+
−
  have "from_to 0 j s = from_to 0 i s @ from_to i j s"+
−
    by (rule from_to_conc[symmetric, OF _ le_ij], simp)+
−
  moreover have "length (from_to 0 j s) = j"+
−
  proof -+
−
    have "from_to 0 j s = firstn j s" using from_to_firstn by metis+
−
    moreover have "length \<dots> = j" by (rule length_firstn_le [OF le_j])+
−
    ultimately show ?thesis by simp+
−
  qed+
−
  moreover have "length (from_to 0 i s) = i"+
−
  proof -+
−
    have "from_to 0 i s = firstn i s" using from_to_firstn by metis+
−
    moreover have "length \<dots> = i" +
−
    proof (rule length_firstn_le)+
−
      from le_ij le_j show "i \<le> length s" by simp+
−
    qed+
−
    ultimately show ?thesis by simp+
−
  qed+
−
  ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)"+
−
proof(cases "m+i \<le> length s")+
−
  case True+
−
  have "restn i s = from_to i (m+i) s @ from_to (m+i) (length s) s"+
−
  proof -+
−
    have "restn i s = from_to i (length s) s"+
−
      by(rule from_to_restn[symmetric], simp)+
−
    also have "\<dots> = from_to i (m+i) s @ from_to (m+i) (length s) s"+
−
      by(rule from_to_conc[symmetric, OF _ True], simp)+
−
    finally show ?thesis .+
−
  qed+
−
  hence "firstn m (restn i s) = firstn m \<dots>" by simp+
−
  moreover have "\<dots> = firstn (length (from_to i (m+i) s)) +
−
                    (from_to i (m+i) s @ from_to (m+i) (length s) s)"+
−
  proof -+
−
    have "length (from_to i (m+i) s) = m"+
−
    proof -+
−
      have "length (from_to i (m+i) s) = (m+i) - i"+
−
        by(rule length_from_to_in [OF _ True], simp)+
−
      thus ?thesis by simp+
−
    qed+
−
    thus ?thesis by simp+
−
  qed+
−
  ultimately show ?thesis using app_firstn_restn by metis+
−
next+
−
  case False+
−
  hence "length s \<le> m + i" by simp+
−
  from from_to_restn [OF this]+
−
  have "from_to i (m + i) s = restn i s" .+
−
  moreover have "firstn m (restn i s) = restn i s" +
−
  proof(rule firstn_ge)+
−
    show "length (restn i s) \<le> m"+
−
    proof -+
−
      have "length (restn i s) = length s - i" using length_restn by metis+
−
      with False show ?thesis by simp+
−
    qed+
−
  qed+
−
  ultimately show ?thesis by simp+
−
qed+
−
+
−
lemma down_to_moment_restm:+
−
  fixes m i s+
−
  shows "down_to (m + i) i s = moment m (restm i s)"+
−
  by (simp add:firstn_restn_from_to down_to_def moment_def restm_def)+
−
+
−
lemma moment_plus_split:+
−
  fixes m i s+
−
  shows "moment (m + i) s = moment m (restm i s) @ moment i s"+
−
proof -+
−
  from moment_split [of m i s]+
−
  have "moment (m + i) s = down_to (m + i) i s @ down_to i 0 s" .+
−
  also have "\<dots> = down_to (m+i) i s @ moment i s" using down_to_moment by simp+
−
  also from down_to_moment_restm have "\<dots> = moment m (restm i s) @ moment i s"+
−
    by simp+
−
  finally show ?thesis .+
−
qed+
−
+
−
lemma length_restm: "length (restm i s) = length s - i"+
−
proof -+
−
  have "length (rev (restn i (rev s))) = length s - i" (is "?L = ?R")+
−
  proof -+
−
    have "?L = length (restn i (rev s))" by simp+
−
    also have "\<dots>  = length (rev s) - i" using length_restn by metis+
−
    also have "\<dots> = ?R" by simp+
−
    finally show ?thesis .+
−
  qed+
−
  thus ?thesis by (simp add:restm_def)+
−
qed+
−
+
−
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+
−
  with app_moment_restm[of t s]+
−
  have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp+
−
  with moment_app show ?thesis by auto+
−
qed+
−
+
−
lemma length_down_to_in: +
−
  assumes le_ij: "i \<le> j"+
−
    and le_js: "j \<le> length s"+
−
  shows "length (down_to j i s) = j - i"+
−
proof -+
−
  have "length (down_to j i s) = length (from_to i j (rev s))"+
−
    by (unfold down_to_def, auto)+
−
  also have "\<dots> = j - i"+
−
  proof(rule length_from_to_in[OF le_ij])+
−
    from le_js show "j \<le> length (rev s)" by simp+
−
  qed+
−
  finally show ?thesis .+
−
qed+
−
+
−
+
−
lemma moment_head: +
−
  assumes le_it: "Suc i \<le> length t"+
−
  obtains e where "moment (Suc i) t = e#moment i t"+
−
proof -+
−
  have "i \<le> Suc i" by simp+
−
  from length_down_to_in [OF this le_it]+
−
  have "length (down_to (Suc i) i t) = 1" by auto+
−
  then obtain e where "down_to (Suc i) i t = [e]"+
−
    apply (cases "(down_to (Suc i) i t)") by auto+
−
  moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"+
−
    by (rule down_to_conc[symmetric], auto)+
−
  ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"+
−
    by (auto simp:down_to_moment)+
−
  from that [OF this] show ?thesis .+
−
qed+
−
+
−
end+
−