theory Moment
imports Main
begin

definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
where "moment n s = rev (take n (rev s))"

value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"

definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
where "restm n s = rev (drop n (rev s))"

value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"

definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
  where "from_to i j s = take (j - i) (drop 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]"

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 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)

declare drop.simps [simp del] 

lemma length_take_le: 
  "n \<le> length s \<Longrightarrow> length (take n s) = n"
by (metis length_take min.absorb2)

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 length_take: 
  "(length (take n s) = length s) \<or> (length (take n s) = n)"
by (metis length_take min_def)

lemma take_conc: 
  assumes le_mn: "m \<le> n"
  shows "take m s = take m (take n  s)"
using assms by (metis min.absorb1 take_take) 

(*
value "down_to 2 0 [5, 4, 3, 2, 1, 0]"
value "moment 2 [5, 4, 3, 2, 1, 0]"
*)

lemma from_to_take: "from_to 0 k s = take k s"
by (simp add:from_to_def drop.simps)

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: 
  "\<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

(*
value "from_to 2 5 [0, 1, 2, 3, 4]"
value "drop 2  [0, 1, 2, 3, 4]"
*)

(*
lemma down_to_moment: "down_to k 0 s = moment k s"
proof -
  have "rev (from_to 0 k (rev s)) = rev (take k (rev s))" 
    using from_to_take by metis
  thus ?thesis by (simp add:down_to_def moment_def)
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 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"
using assms
unfolding down_to_def from_to_def
by (simp)

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 a: "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"
    unfolding down_to_def from_to_def rev_append[symmetric]
    apply(simp del: rev_append)
    by (metis One_nat_def Suc_eq_plus1_left add.commute take_add)
  ultimately have eq_me: "moment (Suc i) t = e # (moment i t)"
    by(simp add: moment_def down_to_def from_to_def)
  from that [OF this] show ?thesis .
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