Theory General
section ‹General Utilities›
theory General
imports Polynomials.Utils
begin
text ‹A couple of general-purpose functions and lemmas, mainly related to lists.›
subsection ‹Lists›
lemma distinct_reorder: "distinct (xs @ (y # ys)) = distinct (y # (xs @ ys))" by auto
lemma set_reorder: "set (xs @ (y # ys)) = set (y # (xs @ ys))" by simp
lemma distinctI:
assumes "⋀i j. i < j ⟹ i < length xs ⟹ j < length xs ⟹ xs ! i ≠ xs ! j"
shows "distinct xs"
by (metis assms distinct_conv_nth nat_neq_iff)
lemma filter_nth_pairE:
assumes "i < j" and "i < length (filter P xs)" and "j < length (filter P xs)"
obtains i' j' where "i' < j'" and "i' < length xs" and "j' < length xs"
and "(filter P xs) ! i = xs ! i'" and "(filter P xs) ! j = xs ! j'"
using assms
proof (induct xs arbitrary: i j thesis)
case Nil
from Nil(3) show ?case by simp
next
case (Cons x xs)
let ?ys = "filter P (x # xs)"
show ?case
proof (cases "P x")
case True
hence *: "?ys = x # (filter P xs)" by simp
from ‹i < j› obtain j0 where j: "j = Suc j0" using lessE by blast
have len_ys: "length ?ys = Suc (length (filter P xs))" and ys_j: "?ys ! j = (filter P xs) ! j0"
by (simp only: * length_Cons, simp only: j * nth_Cons_Suc)
from Cons(5) have "j0 < length (filter P xs)" unfolding len_ys j by auto
show ?thesis
proof (cases "i = 0")
case True
from ‹j0 < length (filter P xs)› obtain j' where "j' < length xs" and **: "(filter P xs) ! j0 = xs ! j'"
by (metis (no_types, lifting) in_set_conv_nth mem_Collect_eq nth_mem set_filter)
have "0 < Suc j'" by simp
thus ?thesis
by (rule Cons(2), simp, simp add: ‹j' < length xs›, simp only: True * nth_Cons_0,
simp only: ys_j nth_Cons_Suc **)
next
case False
then obtain i0 where i: "i = Suc i0" using lessE by blast
have ys_i: "?ys ! i = (filter P xs) ! i0" by (simp only: i * nth_Cons_Suc)
from Cons(3) have "i0 < j0" by (simp add: i j)
from Cons(4) have "i0 < length (filter P xs)" unfolding len_ys i by auto
from _ ‹i0 < j0› this ‹j0 < length (filter P xs)› obtain i' j'
where "i' < j'" and "i' < length xs" and "j' < length xs"
and i': "filter P xs ! i0 = xs ! i'" and j': "filter P xs ! j0 = xs ! j'"
by (rule Cons(1))
from ‹i' < j'› have "Suc i' < Suc j'" by simp
thus ?thesis
by (rule Cons(2), simp add: ‹i' < length xs›, simp add: ‹j' < length xs›,
simp only: ys_i nth_Cons_Suc i', simp only: ys_j nth_Cons_Suc j')
qed
next
case False
hence *: "?ys = filter P xs" by simp
with Cons(4) Cons(5) have "i < length (filter P xs)" and "j < length (filter P xs)" by simp_all
with _ ‹i < j› obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs"
and i': "filter P xs ! i = xs ! i'" and j': "filter P xs ! j = xs ! j'"
by (rule Cons(1))
from ‹i' < j'› have "Suc i' < Suc j'" by simp
thus ?thesis
by (rule Cons(2), simp add: ‹i' < length xs›, simp add: ‹j' < length xs›,
simp only: * nth_Cons_Suc i', simp only: * nth_Cons_Suc j')
qed
qed
lemma distinct_filterI:
assumes "⋀i j. i < j ⟹ i < length xs ⟹ j < length xs ⟹ P (xs ! i) ⟹ P (xs ! j) ⟹ xs ! i ≠ xs ! j"
shows "distinct (filter P xs)"
proof (rule distinctI)
fix i j::nat
assume "i < j" and "i < length (filter P xs)" and "j < length (filter P xs)"
then obtain i' j' where "i' < j'" and "i' < length xs" and "j' < length xs"
and i: "(filter P xs) ! i = xs ! i'" and j: "(filter P xs) ! j = xs ! j'" by (rule filter_nth_pairE)
from ‹i' < j'› ‹i' < length xs› ‹j' < length xs› show "(filter P xs) ! i ≠ (filter P xs) ! j" unfolding i j
proof (rule assms)
from ‹i < length (filter P xs)› show "P (xs ! i')" unfolding i[symmetric] using nth_mem by force
next
from ‹j < length (filter P xs)› show "P (xs ! j')" unfolding j[symmetric] using nth_mem by force
qed
qed
lemma set_zip_map: "set (zip (map f xs) (map g xs)) = (λx. (f x, g x)) ` (set xs)"
by (auto simp add: set_zip) (metis in_set_conv_nth nth_map)
lemma set_zip_map1: "set (zip (map f xs) xs) = (λx. (f x, x)) ` (set xs)"
by (metis set_zip_map map_ident)
lemma set_zip_map2: "set (zip xs (map f xs)) = (λx. (x, f x)) ` (set xs)"
by (metis (no_types, lifting) ext map_ident set_zip_map)
lemma UN_upt: "(⋃i∈{0..<length xs}. f (xs ! i)) = (⋃x∈set xs. f x)"
by (metis image_image map_nth set_map set_upt)
lemma sum_list_zeroI':
assumes "⋀i. i < length xs ⟹ xs ! i = 0"
shows "sum_list xs = 0"
by (metis assms in_set_conv_nth insert_iff subsetI sum_list_zeroI)
lemma sum_list_map2_plus:
assumes "length xs = length ys"
shows "sum_list (map2 (+) xs ys) = sum_list xs + sum_list (ys::'a::comm_monoid_add list)"
using assms
proof (induct rule: list_induct2)
case Nil
show ?case by simp
next
case (Cons x xs y ys)
show ?case by (simp add: Cons(2) ac_simps)
qed
lemma sum_list_eq_nthI:
assumes "i < length xs" and "⋀j. j < length xs ⟹ j ≠ i ⟹ xs ! j = 0"
shows "sum_list xs = xs ! i"
using assms
proof (induct xs arbitrary: i)
case Nil
from Nil(1) show ?case by simp
next
case (Cons x xs)
have *: "xs ! j = 0" if "j < length xs" and "Suc j ≠ i" for j
proof -
have "xs ! j = (x # xs) ! (Suc j)" by simp
also have "... = 0" by (rule Cons(3), simp add: ‹j < length xs›, fact)
finally show ?thesis .
qed
show ?case
proof (cases i)
case 0
have "sum_list xs = 0" by (rule sum_list_zeroI', erule *, simp add: 0)
with 0 show ?thesis by simp
next
case (Suc k)
with Cons(2) have "k < length xs" by simp
hence "sum_list xs = xs ! k"
proof (rule Cons(1))
fix j
assume "j < length xs"
assume "j ≠ k"
hence "Suc j ≠ i" by (simp add: Suc)
with ‹j < length xs› show "xs ! j = 0" by (rule *)
qed
moreover have "x = 0"
proof -
have "x = (x # xs) ! 0" by simp
also have "... = 0" by (rule Cons(3), simp_all add: Suc)
finally show ?thesis .
qed
ultimately show ?thesis by (simp add: Suc)
qed
qed
subsubsection ‹‹max_list››