theory Moment

imports Main

begin

definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

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 length_moment_le:

  assumes le_k: "k \<le> length s"

  shows "length (moment k s) = k"

lemma length_moment_ge:

  assumes le_k: "length s \<le> k"

  shows "length (moment k s) = (length s)"

  assumes le_mn: "m \<le> n"

(*

value "down_to 2 0 [5, 4, 3, 2, 1, 0]"

value "moment 2 [5, 4, 3, 2, 1, 0]"

*)

lemma moment_app [simp]:

  shows "moment i (s'@s) = moment i s"

lemma moment_eq [simp]: "moment (length s) (s'@s) = s"

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 = []"

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

end