(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) 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)