theory List_Util
imports
Logic_Util
"~~/src/HOL/Library/Monad_Syntax"
"$AFP/Polynomial_Factorization/Missing_List"
begin
subsection ‹Partitions›
text ‹Check whether a list of sets forms a partition, i.e.,
whether the sets are pairwise disjoint.›
definition is_partition :: "('a set) list ⇒ bool" where
"is_partition cs ⟷ (∀j<length cs. ∀i<j. cs ! i ∩ cs ! j = {})"
definition is_partition_alt :: "('a set) list ⇒ bool" where
"is_partition_alt cs ⟷ (∀ i j. i < length cs ∧ j < length cs ∧ i ≠ j ⟶ cs!i ∩ cs!j = {})"
lemma is_partition_alt: "is_partition = is_partition_alt"
proof (intro ext)
fix cs :: "'a set list"
{
assume "is_partition_alt cs"
hence "is_partition cs" unfolding is_partition_def is_partition_alt_def by auto
}
moreover
{
assume part: "is_partition cs"
have "is_partition_alt cs" unfolding is_partition_alt_def
proof (intro allI impI)
fix i j
assume "i < length cs ∧ j < length cs ∧ i ≠ j"
with part show "cs ! i ∩ cs ! j = {}"
unfolding is_partition_def
by (cases "i < j", simp, cases "j < i", force, simp)
qed
}
ultimately
show "is_partition cs = is_partition_alt cs" by auto
qed
lemma is_partition_Nil:
"is_partition [] = True" unfolding is_partition_def by auto
lemma is_partition_Cons:
"is_partition (x#xs) ⟷ is_partition xs ∧ x ∩ ⋃(set xs) = {}" (is "?l = ?r")
proof
assume ?l
have one: "is_partition xs"
proof (unfold is_partition_def, intro allI impI)
fix j i assume "j < length xs" and "i < j"
hence "Suc j < length(x#xs)" and "Suc i < Suc j" by auto
from ‹?l›[unfolded is_partition_def,THEN spec,THEN mp,THEN spec,THEN mp,OF this]
have "(x#xs)!(Suc i) ∩ (x#xs)!(Suc j) = {}" .
thus "xs!i ∩ xs!j = {}" by simp
qed
have two: "x ∩ ⋃(set xs) = {}"
proof (rule ccontr)
assume "x ∩ ⋃(set xs) ≠ {}"
then obtain y where "y ∈ x" and "y ∈ ⋃(set xs)" by auto
then obtain z where "z ∈ set xs" and "y ∈ z" by auto
then obtain i where "i < length xs" and "xs!i = z" using in_set_conv_nth[of z xs] by auto
with ‹y ∈ z› have "y ∈ (x#xs)!Suc i" by auto
moreover with ‹y ∈ x› have "y ∈ (x#xs)!0" by simp
ultimately have "(x#xs)!0 ∩ (x#xs)!Suc i ≠ {}" by auto
moreover from ‹i < length xs› have "Suc i < length(x#xs)" by simp
ultimately show False using ‹?l›[unfolded is_partition_def] by best
qed
from one two show ?r ..
next
assume ?r
show ?l
proof (unfold is_partition_def, intro allI impI)
fix j i
assume j: "j < length (x # xs)"
assume i: "i < j"
from i obtain j' where j': "j = Suc j'" by (cases j, auto)
with j have j'len: "j' < length xs" and j'elem: "(x # xs) ! j = xs ! j'" by auto
show "(x # xs) ! i ∩ (x # xs) ! j = {}"
proof (cases i)
case 0
with j'elem have "(x # xs) ! i ∩ (x # xs) ! j = x ∩ xs ! j'" by auto
also have "… ⊆ x ∩ ⋃(set xs)" using j'len by force
finally show ?thesis using ‹?r› by auto
next
case (Suc i')
with i j' have i'j': "i' < j'" by auto
from Suc j' have "(x # xs) ! i ∩ (x # xs) ! j = xs ! i' ∩ xs ! j'" by auto
with ‹?r› i'j' j'len show ?thesis unfolding is_partition_def by auto
qed
qed
qed
lemma is_partition_sublist:
assumes "is_partition (us @ xs @ ys @ zs @ vs)"
shows "is_partition (xs @ zs)"
proof (rule ccontr)
assume "¬ is_partition (xs @ zs)"
then obtain i j where j:"j < length (xs @ zs)" and i:"i < j" and *:"(xs @ zs) ! i ∩ (xs @ zs) ! j ≠ {}"
unfolding is_partition_def by blast
then show False
proof (cases "j < length xs")
case True
let ?m = "j + length us"
let ?n = "i + length us"
from True have "?m < length (us @ xs @ ys @ zs @ vs)" by auto
moreover from i have "?n < ?m" by auto
moreover have "(us @ xs @ ys @ zs @ vs) ! ?n ∩ (us @ xs @ ys @ zs @ vs) ! ?m ≠ {}"
using i True * nth_append
by (metis (no_types, lifting) add_diff_cancel_right' not_add_less2 order.strict_trans)
ultimately show False using assms unfolding is_partition_def by auto
next
case False
let ?m = "j + length us + length ys"
from j have m:"?m < length (us @ xs @ ys @ zs @ vs)" by auto
have mj:"(us @ (xs @ ys @ zs @ vs)) ! ?m = (xs @ zs) ! j" unfolding nth_append using False j by auto
show False
proof (cases "i < length xs")
case True
let ?n = "i + length us"
from i have "?n < ?m" by auto
moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i" by (simp add: True nth_append)
ultimately show False using * m assms mj unfolding is_partition_def by blast
next
case False
let ?n = "i + length us + length ys"
from i have i:"?n < ?m" by auto
moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i"
unfolding nth_append using False i j less_diff_conv2 by auto
ultimately show False using * m assms mj unfolding is_partition_def by blast
qed
qed
qed
lemma is_partition_inj_map:
assumes "is_partition xs"
and "inj_on f (⋃x ∈ set xs. x)"
shows "is_partition (map (op ` f) xs)"
proof (rule ccontr)
assume "¬ is_partition (map (op ` f) xs)"
then obtain i j where neq:"i ≠ j"
and i:"i < length (map (op ` f) xs)" and j:"j < length (map (op ` f) xs)"
and "map (op ` f) xs ! i ∩ map (op ` f) xs ! j ≠ {}"
unfolding is_partition_alt is_partition_alt_def by auto
then obtain x where "x ∈ map (op ` f) xs ! i" and "x ∈ map (op ` f) xs ! j" by auto
then obtain y z where yi:"y ∈ xs ! i" and yx:"f y = x" and zj:"z ∈ xs ! j" and zx:"f z = x"
using i j by auto
show False
proof (cases "y = z")
case True
with zj yi neq assms(1) i j show ?thesis by (auto simp: is_partition_alt is_partition_alt_def)
next
case False
have "y ∈ (⋃x ∈ set xs. x)" using yi i by force
moreover have "z ∈ (⋃x ∈ set xs. x)" using zj j by force
ultimately show ?thesis using assms(2) inj_on_def[of f "(⋃x∈set xs. x)"] False zx yx by blast
qed
qed
context
begin
private fun is_partition_impl :: "'a set list ⇒ 'a set option" where
"is_partition_impl [] = Some {}"
| "is_partition_impl (as # rest) = do {
all ← is_partition_impl rest;
if as ∩ all = {} then Some (all ∪ as) else None
}"
lemma [code]: "is_partition as = (is_partition_impl as ≠ None)"
proof -
note [simp] = is_partition_Cons is_partition_Nil
have "⋀ bs. (is_partition as = (is_partition_impl as ≠ None)) ∧
(is_partition_impl as = Some bs ⟶ bs = ⋃ (set as))"
proof (induct as)
case (Cons as rest bs)
show ?case
proof (cases "is_partition rest")
case False
thus ?thesis using Cons by auto
next
case True
with Cons obtain c where rest: "is_partition_impl rest = Some c"
by (cases "is_partition_impl rest", auto)
with Cons True show ?thesis by auto
qed
qed auto
thus ?thesis by blast
qed
end
lemma case_prod_partition:
"case_prod f (partition p xs) = f (filter p xs) (filter (Not ∘ p) xs)"
by simp
lemmas map_id[simp] = list.map_id
subsection ‹merging functions›
definition fun_merge :: "('a ⇒ 'b)list ⇒ 'a set list ⇒ 'a ⇒ 'b"
where "fun_merge fs as a ≡ (fs ! (LEAST i. i < length as ∧ a ∈ as ! i)) a"
lemma fun_merge: assumes
i: "i < length as"
and a: "a ∈ as ! i"
and ident: "⋀ i j a. i < length as ⟹ j < length as ⟹ a ∈ as ! i ⟹ a ∈ as ! j ⟹ (fs ! i) a = (fs ! j) a"
shows "fun_merge fs as a = (fs ! i) a"
proof -
let ?p = "λ i. i < length as ∧ a ∈ as ! i"
let ?l = "LEAST i. ?p i"
have p: "?p ?l"
by (rule LeastI, insert i a, auto)
show ?thesis unfolding fun_merge_def
by (rule ident[OF _ i _ a], insert p, auto)
qed
lemma fun_merge_part: assumes
part: "is_partition as"
and i: "i < length as"
and a: "a ∈ as ! i"
shows "fun_merge fs as a = (fs ! i) a"
proof(rule fun_merge[OF i a])
fix i j a
assume "i < length as" and "j < length as" and "a ∈ as ! i" and "a ∈ as ! j"
hence "i = j" using part[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto)
thus "(fs ! i) a = (fs ! j) a" by simp
qed
lemma map_nth_conv: "map f ss = map g ts ⟹ ∀i < length ss. f(ss!i) = g(ts!i)"
proof (intro allI impI)
fix i show "map f ss = map g ts ⟹ i < length ss ⟹ f(ss!i) = g(ts!i)"
proof (induct ss arbitrary: i ts)
case Nil thus ?case by (induct ts) auto
next
case (Cons s ss) thus ?case
by (induct ts, simp, (cases i, auto))
qed
qed
lemma distinct_take_drop:
assumes dist: "distinct vs" and len: "i < length vs" shows "distinct(take i vs @ drop (Suc i) vs)" (is "distinct(?xs@?ys)")
proof -
from id_take_nth_drop[OF len] have vs[symmetric]: "vs = ?xs @ vs!i # ?ys" .
with dist have "distinct ?xs" and "distinct(vs!i#?ys)" and "set ?xs ∩ set(vs!i#?ys) = {}" using distinct_append[of ?xs "vs!i#?ys"] by auto
hence "distinct ?ys" and "set ?xs ∩ set ?ys = {}" by auto
with ‹distinct ?xs› show ?thesis using distinct_append[of ?xs ?ys] vs by simp
qed
lemma map_nth_eq_conv:
assumes len: "length xs = length ys"
shows "(map f xs = ys) = (∀i<length ys. f (xs ! i) = ys ! i)" (is "?l = ?r")
proof -
have "(map f xs = ys) = (map f xs = map id ys)" by auto
also have "... = (∀ i < length ys. f (xs ! i) = id (ys ! i))"
using map_nth_conv[of f xs id ys] nth_map_conv[OF len, of f id] unfolding len
by blast
finally show ?thesis by auto
qed
lemma map_upt_len_conv:
"map (λ i . f (xs!i)) [0..<length xs] = map f xs"
by (rule nth_equalityI, auto)
lemma map_upt_add':
"map f [a..<a+b] = map (λ i. f (a + i)) [0..<b]"
by (induct b, auto)
definition generate_lists :: "nat ⇒ 'a list ⇒ 'a list list"
where "generate_lists n xs ≡ concat_lists (map (λ _. xs) [0 ..< n])"
lemma set_generate_lists[simp]: "set (generate_lists n xs) = {as. length as = n ∧ set as ⊆ set xs}"
proof -
{
fix as
have "(length as = n ∧ (∀i<n. as ! i ∈ set xs)) = (length as = n ∧ set as ⊆ set xs)"
proof -
{
assume "length as = n"
hence n: "n = length as" by auto
have "(∀i<n. as ! i ∈ set xs) = (set as ⊆ set xs)" unfolding n
unfolding all_set_conv_all_nth[of as "λ x. x ∈ set xs", symmetric] by auto
}
thus ?thesis by auto
qed
}
thus ?thesis unfolding generate_lists_def unfolding set_concat_lists by auto
qed
lemma nth_append_take:
assumes "i ≤ length xs" shows "(take i xs @ y#ys)!i = y"
proof -
from assms have a: "length(take i xs) = i" by simp
have "(take i xs @ y#ys)!(length(take i xs)) = y" by (rule nth_append_length)
thus ?thesis unfolding a .
qed
lemma nth_append_take_is_nth_conv:
assumes "i < j" and "j ≤ length xs" shows "(take j xs @ ys)!i = xs!i"
proof -
from assms have "i < length(take j xs)" by simp
hence "(take j xs @ ys)!i = take j xs ! i" unfolding nth_append by simp
thus ?thesis unfolding nth_take[OF assms(1)] .
qed
lemma nth_append_drop_is_nth_conv:
assumes "j < i" and "j ≤ length xs" and "i ≤ length xs"
shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i"
proof -
from assms have j: "length(take j xs) = j" by auto
from ‹j < i› obtain n where "Suc(j + n) = i" using less_imp_Suc_add by auto
with assms have i: "i = length(take j xs) + Suc n" by auto
have len: "Suc j + n ≤ length xs" using assms i by auto
have "(take j xs @ y # drop (Suc j) xs)!i =
(y # drop (Suc j) xs)!(i - length(take j xs))" unfolding nth_append i by auto
also have "… = (y # drop (Suc j) xs)!(Suc n)" unfolding i by simp
also have "… = (drop (Suc j) xs)!n" by simp
finally show ?thesis unfolding nth_drop[OF len] using i j by simp
qed
lemma nth_append_take_drop_is_nth_conv:
assumes "i ≤ length xs" and "j ≤ length xs" and "i ≠ j"
shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i"
proof -
from assms have "i < j ∨ i > j" by auto
thus ?thesis
proof
assume "i < j" thus ?thesis using assms by (auto simp: nth_append_take_is_nth_conv)
next
assume "j < i" thus ?thesis using assms by (auto simp: nth_append_drop_is_nth_conv)
qed
qed
lemma take_drop_imp_nth: "⟦take i ss @ x # drop (Suc i) ss = ss⟧ ⟹ x = ss!i"
proof (induct ss arbitrary: i)
case Nil thus ?case by auto
next
case (Cons s ss)
from ‹take i (s#ss) @ x # drop (Suc i) (s#ss) = (s#ss)› show ?case
proof (induct i)
case 0 thus ?case by auto
next
case (Suc i)
from Cons have IH: "take i ss @ x # drop (Suc i) ss = ss ⟹ x = ss!i" by auto
from Suc have "take i ss @ x # drop (Suc i) ss = ss" by auto
with IH show ?case by auto
qed
qed
lemma take_drop_update_first: assumes "j < length ds" and "length cs = length ds"
shows "(take j ds @ drop j cs)[j := ds ! j] = take (Suc j) ds @ drop (Suc j) cs"
using assms
proof (induct j arbitrary: ds cs)
case 0
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
show ?case unfolding ds cs by auto
next
case (Suc j)
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto
qed
lemma take_drop_update_second: assumes "j < length ds" and "length cs = length ds"
shows "(take j ds @ drop j cs)[j := cs ! j] = take j ds @ drop j cs"
using assms
proof (induct j arbitrary: ds cs)
case 0
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
show ?case unfolding ds cs by auto
next
case (Suc j)
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto)
from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto
qed
lemma nth_take_prefix:
"length ys ≤ length xs ⟹ ∀i < length ys. xs!i = ys!i ⟹ take (length ys) xs = ys"
proof (induct xs ys rule: list_induct2')
case (4 x xs y ys)
have "take (length ys) xs = ys"
by (rule 4(1), insert 4(2-3), auto)
moreover from 4(3) have "x = y" by auto
ultimately show ?case by auto
qed auto
lemma take_upt_idx:
assumes i: "i < length ls"
shows "take i ls = [ ls ! j . j ← [0..<i]]"
proof -
have e: "0 + i ≤ i" by auto
show ?thesis
using take_upt[OF e] take_map map_nth
by (metis (hide_lams, no_types) add.left_neutral i nat_less_le take_upt)
qed
fun distinct_eq :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where
"distinct_eq _ [] = True"
| "distinct_eq eq (x # xs) = ((∀ y ∈ set xs. ¬ (eq y x)) ∧ distinct_eq eq xs)"
lemma distinct_eq_append: "distinct_eq eq (xs @ ys) = (distinct_eq eq xs ∧ distinct_eq eq ys ∧ (∀ x ∈ set xs. ∀ y ∈ set ys. ¬ (eq y x)))"
by (induct xs, auto)
lemma append_Cons_nth_left:
assumes "i < length xs"
shows "(xs @ u # ys) ! i = xs ! i"
using assms nth_append[of xs _ i] by simp
lemma append_Cons_nth_middle:
assumes "i = length xs"
shows "(xs @ y # zs) ! i = y"
using assms by auto
lemma append_Cons_nth_right:
assumes "i > length xs"
shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
proof -
from assms have "i - length xs > 0" by auto
then obtain j where j: "i - length xs = Suc j" by (cases "i - length xs", auto)
thus ?thesis by (simp add: nth_append)
qed
lemma append_Cons_nth_not_middle:
assumes "i ≠ length xs"
shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
proof (cases "i < length xs")
case True
thus ?thesis by (simp add: append_Cons_nth_left)
next
case False
with assms have "i > length xs" by arith
thus ?thesis by (rule append_Cons_nth_right)
qed
lemmas append_Cons_nth = append_Cons_nth_middle append_Cons_nth_not_middle
lemma concat_all_nth:
assumes "length xs = length ys"
and "⋀i. i < length xs ⟹ length (xs ! i) = length (ys ! i)"
and "⋀i j. i < length xs ⟹ j < length (xs ! i) ⟹ P (xs ! i ! j) (ys ! i ! j)"
shows "∀k<length (concat xs). P (concat xs ! k) (concat ys ! k)"
using assms
proof (induct xs ys rule: list_induct2)
case (Cons x xs y ys)
from Cons(3)[of 0] have xy: "length x = length y" by simp
from Cons(4)[of 0] xy have pxy: "⋀ j. j < length x ⟹ P (x ! j) (y ! j)" by auto
{
fix i
assume i: "i < length xs"
with Cons(3)[of "Suc i"]
have len: "length (xs ! i) = length (ys ! i)" by simp
from Cons(4)[of "Suc i"] i have "⋀ j. j < length (xs ! i) ⟹ P (xs ! i ! j) (ys ! i ! j)"
by auto
note len and this
}
from Cons(2)[OF this] have ind: "⋀ k. k < length (concat xs) ⟹ P (concat xs ! k) (concat ys ! k)"
by auto
show ?case unfolding concat.simps
proof (intro allI impI)
fix k
assume k: "k < length (x @ concat xs)"
show "P ((x @ concat xs) ! k) ((y @ concat ys) ! k)"
proof (cases "k < length x")
case True
show ?thesis unfolding nth_append using True xy pxy[OF True]
by simp
next
case False
with k have "k - (length x) < length (concat xs)" by auto
then obtain n where n: "k - length x = n" and nxs: "n < length (concat xs)" by auto
show ?thesis unfolding nth_append n n[unfolded xy] using False xy ind[OF nxs]
by auto
qed
qed
qed auto
lemma eq_length_concat_nth:
assumes "length xs = length ys"
and "⋀i. i < length xs ⟹ length (xs ! i) = length (ys ! i)"
shows "length (concat xs) = length (concat ys)"
using assms
proof (induct xs ys rule: list_induct2)
case (Cons x xs y ys)
from Cons(3)[of 0] have xy: "length x = length y" by simp
{
fix i
assume "i < length xs"
with Cons(3)[of "Suc i"]
have "length (xs ! i) = length (ys ! i)" by simp
}
from Cons(2)[OF this] have ind: "length (concat xs) = length (concat ys)" by simp
show ?case using xy ind by auto
qed auto
primrec
list_union :: "'a list ⇒ 'a list ⇒ 'a list"
where
"list_union [] ys = ys"
| "list_union (x # xs) ys = (let zs = list_union xs ys in if x ∈ set zs then zs else x # zs)"
lemma set_list_union[simp]: "set (list_union xs ys) = set xs ∪ set ys"
proof (induct xs)
case (Cons x xs) thus ?case by (cases "x ∈ set (list_union xs ys)") (auto)
qed simp
declare list_union.simps[simp del]
fun list_inter :: "'a list ⇒ 'a list ⇒ 'a list" where
"list_inter [] bs = []"
| "list_inter (a#as) bs =
(if a ∈ set bs then a # list_inter as bs else list_inter as bs)"
lemma set_list_inter[simp]:
"set (list_inter xs ys) = set xs ∩ set ys"
by (induct rule: list_inter.induct) simp_all
declare list_inter.simps[simp del]
primrec list_diff :: "'a list ⇒ 'a list ⇒ 'a list" where
"list_diff [] ys = []"
| "list_diff (x # xs) ys = (let zs = list_diff xs ys in if x ∈ set ys then zs else x # zs)"
lemma set_list_diff[simp]:
"set (list_diff xs ys) = set xs - set ys"
proof (induct xs)
case (Cons x xs) thus ?case by (cases "x ∈ set ys") (auto)
qed simp
declare list_diff.simps[simp del]
lemma nth_drop_0: "0 < length ss ⟹ (ss!0)#drop (Suc 0) ss = ss" by (induct ss) auto
lemma set_foldr_remdups_set_map_conv[simp]:
"set (foldr (λx xs. remdups (f x @ xs)) xs []) = ⋃(set (map (set ∘ f) xs))"
by (induct xs) auto
lemma [code_unfold]: "set xs ⊆ set ys ⟷ list_all (λx. x ∈ set ys) xs"
unfolding list_all_iff by auto
fun union_list_sorted where
"union_list_sorted (x # xs) (y # ys) =
(if x = y then x # union_list_sorted xs ys
else if x < y then x # union_list_sorted xs (y # ys)
else y # union_list_sorted (x # xs) ys)"
| "union_list_sorted [] ys = ys"
| "union_list_sorted xs [] = xs"
lemma [simp]: "set (union_list_sorted xs ys) = set xs ∪ set ys"
by (induct xs ys rule: union_list_sorted.induct, auto)
fun subtract_list_sorted :: "('a :: linorder) list ⇒ 'a list ⇒ 'a list" where
"subtract_list_sorted (x # xs) (y # ys) =
(if x = y then subtract_list_sorted xs (y # ys)
else if x < y then x # subtract_list_sorted xs (y # ys)
else subtract_list_sorted (x # xs) ys)"
| "subtract_list_sorted [] ys = []"
| "subtract_list_sorted xs [] = xs"
lemma set_subtract_list_sorted[simp]: "sorted xs ⟹ sorted ys ⟹
set (subtract_list_sorted xs ys) = set xs - set ys"
proof (induct xs ys rule: subtract_list_sorted.induct)
case (1 x xs y ys)
have xxs: "sorted (x # xs)" by fact
have yys: "sorted (y # ys)" by fact
have xs: "sorted xs" using xxs by (cases, auto)
show ?case
proof (cases "x = y")
case True
thus ?thesis using 1(1)[OF True xs yys] by auto
next
case False note neq = this
note IH = 1(2-3)[OF this]
show ?thesis
by (cases "x < y", insert IH xxs yys False, auto simp: sorted_Cons)
qed
qed auto
lemma subset_subtract_listed_sorted: "set (subtract_list_sorted xs ys) ⊆ set xs"
by (induct xs ys rule: subtract_list_sorted.induct, auto)
lemma set_subtract_list_distinct[simp]: "distinct xs ⟹ distinct (subtract_list_sorted xs ys)"
by (induct xs ys rule: subtract_list_sorted.induct, insert subset_subtract_listed_sorted, auto)
lemma distinct_remdups_adj [simp]: "sorted xs ⟹ distinct (remdups_adj xs)"
by (induct xs rule: remdups_adj.induct) (auto simp add: sorted_Cons)
definition "remdups_sort xs = remdups_adj (sort xs)"
lemma remdups_sort[simp]: "sorted (remdups_sort xs)" "set (remdups_sort xs) = set xs"
"distinct (remdups_sort xs)"
by (simp_all add: remdups_sort_def)
text ‹maximum and minimum›
lemma max_list_mono: assumes "⋀ x. x ∈ set xs - set ys ⟹ ∃ y. y ∈ set ys ∧ x ≤ y"
shows "max_list xs ≤ max_list ys"
using assms
proof (induct xs)
case (Cons x xs)
have "x ≤ max_list ys"
proof (cases "x ∈ set ys")
case True
from max_list[OF this] show ?thesis .
next
case False
with Cons(2)[of x] obtain y where y: "y ∈ set ys"
and xy: "x ≤ y" by auto
from xy max_list[OF y] show ?thesis by arith
qed
moreover have "max_list xs ≤ max_list ys"
by (rule Cons(1)[OF Cons(2)], auto)
ultimately show ?case by auto
qed auto
fun min_list :: "('a :: linorder) list ⇒ 'a" where
"min_list [x] = x"
| "min_list (x # xs) = min x (min_list xs)"
lemma min_list: "(x :: 'a :: linorder) ∈ set xs ⟹ min_list xs ≤ x"
proof (induct xs, simp)
case (Cons y ys) note oCons = this
show ?case
proof (cases ys)
case Nil
thus ?thesis using Cons by auto
next
case (Cons z zs)
hence id: "min_list (y # ys) = min y (min_list ys)"
by auto
show ?thesis
proof (cases "x = y")
case True
show ?thesis unfolding id True by auto
next
case False
have "min y (min_list ys) ≤ min_list ys" by auto
also have "... ≤ x" using oCons False by auto
finally show ?thesis unfolding id .
qed
qed
qed
lemma min_list_Cons:
assumes xy: "x ≤ y"
and len: "length xs = length ys"
and xsys: "min_list xs ≤ min_list ys"
shows "min_list (x # xs) ≤ min_list (y # ys)"
proof (cases xs)
case Nil
with len have ys: "ys = []" by simp
with xy Nil show ?thesis by simp
next
case (Cons x' xs')
with len obtain y' ys' where ys: "ys = y' # ys'" by (cases ys, auto)
from Cons have one: "min_list (x # xs) = min x (min_list xs)" by auto
from ys have two: "min_list (y # ys) = min y (min_list ys)" by auto
show ?thesis unfolding one two using xy xsys
unfolding min_def by auto
qed
lemma min_list_nth:
assumes "length xs = length ys"
and "⋀i. i < length ys ⟹ xs ! i ≤ ys ! i"
shows "min_list xs ≤ min_list ys"
using assms
proof (induct xs arbitrary: ys)
case Nil
thus ?case by auto
next
case (Cons x xs zs)
from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto)
note Cons = Cons[unfolded zs]
from Cons(2) have len: "length xs = length ys" by simp
from Cons(3)[of 0] have xy: "x ≤ y" by simp
{
fix i
assume "i < length xs"
with Cons(3)[of "Suc i"] Cons(2)
have "xs ! i ≤ ys ! i" by simp
}
from Cons(1)[OF len this] Cons(2) have ind: "min_list xs ≤ min_list ys" by simp
show ?case unfolding zs
by (rule min_list_Cons[OF xy len ind])
qed
lemma min_list_ex:
assumes "xs ≠ []" shows "∃x∈set xs. min_list xs = x"
using assms
proof (induct xs)
case Nil thus ?case by simp
next
case (Cons x xs) note oCons = this
show ?case
proof (cases xs)
case Nil
thus ?thesis by auto
next
case (Cons y ys)
hence id: "min_list (x # xs) = min x (min_list xs)" and nNil: "xs ≠ []" by auto
show ?thesis
proof (cases "x ≤ min_list xs")
case True
show ?thesis unfolding id
by (rule bexI[of _ x], insert True, auto simp: min_def)
next
case False
show ?thesis unfolding id min_def
using oCons(1)[OF nNil] False by auto
qed
qed
qed
lemma min_list_subset:
assumes subset: "set ys ⊆ set xs" and mem: "min_list xs ∈ set ys"
shows "min_list xs = min_list ys"
proof -
from subset mem have "xs ≠ []" by auto
from min_list_ex[OF this] obtain x where x: "x ∈ set xs" and mx: "min_list xs = x" by auto
from min_list[OF mem] have two: "min_list ys ≤ min_list xs" by auto
from mem have "ys ≠ []" by auto
from min_list_ex[OF this] obtain y where y: "y ∈ set ys" and my: "min_list ys = y" by auto
from y subset have "y ∈ set xs" by auto
from min_list[OF this] have one: "min_list xs ≤ y" by auto
from one two
show ?thesis unfolding mx my by auto
qed
text‹Apply a permutation to a list.›
primrec permut_aux :: "'a list ⇒ (nat ⇒ nat) ⇒ 'a list ⇒ 'a list" where
"permut_aux [] _ _ = []" |
"permut_aux (a # as) f bs = (bs ! f 0) # (permut_aux as (λn. f (Suc n)) bs)"
definition permut :: "'a list ⇒ (nat ⇒ nat) ⇒ 'a list" where
"permut as f = permut_aux as f as"
declare permut_def[simp]
lemma permut_aux_sound:
assumes "i < length as"
shows "permut_aux as f bs ! i = bs ! (f i)"
using assms proof (induct as arbitrary: i f bs)
case Nil thus ?case by simp
next
case (Cons x xs)
show ?case proof (cases i)
case 0 thus ?thesis by simp
next
case (Suc j)
with Cons(2) have "j < length xs" by simp
from Cons(1)[OF this] and Suc show ?thesis by simp
qed
qed
lemma permut_sound:
assumes "i < length as"
shows "permut as f ! i = as ! (f i)"
using assms and permut_aux_sound by simp
lemma permut_aux_length:
assumes "bij_betw f {..<length as} {..<length bs}"
shows "length (permut_aux as f bs) = length as"
by (induct as arbitrary: f bs, simp_all)
lemma permut_length:
assumes "bij_betw f {..< length as} {..< length as}"
shows "length (permut as f) = length as"
using permut_aux_length[OF assms] by simp
lemma foldl_assoc:
fixes b :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a" (infixl "⋅" 55)
assumes "⋀f g h. f ⋅ (g ⋅ h) = f ⋅ g ⋅ h"
shows "foldl op ⋅ (x ⋅ y) zs = x ⋅ foldl op ⋅ y zs"
using assms[symmetric] by (induct zs arbitrary: y) simp_all
lemma foldr_assoc:
assumes "⋀f g h. b (b f g) h = b f (b g h)"
shows "foldr b xs (b y z) = b (foldr b xs y) z"
using assms by (induct xs) simp_all
lemma foldl_foldr_o_id:
"foldl op ∘ id fs = foldr op ∘ fs id"
proof (induct fs)
case Nil show ?case by simp
next
case (Cons f fs)
have "id ∘ f = f ∘ id" by simp
with Cons [symmetric] show ?case
by (simp only: foldl_Cons foldr_Cons o_apply [of _ _ id] foldl_assoc o_assoc)
qed
lemma foldr_o_o_id[simp]:
"foldr (op ∘ ∘ f) xs id a = foldr f xs a"
by (induct xs) simp_all
lemma Ex_list_of_length_P:
assumes "∀i<n. ∃x. P x i"
shows "∃xs. length xs = n ∧ (∀i<n. P (xs ! i) i)"
proof -
from assms have "∀ i. ∃ x. i < n ⟶ P x i" by simp
from choice[OF this] obtain xs where xs: "⋀ i. i < n ⟹ P (xs i) i" by auto
show ?thesis
by (rule exI[of _ "map xs [0 ..< n]"], insert xs, auto)
qed
lemma ex_set_conv_ex_nth: "(∃x∈set xs. P x) = (∃i<length xs. P (xs ! i))"
using in_set_conv_nth[of _ xs] by force
lemma map_eq_set_zipD [dest]:
assumes "map f xs = map f ys"
and "(x, y) ∈ set (zip xs ys)"
shows "f x = f y"
using assms
proof (induct xs arbitrary: ys)
case (Cons x xs)
then show ?case by (cases ys) auto
qed simp
fun span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list" where
"span P (x # xs) =
(if P x then let (ys, zs) = span P xs in (x # ys, zs)
else ([], x # xs))" |
"span _ [] = ([], [])"
lemma span[simp]: "span P xs = (takeWhile P xs, dropWhile P xs)"
by (induct xs, auto)
declare span.simps[simp del]
lemma parallel_list_update: assumes
one_update: "⋀ xs i y. length xs = n ⟹ i < n ⟹ r (xs ! i) y ⟹ p xs ⟹ p (xs[i := y])"
and init: "length xs = n" "p xs"
and rel: "length ys = n" "⋀ i. i < n ⟹ r (xs ! i) (ys ! i)"
shows "p ys"
proof -
note len = rel(1) init(1)
{
fix i
assume "i ≤ n"
hence "p (take i ys @ drop i xs)"
proof (induct i)
case 0 with init show ?case by simp
next
case (Suc i)
hence IH: "p (take i ys @ drop i xs)" by simp
from Suc have i: "i < n" by simp
let ?xs = "(take i ys @ drop i xs)"
have "length ?xs = n" using i len by simp
from one_update[OF this i _ IH, of "ys ! i"] rel(2)[OF i] i len
show ?case by (simp add: nth_append take_drop_update_first)
qed
}
from this[of n] show ?thesis using len by auto
qed
lemma nth_concat_two_lists:
"i < length (concat (xs :: 'a list list)) ⟹ length (ys :: 'b list list) = length xs
⟹ (⋀ i. i < length xs ⟹ length (ys ! i) = length (xs ! i))
⟹ ∃ j k. j < length xs ∧ k < length (xs ! j) ∧ (concat xs) ! i = xs ! j ! k ∧
(concat ys) ! i = ys ! j ! k"
proof (induct xs arbitrary: i ys)
case (Cons x xs i yys)
then obtain y ys where yys: "yys = y # ys" by (cases yys, auto)
note Cons = Cons[unfolded yys]
from Cons(4)[of 0] have [simp]: "length y = length x" by simp
show ?case
proof (cases "i < length x")
case True
show ?thesis unfolding yys
by (rule exI[of _ 0], rule exI[of _ i], insert True Cons(2-4), auto simp: nth_append)
next
case False
let ?i = "i - length x"
from False Cons(2-3) have "?i < length (concat xs)" "length ys = length xs" by auto
note IH = Cons(1)[OF this]
{
fix i
assume "i < length xs"
with Cons(4)[of "Suc i"] have "length (ys ! i) = length (xs ! i)" by simp
}
from IH[OF this]
obtain j k where IH1: "j < length xs" "k < length (xs ! j)"
"concat xs ! ?i = xs ! j ! k"
"concat ys ! ?i = ys ! j ! k" by auto
show ?thesis unfolding yys
by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH1 False, auto simp: nth_append)
qed
qed simp
fun remdups_gen :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list" where
"remdups_gen f [] = []"
| "remdups_gen f (x # xs) = x # remdups_gen f [y <- xs. ¬ f x = f y]"
lemma remdups_gen_subset: "set (remdups_gen f xs) ⊆ set xs"
by (induct f xs rule: remdups_gen.induct, auto)
lemma remdups_gen_elem_imp_elem: "x ∈ set (remdups_gen f xs) ⟹ x ∈ set xs"
using remdups_gen_subset[of f xs] by blast
lemma elem_imp_remdups_gen_elem: "x ∈ set xs ⟹ ∃ y ∈ set (remdups_gen f xs). f x = f y"
proof (induct f xs rule: remdups_gen.induct)
case (2 f z zs)
show ?case
proof (cases "f x = f z")
case False
with 2(2) have "x ∈ set [y←zs . f z ≠ f y]" by auto
from 2(1)[OF this] show ?thesis by auto
qed auto
qed auto
lemma take_nth_drop_concat:
assumes "i < length xss" and "xss ! i = ys"
and "j < length ys" and "ys ! j = z"
shows "∃k < length (concat xss).
take k (concat xss) = concat (take i xss) @ take j ys ∧
concat xss ! k = xss ! i ! j ∧
drop (Suc k) (concat xss) = drop (Suc j) ys @ concat (drop (Suc i) xss)"
using assms(1, 2)
proof (induct xss arbitrary: i rule: List.rev_induct)
case (snoc xs xss)
then show ?case using assms by (cases "i < length xss") (auto simp: nth_append)
qed simp
lemma concat_map_empty [simp]:
"concat (map (λ_. []) xs) = []"
by simp
lemma map_upt_len_same_len_conv:
assumes "length xs = length ys"
shows "map (λi. f (xs ! i)) [0 ..< length ys] = map f xs"
unfolding assms [symmetric] by (rule map_upt_len_conv)
lemma concat_map_concat [simp]:
"concat (map concat xs) = concat (concat xs)"
by (induct xs) simp_all
lemma concat_concat_map:
"concat (concat (map f xs)) = concat (map (concat ∘ f) xs)"
by (induct xs) simp_all
lemma UN_upt_len_conv [simp]:
"length xs = n ⟹ (⋃i ∈ {0 ..< n}. f (xs ! i)) = ⋃set (map f xs)"
by (force simp: in_set_conv_nth)
lemma Ball_at_Least0LessThan_conv [simp]:
"length xs = n ⟹
(∀i ∈ {0 ..< n}. P (xs ! i)) ⟷ (∀x ∈ set xs. P x)"
by (metis atLeast0LessThan in_set_conv_nth lessThan_iff)
lemma listsum_replicate_length [simp]:
"listsum (replicate (length xs) (Suc 0)) = length xs"
by (induct xs) simp_all
lemma list_all2_in_set2:
assumes "list_all2 P xs ys" and "y ∈ set ys"
obtains x where "x ∈ set xs" and "P x y"
using assms by (induct) auto
lemma map_eq_conv':
"map f xs = map g ys ⟷ length xs = length ys ∧ (∀i < length xs. f (xs ! i) = g (ys ! i))"
by (auto dest: map_eq_imp_length_eq map_nth_conv simp: nth_map_conv)
end