Theory Sublist_Iteration
subsection ‹Iteration of Subsets of Factors›
theory Sublist_Iteration
imports
Polynomial_Factorization.Missing_Multiset
Polynomial_Factorization.Missing_List
"HOL-Library.IArray"
begin
paragraph ‹Misc lemmas›
lemma mem_snd_map: "(∃x. (x, y) ∈ S) ⟷ y ∈ snd ` S" by force
lemma filter_upt: assumes "l ≤ m" "m < n" shows "filter ((≤) m) [l..<n] = [m..<n]"
proof(insert assms, induct n)
case 0 then show ?case by auto
next
case (Suc n) then show ?case by (cases "m = n", auto)
qed
lemma upt_append: "i < j ⟹ j < k ⟹ [i..<j]@[j..<k] = [i..<k]"
proof(induct k arbitrary: j)
case 0 then show ?case by auto
next
case (Suc k) then show ?case by (cases "j = k", auto)
qed
lemma IArray_sub[simp]: "(!!) as = (!) (IArray.list_of as)" by auto
declare IArray.sub_def[simp del]
text ‹Following lemmas in this section are for @{const subseqs}›
lemma subseqs_Cons[simp]: "subseqs (x#xs) = map (Cons x) (subseqs xs) @ subseqs xs"
by (simp add: Let_def)
declare subseqs.simps(2) [simp del]
lemma singleton_mem_set_subseqs [simp]: "[x] ∈ set (subseqs xs) ⟷ x ∈ set xs" by (induct xs, auto)
lemma Cons_mem_set_subseqsD: "y#ys ∈ set (subseqs xs) ⟹ y ∈ set xs" by (induct xs, auto)
lemma subseqs_subset: "ys ∈ set (subseqs xs) ⟹ set ys ⊆ set xs"
by (metis Pow_iff image_eqI subseqs_powset)
lemma Cons_mem_set_subseqs_Cons:
"y#ys ∈ set (subseqs (x#xs)) ⟷ (y = x ∧ ys ∈ set (subseqs xs)) ∨ y#ys ∈ set (subseqs xs)"
by auto
lemma sorted_subseqs_sorted:
"sorted xs ⟹ ys ∈ set (subseqs xs) ⟹ sorted ys"
proof(induct xs arbitrary: ys)
case Nil thus ?case by simp
next
case Cons thus ?case using subseqs_subset by fastforce
qed
lemma subseqs_of_subseq: "ys ∈ set (subseqs xs) ⟹ set (subseqs ys) ⊆ set (subseqs xs)"
proof(induct xs arbitrary: ys)
case Nil then show ?case by auto
next
case IHx: (Cons x xs)
from IHx.prems show ?case
proof(induct ys)
case Nil then show ?case by auto
next
case IHy: (Cons y ys)
from IHy.prems[unfolded subseqs_Cons]
consider "y = x" "ys ∈ set (subseqs xs)" | "y # ys ∈ set (subseqs xs)" by auto
then show ?case
proof(cases)
case 1 with IHx.hyps show ?thesis by auto
next
case 2 from IHx.hyps[OF this] show ?thesis by auto
qed
qed
qed
lemma mem_set_subseqs_append: "xs ∈ set (subseqs ys) ⟹ xs ∈ set (subseqs (zs @ ys))"
by (induct zs, auto)
lemma Cons_mem_set_subseqs_append:
"x ∈ set ys ⟹ xs ∈ set (subseqs zs) ⟹ x#xs ∈ set (subseqs (ys@zs))"
proof(induct ys)
case Nil then show ?case by auto
next
case IH: (Cons y ys)
then consider "x = y" | "x ∈ set ys" by auto
then show ?case
proof(cases)
case 1 with IH show ?thesis by (auto intro: mem_set_subseqs_append)
next
case 2 from IH.hyps[OF this IH.prems(2)] show ?thesis by auto
qed
qed
lemma Cons_mem_set_subseqs_sorted:
"sorted xs ⟹ y#ys ∈ set (subseqs xs) ⟹ y#ys ∈ set (subseqs (filter (λx. y ≤ x) xs))"
by (induct xs) (auto simp: Let_def)
lemma subseqs_map[simp]: "subseqs (map f xs) = map (map f) (subseqs xs)" by (induct xs, auto)
lemma subseqs_of_indices: "map (map (nth xs)) (subseqs [0..<length xs]) = subseqs xs"
proof (induct xs)
case Nil then show ?case by auto
next
case (Cons x xs)
from this[symmetric]
have "subseqs xs = map (map ((!) (x#xs))) (subseqs [Suc 0..<Suc (length xs)])"
by (fold map_Suc_upt, simp)
then show ?case by (unfold length_Cons upt_conv_Cons[OF zero_less_Suc], simp)
qed
paragraph ‹Specification›
definition "subseq_of_length n xs ys ≡ ys ∈ set (subseqs xs) ∧ length ys = n"
lemma subseq_of_lengthI[intro]:
assumes "ys ∈ set (subseqs xs)" "length ys = n"
shows "subseq_of_length n xs ys"
by (insert assms, unfold subseq_of_length_def, auto)
lemma subseq_of_lengthD[dest]:
assumes "subseq_of_length n xs ys"
shows "ys ∈ set (subseqs xs)" "length ys = n"
by (insert assms, unfold subseq_of_length_def, auto)
lemma subseq_of_length0[simp]: "subseq_of_length 0 xs ys ⟷ ys = []" by auto
lemma subseq_of_length_Nil[simp]: "subseq_of_length n [] ys ⟷ n = 0 ∧ ys = []"
by (auto simp: subseq_of_length_def)
lemma subseq_of_length_Suc_upt:
"subseq_of_length (Suc n) [0..<m] xs ⟷
(if n = 0 then length xs = Suc 0 ∧ hd xs < m
else hd xs < hd (tl xs) ∧ subseq_of_length n [0..<m] (tl xs))" (is "?l ⟷ ?r")
proof(cases "n")
case 0
show ?thesis
proof(intro iffI)
assume l: "?l"
with 0 have 1: "length xs = Suc 0" by auto
then have xs: "xs = [hd xs]" by (metis length_0_conv length_Suc_conv list.sel(1))
with l have "[hd xs] ∈ set (subseqs [0..<m])" by auto
with 1 show "?r" by (unfold 0, auto)
next
assume ?r
with 0 have 1: "length xs = Suc 0" and 2: "hd xs < m" by auto
then have xs: "xs = [hd xs]" by (metis length_0_conv length_Suc_conv list.sel(1))
from 2 show "?l" by (subst xs, auto simp: 0)
qed
next
case n: (Suc n')
show ?thesis
proof (intro iffI)
assume "?l"
with n have 1: "length xs = Suc (Suc n')" and 2: "xs ∈ set (subseqs [0..<m])" by auto
from 1[unfolded length_Suc_conv]
obtain x y ys where xs: "xs = x#y#ys" and n': "length ys = n'" by auto
have "sorted xs" by(rule sorted_subseqs_sorted[OF _ 2], auto)
from this[unfolded xs] have "x ≤ y" by auto
moreover
from 2 have "distinct xs" by (rule subseqs_distinctD, auto)
from this[unfolded xs] have "x ≠ y" by auto
ultimately have "x < y" by auto
moreover
from 2 have "y#ys ∈ set (subseqs [0..<m])" by (unfold xs, auto dest: Cons_in_subseqsD)
with n n' have "subseq_of_length n [0..<m] (y#ys)" by auto
ultimately show ?r by (auto simp: xs)
next
assume r: "?r"
with n have len: "length xs = Suc (Suc n')"
and *: "hd xs < hd (tl xs)" "tl xs ∈ set (subseqs [0..<m])" by auto
from len[unfolded length_Suc_conv] obtain x y ys
where xs: "xs = x#y#ys" and n': "length ys = n'" by auto
with * have xy: "x < y" and yys: "y#ys ∈ set (subseqs [0..<m])" by auto
from Cons_mem_set_subseqs_sorted[OF _ yys]
have "y#ys ∈ set (subseqs (filter ((≤) y) [0..<m]))" by auto
also from Cons_mem_set_subseqsD[OF yys] have ym: "y < m" by auto
then have "filter ((≤) y) [0..<m] = [y..<m]" by (auto intro: filter_upt)
finally have "y#ys ∈ set (subseqs [y..<m])" by auto
with xy have "x#y#ys ∈ set (subseqs (x#[y..<m]))" by auto
also from xy have "... ⊆ set (subseqs ([0..<y] @ [y..<m]))"
by (intro subseqs_of_subseq Cons_mem_set_subseqs_append, auto intro: subseqs_refl)
also from xy ym have "[0..<y] @ [y..<m] = [0..<m]" by (auto intro: upt_append)
finally have "xs ∈ set (subseqs [0..<m])" by (unfold xs)
with len[folded n] show ?l by auto
qed
qed
lemma subseqs_of_length_of_indices:
"{ ys. subseq_of_length n xs ys } = { map (nth xs) is | is. subseq_of_length n [0..<length xs] is }"
by(unfold subseq_of_length_def, subst subseqs_of_indices[symmetric], auto)
lemma subseqs_of_length_Suc_Cons:
"{ ys. subseq_of_length (Suc n) (x#xs) ys } =
Cons x ` { ys. subseq_of_length n xs ys } ∪ { ys. subseq_of_length (Suc n) xs ys }"
by (unfold subseq_of_length_def, auto)