(* Author: Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at> (2015) Author: Christian Sternagel <c.sternagel@gmail.com> (2013-2016) Author: Martin Avanzini <martin.avanzini@uibk.ac.at> (2014) Author: René Thiemann <rene.thiemann@uibk.ac.at> (2013-2015) Author: Julian Nagele <julian.nagele@uibk.ac.at> (2016) License: LGPL (see file COPYING.LESSER) *) section ‹Preliminaries› subsection ‹Multihole Contexts› theory Multihole_Context imports Utils begin unbundle lattice_syntax subsubsection ‹Partitioning lists into chunks of given length› lemma concat_nth: assumes "m < length xs" and "n < length (xs ! m)" and "i = sum_list (map length (take m xs)) + n" shows "concat xs ! i = xs ! m ! n" using assms proof (induct xs arbitrary: m n i) case (Cons x xs) show ?case proof (cases m) case 0 then show ?thesis using Cons by (simp add: nth_append) next case (Suc k) with Cons(1) [of k n "i - length x"] and Cons(2-) show ?thesis by (simp_all add: nth_append) qed qed simp lemma sum_list_take_eq: fixes xs :: "nat list" shows "k < i ⟹ i < length xs ⟹ sum_list (take i xs) = sum_list (take k xs) + xs ! k + sum_list (take (i - Suc k) (drop (Suc k) xs))" by (subst id_take_nth_drop [of k]) (auto simp: min_def drop_take) fun partition_by where "partition_by xs [] = []" | "partition_by xs (y#ys) = take y xs # partition_by (drop y xs) ys" lemma partition_by_map0_append [simp]: "partition_by xs (map (λx. 0) ys @ zs) = replicate (length ys) [] @ partition_by xs zs" by (induct ys) simp_all lemma concat_partition_by [simp]: "sum_list ys = length xs ⟹ concat (partition_by xs ys) = xs" by (induct ys arbitrary: xs) simp_all definition partition_by_idx where "partition_by_idx l ys i j = partition_by [0..<l] ys ! i ! j" lemma partition_by_nth_nth_old: assumes "i < length (partition_by xs ys)" and "j < length (partition_by xs ys ! i)" and "sum_list ys = length xs" shows "partition_by xs ys ! i ! j = xs ! (sum_list (map length (take i (partition_by xs ys))) + j)" using concat_nth [OF assms(1, 2) refl] unfolding concat_partition_by [OF assms(3)] by simp lemma map_map_partition_by: "map (map f) (partition_by xs ys) = partition_by (map f xs) ys" by (induct ys arbitrary: xs) (auto simp: take_map drop_map) lemma length_partition_by [simp]: "length (partition_by xs ys) = length ys" by (induct ys arbitrary: xs) simp_all lemma partition_by_Nil [simp]: "partition_by [] ys = replicate (length ys) []" by (induct ys) simp_all lemma partition_by_concat_id [simp]: assumes "length xss = length ys" and "⋀i. i < length ys ⟹ length (xss ! i) = ys ! i" shows "partition_by (concat xss) ys = xss" using assms by (induct ys arbitrary: xss) (simp, case_tac xss, simp, fastforce) lemma partition_by_nth: "i < length ys ⟹ partition_by xs ys ! i = take (ys ! i) (drop (sum_list (take i ys)) xs)" by (induct ys arbitrary: xs i) (simp, case_tac i, simp_all add: ac_simps) lemma partition_by_nth_less: assumes "k < i" and "i < length zs" and "length xs = sum_list (take i zs) + j" shows "partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)" proof - have "partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))" using assms by (auto simp: partition_by_nth) moreover have "zs ! k + sum_list (take k zs) ≤ length xs" using assms by (simp add: sum_list_take_eq) ultimately show ?thesis by simp qed lemma partition_by_nth_greater: assumes "i < k" and "k < length zs" and "j < zs ! i" and "length xs = sum_list (take i zs) + j" shows "partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))" proof - have "partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))" using assms by (auto simp: partition_by_nth) moreover have "sum_list (take k zs) > length xs" using assms by (auto simp: sum_list_take_eq) ultimately show ?thesis by (auto) (metis Suc_diff_Suc drop_Suc_Cons) qed lemma length_partition_by_nth: "sum_list ys = length xs ⟹ i < length ys ⟹ length (partition_by xs ys ! i) = ys ! i" by (induct ys arbitrary: xs i; case_tac i) auto lemma partition_by_nth_nth_elem: assumes "sum_list ys = length xs" "i < length ys" "j < ys ! i" shows "partition_by xs ys ! i ! j ∈ set xs" proof - from assms have "j < length (partition_by xs ys ! i)" by (simp only: length_partition_by_nth) then have "partition_by xs ys ! i ! j ∈ set (partition_by xs ys ! i)" by auto with assms(2) have "partition_by xs ys ! i ! j ∈ set (concat (partition_by xs ys))" by auto then show ?thesis using assms by simp qed lemma partition_by_nth_nth: assumes "sum_list ys = length xs" "i < length ys" "j < ys ! i" shows "partition_by xs ys ! i ! j = xs ! partition_by_idx (length xs) ys i j" "partition_by_idx (length xs) ys i j < length xs" unfolding partition_by_idx_def proof - let ?n = "partition_by [0..<length xs] ys ! i ! j" show "?n < length xs" using partition_by_nth_nth_elem[OF _ assms(2,3), of "[0..<length xs]"] assms(1) by simp have li: "i < length (partition_by [0..<length xs] ys)" using assms(2) by simp have lj: "j < length (partition_by [0..<length xs] ys ! i)" using assms by (simp add: length_partition_by_nth) have "partition_by (map ((!) xs) [0..<length xs]) ys ! i ! j = xs ! ?n" by (simp only: map_map_partition_by[symmetric] nth_map[OF li] nth_map[OF lj]) then show "partition_by xs ys ! i ! j = xs ! ?n" by (simp add: map_nth) qed lemma map_length_partition_by [simp]: "sum_list ys = length xs ⟹ map length (partition_by xs ys) = ys" by (intro nth_equalityI, auto simp: length_partition_by_nth) lemma map_partition_by_nth [simp]: "i < length ys ⟹ map f (partition_by xs ys ! i) = partition_by (map f xs) ys ! i" by (induct ys arbitrary: i xs) (simp, case_tac i, simp_all add: take_map drop_map) lemma sum_list_partition_by [simp]: "sum_list ys = length xs ⟹ sum_list (map (λx. sum_list (map f x)) (partition_by xs ys)) = sum_list (map f xs)" by (induct ys arbitrary: xs) (simp_all, metis append_take_drop_id sum_list_append map_append) lemma partition_by_map_conv: "partition_by xs ys = map (λi. take (ys ! i) (drop (sum_list (take i ys)) xs)) [0 ..< length ys]" by (rule nth_equalityI) (simp_all add: partition_by_nth) lemma UN_set_partition_by_map: "sum_list ys = length xs ⟹ (⋃x∈set (partition_by (map f xs) ys). ⋃ (set x)) = ⋃(set (map f xs))" by (induct ys arbitrary: xs) (simp_all add: drop_map take_map, metis UN_Un append_take_drop_id set_append) lemma UN_set_partition_by: "sum_list ys = length xs ⟹ (⋃zs ∈ set (partition_by xs ys). ⋃x ∈ set zs. f x) = (⋃x ∈ set xs. f x)" by (induct ys arbitrary: xs) (simp_all, metis UN_Un append_take_drop_id set_append) lemma Ball_atLeast0LessThan_partition_by_conv: "(∀i∈{0..<length ys}. ∀x∈set (partition_by xs ys ! i). P x) = (∀x ∈ ⋃(set (map set (partition_by xs ys))). P x)" by auto (metis atLeast0LessThan in_set_conv_nth length_partition_by lessThan_iff) lemma Ball_set_partition_by: "sum_list ys = length xs ⟹ (∀x ∈ set (partition_by xs ys). ∀y ∈ set x. P y) = (∀x ∈ set xs. P x)" proof (induct ys arbitrary: xs) case (Cons y ys) then show ?case apply (subst (2) append_take_drop_id [of y xs, symmetric]) apply (simp only: set_append) apply auto done qed simp lemma partition_by_append2: "partition_by xs (ys @ zs) = partition_by (take (sum_list ys) xs) ys @ partition_by (drop (sum_list ys) xs) zs" by (induct ys arbitrary: xs) (auto simp: drop_take ac_simps split: split_min) lemma partition_by_concat2: "partition_by xs (concat ys) = concat (map (λi . partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])" proof - have *: "map (λi . partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys] = map (λ(x,y). partition_by x y) (zip (partition_by xs (map sum_list ys)) ys)" using zip_nth_conv[of "partition_by xs (map sum_list ys)" ys] by auto show ?thesis unfolding * by (induct ys arbitrary: xs) (auto simp: partition_by_append2) qed lemma partition_by_partition_by: "length xs = sum_list (map sum_list ys) ⟹ partition_by (partition_by xs (concat ys)) (map length ys) = map (λi. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys]" by (auto simp: partition_by_concat2 intro: partition_by_concat_id) subsubsection ‹Multihole contexts definition and functionalities›