theory Momentimports Mainbeginfun firstn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"where "firstn 0 s = []" | "firstn (Suc n) [] = []" | "firstn (Suc n) (e#s) = e#(firstn n s)"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 autolemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" by simplemma 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 qedqedlemma 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 qedqedlemma firstn_eq [simp]: "firstn (length s) s = s" by simplemma 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 qedqedlemma 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)qeddeclare 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 qedqedlemma 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 qedqedlemma 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 simpnext from firstn_restn_s show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)" by metisqedlemma 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)qedlemma 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 simpnext from moment_restm_s show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)" by metisqedlemma 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)qedlemma 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 autonext case False from False have "length s \<le> n" by simp from firstn_ge [OF this] show ?thesis by autoqedlemma 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 simpnext case False from False and le_mn have "length s \<le> n" by simp from firstn_ge [OF this] show ?thesis by simpqedlemma 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)qedlemma 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 simpqedlemma 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 qedqedlemma 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 autoqedlemma 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 qedqedlemma 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)qedlemma 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)qedlemma 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 autoqedlemma 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 simpqed(*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 autoqedlemma 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)qedlemma 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)qedlemma 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 .qedlemma 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 simpnext case False hence "length s \<le> i" by simp from restn_ge [OF this] have "restn i s = []" . with False show ?thesis by simpqedlemma 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 autoqedlemma 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 metisnext 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 simpqedlemma 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 .qedlemma 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)qedend