Theory Multihole_Context
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›