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>