Theory Polynomial_Factorization.Missing_List
subsection ‹Missing List›
text ‹The provides some standard algorithms and lemmas on lists.›
theory Missing_List
imports
Matrix.Utility
"HOL-Library.Monad_Syntax"
begin
fun concat_lists :: "'a list list ⇒ 'a list list" where
"concat_lists [] = [[]]"
| "concat_lists (as # xs) = concat (map (λvec. map (λa. a # vec) as) (concat_lists xs))"
lemma concat_lists_listset: "set (concat_lists xs) = listset (map set xs)"
by (induct xs, auto simp: set_Cons_def)
lemma sum_list_concat: "sum_list (concat ls) = sum_list (map sum_list ls)"
by (induct ls, auto)
lemma listset: "listset xs = { ys. length ys = length xs ∧ (∀ i < length xs. ys ! i ∈ xs ! i)}"
proof (induct xs)
case (Cons x xs)
let ?n = "length xs"
from Cons
have "?case = (set_Cons x {ys. length ys = ?n ∧ (∀i < ?n. ys ! i ∈ xs ! i)} =
{ys. length ys = Suc ?n ∧ ys ! 0 ∈ x ∧ (∀i < ?n. ys ! Suc i ∈ xs ! i)})"
(is "_ = (?L = ?R)")
by (auto simp: all_Suc_conv)
also have "?L = ?R"
by (auto simp: set_Cons_def, case_tac xa, auto)
finally show ?case by simp
qed auto
lemma set_concat_lists[simp]: "set (concat_lists xs) = {as. length as = length xs ∧ (∀i<length xs. as ! i ∈ set (xs ! i))}"
unfolding concat_lists_listset listset by simp
declare concat_lists.simps[simp del]
fun find_map_filter :: "('a ⇒ 'b) ⇒ ('b ⇒ bool) ⇒ 'a list ⇒ 'b option" where
"find_map_filter f p [] = None"
| "find_map_filter f p (a # as) = (let b = f a in if p b then Some b else find_map_filter f p as)"
lemma find_map_filter_Some: "find_map_filter f p as = Some b ⟹ p b ∧ b ∈ f ` set as"
by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits)
lemma find_map_filter_None: "find_map_filter f p as = None ⟹ ∀ b ∈ f ` set as. ¬ p b"
by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits)
lemma remdups_adj_sorted_distinct[simp]: "sorted xs ⟹ distinct (remdups_adj xs)"
by (induct xs rule: remdups_adj.induct) (auto)
lemma subseqs_length_simple:
assumes "b ∈ set (subseqs xs)" shows "length b ≤ length xs"
using assms by(induct xs arbitrary:b;auto simp:Let_def Suc_leD)
lemma subseqs_length_simple_False:
assumes "b ∈ set (subseqs xs)" " length xs < length b" shows False
using assms subseqs_length_simple by fastforce
lemma empty_subseqs[simp]: "[] ∈ set (subseqs xs)" by (induct xs, auto simp: Let_def)
lemma full_list_subseqs: "{ys. ys ∈ set (subseqs xs) ∧ length ys = length xs} = {xs}"
proof (induct xs)
case (Cons x xs)
have "?case = ({ys ∈ (#) x ` set (subseqs xs) ∪ set (subseqs xs).
length ys = Suc (length xs)} = (#) x ` {xs})" (is "_ = (?l = ?r)")
by (auto simp: Let_def)
also have "?l = {ys ∈ (#) x ` set (subseqs xs). length ys = Suc (length xs)}"
using length_subseqs[of xs]
using subseqs_length_simple_False by force
also have "… = (#) x ` {ys ∈ set (subseqs xs). length ys = length xs}"
by auto
also have "… = (#) x ` {xs}" unfolding Cons by auto
finally show ?case by simp
qed simp
lemma nth_concat_split: assumes "i < length (concat xs)"
shows "∃ j k. j < length xs ∧ k < length (xs ! j) ∧ concat xs ! i = xs ! j ! k"
using assms
proof (induct xs arbitrary: i)
case (Cons x xs i)
define I where "I = i - length x"
show ?case
proof (cases "i < length x")
case True note l = this
hence i: "concat (Cons x xs) ! i = x ! i" by (auto simp: nth_append)
show ?thesis unfolding i
by (rule exI[of _ 0], rule exI[of _ i], insert Cons l, auto)
next
case False note l = this
from l Cons(2) have i: "i = length x + I" "I < length (concat xs)" unfolding I_def by auto
hence iI: "concat (Cons x xs) ! i = concat xs ! I" by (auto simp: nth_append)
from Cons(1)[OF i(2)] obtain j k where
IH: "j < length xs ∧ k < length (xs ! j) ∧ concat xs ! I = xs ! j ! k" by auto
show ?thesis unfolding iI
by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH, auto)
qed
qed simp
lemma nth_concat_diff: assumes "i1 < length (concat xs)" "i2 < length (concat xs)" "i1 ≠ i2"
shows "∃ j1 k1 j2 k2. (j1,k1) ≠ (j2,k2) ∧ j1 < length xs ∧ j2 < length xs
∧ k1 < length (xs ! j1) ∧ k2 < length (xs ! j2)
∧ concat xs ! i1 = xs ! j1 ! k1 ∧ concat xs ! i2 = xs ! j2 ! k2"
using assms
proof (induct xs arbitrary: i1 i2)
case (Cons x xs)
define I1 where "I1 = i1 - length x"
define I2 where "I2 = i2 - length x"
show ?case
proof (cases "i1 < length x")
case True note l1 = this
hence i1: "concat (Cons x xs) ! i1 = x ! i1" by (auto simp: nth_append)
show ?thesis
proof (cases "i2 < length x")
case True note l2 = this
hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append)
show ?thesis unfolding i1 i2
by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ 0], rule exI[of _ i2],
insert Cons(4) l1 l2, auto)
next
case False note l2 = this
from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto
hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append)
from nth_concat_split[OF i22(2)] obtain j2 k2 where
*: "j2 < length xs ∧ k2 < length (xs ! j2) ∧ concat xs ! I2 = xs ! j2 ! k2" by auto
show ?thesis unfolding i1 i2
by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ "Suc j2"], rule exI[of _ k2],
insert * l1, auto)
qed
next
case False note l1 = this
from l1 Cons(2) have i11: "i1 = length x + I1" "I1 < length (concat xs)" unfolding I1_def by auto
hence i1: "concat (Cons x xs) ! i1 = concat xs ! I1" by (auto simp: nth_append)
show ?thesis
proof (cases "i2 < length x")
case False note l2 = this
from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto
hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append)
from Cons(4) i11 i22 have diff: "I1 ≠ I2" by auto
from Cons(1)[OF i11(2) i22(2) diff] obtain j1 k1 j2 k2
where IH: "(j1,k1) ≠ (j2,k2) ∧ j1 < length xs ∧ j2 < length xs
∧ k1 < length (xs ! j1) ∧ k2 < length (xs ! j2)
∧ concat xs ! I1 = xs ! j1 ! k1 ∧ concat xs ! I2 = xs ! j2 ! k2" by auto
show ?thesis unfolding i1 i2
by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ "Suc j2"], rule exI[of _ k2],
insert IH, auto)
next
case True note l2 = this
hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append)
from nth_concat_split[OF i11(2)] obtain j1 k1 where
*: "j1 < length xs ∧ k1 < length (xs ! j1) ∧ concat xs ! I1 = xs ! j1 ! k1" by auto
show ?thesis unfolding i1 i2
by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ 0], rule exI[of _ i2],
insert * l2, auto)
qed
qed
qed auto
lemma list_all2_map_map: "(⋀ x. x ∈ set xs ⟹ R (f x) (g x)) ⟹ list_all2 R (map f xs) (map g xs)"
by (induct xs, auto)
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 ((`) f) xs)"
proof (rule ccontr)
assume "¬ is_partition (map ((`) f) xs)"
then obtain i j where neq:"i ≠ j"
and i:"i < length (map ((`) f) xs)" and j:"j < length (map ((`) f) xs)"
and "map ((`) f) xs ! i ∩ map ((`) f) xs ! j ≠ {}"
unfolding is_partition_alt is_partition_alt_def by auto
then obtain x where "x ∈ map ((`) f) xs ! i" and "x ∈ map ((`) 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 is_partition_code[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 ‹j < i› obtain n where ij: "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 using ij len 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 using assms
by (auto simp: nth_append_take_is_nth_conv nth_append_drop_is_nth_conv)
qed
lemma take_drop_imp_nth: "⟦take i ss @ x # drop (Suc i) ss = ss⟧ ⟹ x = ss!i"
proof (induct ss arbitrary: i)
case (Cons s ss)
from ‹take i (s#ss) @ x # drop (Suc i) (s#ss) = (s#ss)› show ?case
proof (induct i)
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 auto
qed auto
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 (opaque_lifting, 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"
by (simp add: assms nth_append)
lemma append_Cons_nth_not_middle:
assumes "i ≠ length xs"
shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
by (metis assms list_update_length nth_list_update_neq)
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 (simp add: Cons_nth_drop_Suc)
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 subset_set_code[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 (simp)
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)
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)
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)
case oCons : (Cons y ys)
show ?case
proof (cases ys)
case Nil
thus ?thesis using oCons by auto
next
case (Cons z zs)
hence "min_list (y # ys) = min y (min_list ys)"
by auto
then show ?thesis
using min_le_iff_disj oCons.hyps oCons.prems by auto
qed
qed simp
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)"
by (metis min_list.simps len length_greater_0_conv min.mono nth_drop_0 xsys xy)
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 (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 auto
lemma min_list_ex:
assumes "xs ≠ []" shows "∃x∈set xs. min_list xs = x"
using assms
proof (induct xs)
case oCons : (Cons x xs)
show ?case
proof (cases xs)
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 auto
qed auto
lemma min_list_subset:
assumes subset: "set ys ⊆ set xs" and mem: "min_list xs ∈ set ys"
shows "min_list xs = min_list ys"
by (metis antisym empty_iff empty_set mem min_list min_list_ex subset subsetD)
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 (Cons x xs)
show ?case
proof (cases i)
case (Suc j)
with Cons(2) have "j < length xs" by simp
from Cons(1)[OF this] and Suc show ?thesis by simp
qed simp
qed simp
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
declare permut_def[simp del]
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 (⋅) (x ⋅ y) zs = x ⋅ foldl (⋅) 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 (∘) id fs = foldr (∘) fs id"
proof (induct fs)
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 simp
lemma foldr_o_o_id[simp]:
"foldr ((∘) ∘ 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
text ‹Removing duplicates w.r.t. some function.›
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 sum_list_replicate_length [simp]:
"sum_list (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))"
using map_equality_iff map_equality_iff nth_map_conv by auto
lemma list_3_cases[case_names Nil 1 2]:
assumes "xs = [] ⟹ P"
and "⋀x. xs = [x] ⟹ P"
and "⋀x y ys. xs = x#y#ys ⟹ P"
shows P
using assms by (rule remdups_adj.cases)
lemma list_4_cases[case_names Nil 1 2 3]:
assumes "xs = [] ⟹ P"
and "⋀x. xs = [x] ⟹ P"
and "⋀x y. xs = [x,y] ⟹ P"
and "⋀x y z zs. xs = x # y # z # zs ⟹ P"
shows P
using assms by (cases xs; cases "tl xs"; cases "tl (tl xs)", auto)
lemma foldr_append2 [simp]:
"foldr ((@) ∘ f) xs (ys @ zs) = foldr ((@) ∘ f) xs ys @ zs"
by (induct xs) simp_all
lemma foldr_append2_Nil [simp]:
"foldr ((@) ∘ f) xs [] @ zs = foldr ((@) ∘ f) xs zs"
unfolding foldr_append2 [symmetric] by simp
lemma UNION_set_zip:
"(⋃x ∈ set (zip [0..<length xs] (map f xs)). g x) = (⋃i < length xs. g (i, f (xs ! i)))"
by (auto simp: set_conv_nth)
lemma zip_fst: "p ∈ set (zip as bs) ⟹ fst p ∈ set as"
by (metis in_set_zipE prod.collapse)
lemma zip_snd: "p ∈ set (zip as bs) ⟹ snd p ∈ set bs"
by (metis in_set_zipE prod.collapse)
lemma zip_size_aux: "size_list (size o snd) (zip ts ls) ≤ (size_list size ls)"
proof (induct ls arbitrary: ts)
case (Cons l ls ts)
thus ?case by (cases ts, auto)
qed auto
text‹We definie the function that remove the nth element of
a list. It uses take and drop and the soundness is therefore not
too hard to prove thanks to the already existing lemmas.›
definition remove_nth :: "nat ⇒ 'a list ⇒ 'a list" where
"remove_nth n xs ≡ (take n xs) @ (drop (Suc n) xs)"
declare remove_nth_def[simp]
lemma remove_nth_len:
assumes i: "i < length xs"
shows "length xs = Suc (length (remove_nth i xs))"
proof -
show ?thesis unfolding arg_cong[where f = "length", OF id_take_nth_drop[OF i]]
unfolding remove_nth_def by simp
qed
lemma remove_nth_length :
assumes n_bd: "n < length xs"
shows "length (remove_nth n xs) = length xs - 1"
using n_bd by force
lemma remove_nth_id : "length xs ≤ n ⟹ remove_nth n xs = xs"
by simp
lemma remove_nth_sound_l :
assumes p_ub: "p < n"
shows "(remove_nth n xs) ! p = xs ! p"
proof (cases "n < length xs")
case True
from length_take and True have ltk: "length (take n xs) = n" by simp
{
assume pltn: "p < n"
from this and ltk have plttk: "p < length (take n xs)" by simp
with nth_append[of "take n xs" _ p]
have "((take n xs) @ (drop (Suc n) xs)) ! p = take n xs ! p" by auto
with pltn and nth_take have "((take n xs) @ (drop (Suc n) xs)) ! p = xs ! p" by simp
}
from this and ltk and p_ub show ?thesis by simp
next
case False
hence "length xs ≤ n" by arith
with remove_nth_id show ?thesis by force
qed
lemma remove_nth_sound_r :
assumes "n ≤ p" and "p < length xs"
shows "(remove_nth n xs) ! p = xs ! (Suc p)"
proof-
from ‹n ≤ p› and ‹p < length xs› have n_ub: "n < length xs" by arith
from length_take and n_ub have ltk: "length (take n xs) = n" by simp
from ‹n ≤ p› and ltk and nth_append[of "take n xs" _ p]
have Hrew: "((take n xs) @ (drop (Suc n) xs)) ! p = drop (Suc n) xs ! (p - n)" by auto
from ‹n ≤ p› have idx: "Suc n + (p - n) = Suc p" by arith
from ‹p < length xs› have Sp_ub: "Suc p ≤ length xs" by arith
from idx and Sp_ub and nth_drop have Hrew': "drop (Suc n) xs ! (p - n) = xs ! (Suc p)" by simp
from Hrew and Hrew' show ?thesis by simp
qed
lemma nth_remove_nth_conv:
assumes "i < length (remove_nth n xs)"
shows "remove_nth n xs ! i = xs ! (if i < n then i else Suc i)"
using assms remove_nth_sound_l remove_nth_sound_r[of n i xs] by auto
lemma remove_nth_P_compat :
assumes aslbs: "length as = length bs"
and Pab: "∀i. i < length as ⟶ P (as ! i) (bs ! i)"
shows "∀i. i < length (remove_nth p as) ⟶ P (remove_nth p as ! i) (remove_nth p bs ! i)"
proof (cases "p < length as")
case True
hence p_ub: "p < length as" by assumption
with remove_nth_length have lr_ub: "length (remove_nth p as) = length as - 1" by auto
{
fix i assume i_ub: "i < length (remove_nth p as)"
have "P (remove_nth p as ! i) (remove_nth p bs ! i)"
proof (cases "i < p")
case True
from i_ub and lr_ub have i_ub2: "i < length as" by arith
from i_ub2 and Pab have P: "P (as ! i) (bs ! i)" by blast
from P and remove_nth_sound_l[OF True, of as] and remove_nth_sound_l[OF True, of bs]
show ?thesis by simp
next
case False
hence p_ub2: "p ≤ i" by arith
from i_ub and lr_ub have Si_ub: "Suc i < length as" by arith
with Pab have P: "P (as ! Suc i) (bs ! Suc i)" by blast
from i_ub and lr_ub have i_uba: "i < length as" by arith
from i_uba and aslbs have i_ubb: "i < length bs" by simp
from P and p_ub and aslbs and remove_nth_sound_r[OF p_ub2 i_uba]
and remove_nth_sound_r[OF p_ub2 i_ubb]
show ?thesis by auto
qed
}
thus ?thesis by simp
next
case False
hence p_lba: "length as ≤ p" by arith
with aslbs have p_lbb: "length bs ≤ p" by simp
from remove_nth_id[OF p_lba] and remove_nth_id[OF p_lbb] and Pab
show ?thesis by simp
qed
declare remove_nth_def[simp del]
definition adjust_idx :: "nat ⇒ nat ⇒ nat" where
"adjust_idx i j ≡ (if j < i then j else (Suc j))"
definition adjust_idx_rev :: "nat ⇒ nat ⇒ nat" where
"adjust_idx_rev i j ≡ (if j < i then j else j - Suc 0)"
lemma adjust_idx_rev1: "adjust_idx_rev i (adjust_idx i j) = j"
using adjust_idx_def adjust_idx_rev_def by auto
lemma adjust_idx_rev2:
assumes "j ≠ i" shows "adjust_idx i (adjust_idx_rev i j) = j"
using adjust_idx_def adjust_idx_rev_def assms by auto
lemma adjust_idx_i:
"adjust_idx i j ≠ i"
using adjust_idx_def lessI less_irrefl_nat by auto
lemma adjust_idx_nth:
assumes i: "i < length xs"
shows "remove_nth i xs ! j = xs ! adjust_idx i j" (is "?l = ?r")
proof -
let ?j = "adjust_idx i j"
from i have ltake: "length (take i xs) = i" by simp
note nth_xs = arg_cong[where f = "λ xs. xs ! ?j", OF id_take_nth_drop[OF i], unfolded nth_append ltake]
show ?thesis
proof (cases "j < i")
case True
hence j: "?j = j" unfolding adjust_idx_def by simp
show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake
using True by simp
next
case False
hence j: "?j = Suc j" unfolding adjust_idx_def by simp
from i have lxs: "min (length xs) i = i" by simp
show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append
using False by (simp add: lxs)
qed
qed
lemma adjust_idx_rev_nth:
assumes i: "i < length xs"
and ji: "j ≠ i"
shows "remove_nth i xs ! adjust_idx_rev i j = xs ! j" (is "?l = ?r")
by (simp add: adjust_idx_nth adjust_idx_rev2 i ji)
lemma adjust_idx_length:
assumes i: "i < length xs"
and j: "j < length (remove_nth i xs)"
shows "adjust_idx i j < length xs"
using adjust_idx_def i j remove_nth_len by fastforce
lemma adjust_idx_rev_length:
assumes "i < length xs"
and "j < length xs"
and "j ≠ i"
shows "adjust_idx_rev i j < length (remove_nth i xs)"
by (metis adjust_idx_def adjust_idx_rev2 assms not_less_eq remove_nth_len)
text‹If a binary relation holds on two couples of lists, then it holds on
the concatenation of the two couples.›
lemma P_as_bs_extend:
assumes lab: "length as = length bs"
and lcd: "length cs = length ds"
and nsab: "∀i. i < length bs ⟶ P (as ! i) (bs ! i)"
and nscd: "∀i. i < length ds ⟶ P (cs ! i) (ds ! i)"
shows "∀i. i < length (bs @ ds) ⟶ P ((as @ cs) ! i) ((bs @ ds) ! i)"
by (simp add: lab nsab nscd nth_append)
text‹Extension of filter and partition to binary relations.›
fun filter2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ ('a list × 'b list)" where
"filter2 P [] _ = ([], [])" |
"filter2 P _ [] = ([], [])" |
"filter2 P (a # as) (b # bs) = (if P a b
then (a # fst (filter2 P as bs), b # snd (filter2 P as bs))
else filter2 P as bs)"
lemma filter2_length:
"length (fst (filter2 P as bs)) ≡ length (snd (filter2 P as bs))"
proof (induct as arbitrary: bs)
case Nil
show ?case by simp
next
case (Cons a as) note IH = this
thus ?case proof (cases bs)
case Nil
thus ?thesis by simp
next
case (Cons b bs)
thus ?thesis proof (cases "P a b")
case True
with Cons and IH show ?thesis by simp
next
case False
with Cons and IH show ?thesis by simp
qed
qed
qed
lemma filter2_sound: "∀i. i < length (fst (filter2 P as bs)) ⟶ P (fst (filter2 P as bs) ! i) (snd (filter2 P as bs) ! i)"
proof (induct as arbitrary: bs)
case Nil
thus ?case by simp
next
case (Cons a as) note IH = this
thus ?case proof (cases bs)
case Nil
thus ?thesis by simp
next
case (Cons b bs)
thus ?thesis proof (cases "P a b")
case False
with Cons and IH show ?thesis by simp
next
case True
{
fix i
assume i_bd: "i < length (fst (filter2 P (a # as) (b # bs)))"
have "P (fst (filter2 P (a # as) (b # bs)) ! i) (snd (filter2 P (a # as) (b # bs)) ! i)" proof (cases i)
case 0
with True show ?thesis by simp
next
case (Suc j)
with i_bd and True have "j < length (fst (filter2 P as bs))" by auto
with Suc and IH and True show ?thesis by simp
qed
}
with Cons show ?thesis by simp
qed
qed
qed
definition partition2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ ('a list × 'b list) × ('a list × 'b list)" where
"partition2 P as bs ≡ ((filter2 P as bs) , (filter2 (λa b. ¬ (P a b)) as bs))"
lemma partition2_sound_P: "∀i. i < length (fst (fst (partition2 P as bs))) ⟶
P (fst (fst (partition2 P as bs)) ! i) (snd (fst (partition2 P as bs)) ! i)"
by (simp add: filter2_sound partition2_def)
lemma partition2_sound_nP: "∀i. i < length (fst (snd (partition2 P as bs))) ⟶
¬ P (fst (snd (partition2 P as bs)) ! i) (snd (snd (partition2 P as bs)) ! i)"
by (metis filter2_sound partition2_def snd_conv)
text‹Membership decision function that actually returns the
value of the index where the value can be found.›
fun mem_idx :: "'a ⇒ 'a list ⇒ nat Option.option" where
"mem_idx _ [] = None" |
"mem_idx x (a # as) = (if x = a then Some 0 else map_option Suc (mem_idx x as))"
lemma mem_idx_sound_output:
assumes "mem_idx x as = Some i"
shows "i < length as ∧ as ! i = x"
using assms proof (induct as arbitrary: i)
case Nil thus ?case by simp
next
case (Cons a as) note IH = this
thus ?case proof (cases "x = a")
case True with IH(2) show ?thesis by simp
next
case False note neq_x_a = this
show ?thesis proof (cases "mem_idx x as")
case None with IH(2) and neq_x_a show ?thesis by simp
next
case (Some j)
with IH(2) and neq_x_a have "i = Suc j" by simp
with IH(1) and Some show ?thesis by simp
qed
qed
qed
lemma mem_idx_sound_output2:
assumes "mem_idx x as = Some i"
shows "∀j. j < i ⟶ as ! j ≠ x"
using assms proof (induct as arbitrary: i)
case Nil thus ?case by simp
next
case (Cons a as) note IH = this
thus ?case proof (cases "x = a")
case True with IH show ?thesis by simp
next
case False note neq_x_a = this
show ?thesis proof (cases "mem_idx x as")
case None with IH(2) and neq_x_a show ?thesis by simp
next
case (Some j)
with IH(2) and neq_x_a have eq_i_Sj: "i = Suc j" by simp
{
fix k assume k_bd: "k < i"
have "(a # as) ! k ≠ x"
proof (cases k)
case 0 with neq_x_a show ?thesis by simp
next
case (Suc l)
with k_bd and eq_i_Sj have l_bd: "l < j" by arith
with IH(1) and Some have "as ! l ≠ x" by simp
with Suc show ?thesis by simp
qed
}
thus ?thesis by simp
qed
qed
qed
lemma mem_idx_sound:
"(x ∈ set as) = (∃i. mem_idx x as = Some i)"
proof (induct as)
case Nil thus ?case by simp
next
case (Cons a as) note IH = this
show ?case proof (cases "x = a")
case True thus ?thesis by simp
next
case False
{
assume "x ∈ set (a # as)"
with False have "x ∈ set as" by simp
with IH obtain i where Some_i: "mem_idx x as = Some i" by auto
with False have "mem_idx x (a # as) = Some (Suc i)" by simp
hence "∃i. mem_idx x (a # as) = Some i" by simp
}
moreover
{
assume "∃i. mem_idx x (a # as) = Some i"
then obtain i where Some_i: "mem_idx x (a # as) = Some i" by fast
have "x ∈ set as" proof (cases i)
case 0 with mem_idx_sound_output[OF Some_i] and False show ?thesis by simp
next
case (Suc j)
with Some_i and False have "mem_idx x as = Some j" by simp
hence "∃i. mem_idx x as = Some i" by simp
with IH show ?thesis by simp
qed
hence "x ∈ set (a # as)" by simp
}
ultimately show ?thesis by fast
qed
qed
lemma mem_idx_sound2:
"(x ∉ set as) = (mem_idx x as = None)"
unfolding mem_idx_sound by auto
lemma sum_list_replicate_mono: assumes "w1 ≤ (w2 :: nat)"
shows "sum_list (replicate n w1) ≤ sum_list (replicate n w2)"
proof (induct n)
case (Suc n)
thus ?case using ‹w1 ≤ w2› by auto
qed simp
lemma all_gt_0_sum_list_map:
assumes *: "⋀x. f x > (0::nat)"
and x: "x ∈ set xs" and len: "1 < length xs"
shows "f x < (∑x←xs. f x)"
using x len
proof (induct xs)
case (Cons y xs)
show ?case
proof (cases "y = x")
case True
with *[of "hd xs"] Cons(3) show ?thesis by (cases xs, auto)
next
case False
with Cons(2) have x: "x ∈ set xs" by auto
then obtain z zs where xs: "xs = z # zs" by (cases xs, auto)
show ?thesis
proof (cases "length zs")
case 0
with x xs *[of y] show ?thesis by auto
next
case (Suc n)
with xs have "1 < length xs" by auto
from Cons(1)[OF x this] show ?thesis by simp
qed
qed
qed simp
lemma map_of_filter:
assumes "P x"
shows "map_of [(x',y) ← ys. P x'] x = map_of ys x"
proof (induct ys)
case (Cons xy ys)
obtain x' y where xy: "xy = (x',y)" by force
show ?case
using assms local.Cons by auto
qed simp
lemma set_subset_insertI: "set xs ⊆ set (List.insert x xs)"
by auto
lemma set_removeAll_subset: "set (removeAll x xs) ⊆ set xs"
by auto
lemma map_of_append_Some:
"map_of xs y = Some z ⟹ map_of (xs @ ys) y = Some z"
by simp
lemma map_of_append_None:
"map_of xs y = None ⟹ map_of (xs @ ys) y = map_of ys y"
by (simp add: map_add_def)
end