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)"+ −
+ −
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"+ −
by (metis firstn_restn_s moment_def restm_def rev_append rev_rev_ident)+ −
+ −
declare restn.simps [simp del] firstn.simps[simp del]+ −
+ −
lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"+ −
by (metis firstn_ge)+ −
+ −
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)"+ −
by (metis append_eq_conv_conj firstn_ge firstn_le firstn_restn_s le_refl)+ −
lemma length_moment_le:+ −
fixes k s+ −
assumes le_k: "k \<le> length s"+ −
shows "length (moment k s) = k"+ −
by (metis assms length_firstn_le length_rev moment_def)+ −
+ −
lemma app_moment_restm: + −
fixes s1 s2+ −
shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)"+ −
by (metis app_firstn_restn length_rev moment_def restm_def rev_append rev_rev_ident)+ −
+ −
lemma length_moment_ge:+ −
fixes k s+ −
assumes le_k: "length s \<le> k"+ −
shows "length (moment k s) = (length s)"+ −
by (metis assms firstn_ge length_rev moment_def)+ −
+ −
lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"+ −
by (metis length_firstn_ge length_firstn_le nat_le_linear)+ −
+ −
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)"+ −
by (metis app_moment_restm append_take_drop_id assms drop_drop length_drop moment_def restn.simps)+ −
+ −
(*+ −
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"+ −
by (metis assms firstn_le length_rev moment_def rev_append)+ −
+ −
lemma moment_eq [simp]: "moment (length s) (s'@s) = s"+ −
by (metis app_moment_restm)+ −
+ −
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"+ −
by (metis down_to_def from_to_conc le_ij le_jk rev_append)+ −
+ −
lemma restn_ge:+ −
fixes s k+ −
assumes le_k: "length s \<le> k"+ −
shows "restn k s = []"+ −
by (metis assms diff_is_0_eq moment_def moment_zero restn.simps)+ −
+ −
lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []"+ −
by (metis firstn_nil from_to_def restn_ge)+ −
+ −
(*+ −
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"+ −
by (metis app_moment_restm append_Nil2 append_take_drop_id assms diff_is_0_eq' drop_take firstn_restn_s from_to_def length_drop moment_def moment_zero restn.simps)+ −
+ −
lemma down_to_moment: "down_to k 0 s = moment k s"+ −
by (metis down_to_def from_to_firstn moment_def)+ −
+ −
lemma down_to_restm:+ −
assumes le_s: "length s \<le> j"+ −
shows "down_to j k s = restm k s"+ −
by (metis assms down_to_def from_to_restn length_rev restm_def)+ −
+ −
lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s"+ −
by (metis down_to_conc down_to_moment le0 le_add1 nat_add_commute)+ −
+ −
lemma length_restn: "length (restn i s) = length s - i"+ −
by (metis diff_le_self length_firstn_le length_rev restn.simps)+ −
+ −
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"+ −
by (metis diff_le_mono from_to_def le_j length_firstn_le length_restn)+ −
+ −
lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)"+ −
by (metis diff_add_inverse2 from_to_def)+ −
+ −
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"+ −
by (metis down_to_moment down_to_moment_restm moment_split)+ −
+ −
lemma length_restm: "length (restm i s) = length s - i"+ −
by (metis length_restn length_rev restm_def)+ −
+ −
end+ −