# Theory Polynomials.Utils

```(* Author: Alexander Maletzky *)

section ‹Utilities›

theory Utils
imports Main Well_Quasi_Orders.Almost_Full_Relations
begin

lemma subset_imageE_inj:
assumes "B ⊆ f ` A"
obtains C where "C ⊆ A" and "B = f ` C" and "inj_on f C"
proof -
define g where "g = (λx. SOME a. a ∈ A ∧ f a = x)"
have "g b ∈ A ∧ f (g b) = b" if "b ∈ B" for b
proof -
from that assms have "b ∈ f ` A" ..
then obtain a where "a ∈ A" and "b = f a" ..
hence "a ∈ A ∧ f a = b" by simp
thus ?thesis unfolding g_def by (rule someI)
qed
hence 1: "⋀b. b ∈ B ⟹ g b ∈ A" and 2: "⋀b. b ∈ B ⟹ f (g b) = b" by simp_all
let ?C = "g ` B"
show ?thesis
proof
show "?C ⊆ A" by (auto intro: 1)
next
show "B = f ` ?C"
proof (rule set_eqI)
fix b
show "b ∈ B ⟷ b ∈ f ` ?C"
proof
assume "b ∈ B"
moreover from this have "f (g b) = b" by (rule 2)
ultimately show "b ∈ f ` ?C" by force
next
assume "b ∈ f ` ?C"
then obtain b' where "b' ∈ B" and "b = f (g b')" unfolding image_image ..
moreover from this(1) have "f (g b') = b'" by (rule 2)
ultimately show "b ∈ B" by simp
qed
qed
next
show "inj_on f ?C"
proof
fix x y
assume "x ∈ ?C"
then obtain bx where "bx ∈ B" and x: "x = g bx" ..
moreover from this(1) have "f (g bx) = bx" by (rule 2)
ultimately have *: "f x = bx" by simp
assume "y ∈ ?C"
then obtain "by" where "by ∈ B" and y: "y = g by" ..
moreover from this(1) have "f (g by) = by" by (rule 2)
ultimately have "f y = by" by simp
moreover assume "f x = f y"
ultimately have "bx = by" using * by simp
thus "x = y" by (simp only: x y)
qed
qed
qed

lemma wfP_chain:
assumes "¬(∃f. ∀i. r (f (Suc i)) (f i))"
shows "wfP r"
proof -
from assms wf_iff_no_infinite_down_chain[of "{(x, y). r x y}"] have "wf {(x, y). r x y}" by auto
thus "wfP r" unfolding wfP_def .
qed

lemma transp_sequence:
assumes "transp r" and "⋀i. r (seq (Suc i)) (seq i)" and "i < j"
shows "r (seq j) (seq i)"
proof -
have "⋀k. r (seq (i + Suc k)) (seq i)"
proof -
fix k::nat
show "r (seq (i + Suc k)) (seq i)"
proof (induct k)
case 0
from assms(2) have "r (seq (Suc i)) (seq i)" .
thus ?case by simp
next
case (Suc k)
note assms(1)
moreover from assms(2) have "r (seq (Suc (Suc i + k))) (seq (Suc (i + k)))" by simp
moreover have "r (seq (Suc (i + k))) (seq i)" using Suc.hyps by simp
ultimately have "r (seq (Suc (Suc i + k))) (seq i)" by (rule transpD)
thus ?case by simp
qed
qed
hence "r (seq (i + Suc(j - i - 1))) (seq i)" .
thus "r (seq j) (seq i)" using ‹i < j› by simp
qed

lemma almost_full_on_finite_subsetE:
assumes "reflp P" and "almost_full_on P S"
obtains T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. P t s)"
proof -
define crit where "crit = (λU s. s ∈ S ∧ (∀u∈U. ¬ P u s))"
have critD: "s ∉ U" if "crit U s" for U s
proof
assume "s ∈ U"
from ‹crit U s› have "∀u∈U. ¬ P u s" unfolding crit_def ..
from this ‹s ∈ U› have "¬ P s s" ..
moreover from assms(1) have "P s s" by (rule reflpD)
ultimately show False ..
qed
define "fun"
where "fun = (λU. (if (∃s. crit U s) then
insert (SOME s. crit U s) U
else
U
))"
define seq where "seq = rec_nat {} (λ_. fun)"
have seq_Suc: "seq (Suc i) = fun (seq i)" for i by (simp add: seq_def)

have seq_incr_Suc: "seq i ⊆ seq (Suc i)" for i by (auto simp add: seq_Suc fun_def)
have seq_incr: "i ≤ j ⟹ seq i ⊆ seq j" for i j
proof -
assume "i ≤ j"
hence "i = j ∨ i < j" by auto
thus "seq i ⊆ seq j"
proof
assume "i = j"
thus ?thesis by simp
next
assume "i < j"
with _ seq_incr_Suc show ?thesis by (rule transp_sequence, simp add: transp_def)
qed
qed
have sub: "seq i ⊆ S" for i
fix i
assume "Ex (crit (seq i))"
hence "crit (seq i) (Eps (crit (seq i)))" by (rule someI_ex)
thus "Eps (crit (seq i)) ∈ S" by (simp add: crit_def)
qed
have "∃i. seq (Suc i) = seq i"
proof (rule ccontr, simp)
assume "∀i. seq (Suc i) ≠ seq i"
with seq_incr_Suc have "seq i ⊂ seq (Suc i)" for i by blast
define seq1 where "seq1 = (λn. (SOME s. s ∈ seq (Suc n) ∧ s ∉ seq n))"
have seq1: "seq1 n ∈ seq (Suc n) ∧ seq1 n ∉ seq n" for n unfolding seq1_def
proof (rule someI_ex)
from ‹seq n ⊂ seq (Suc n)› show "∃x. x ∈ seq (Suc n) ∧ x ∉ seq n" by blast
qed
have "seq1 i ∈ S" for i
proof
from seq1[of i] show "seq1 i ∈ seq (Suc i)" ..
qed (fact sub)
with assms(2) obtain a b where "a < b" and "P (seq1 a) (seq1 b)" by (rule almost_full_onD)
from ‹a < b› have "Suc a ≤ b" by simp
from seq1 have "seq1 a ∈ seq (Suc a)" ..
also from ‹Suc a ≤ b› have "... ⊆ seq b" by (rule seq_incr)
finally have "seq1 a ∈ seq b" .
from seq1 have "seq1 b ∈ seq (Suc b)" and "seq1 b ∉ seq b" by blast+
hence "crit (seq b) (seq1 b)" by (simp add: seq_Suc fun_def someI split: if_splits)
hence "∀u∈seq b. ¬ P u (seq1 b)" by (simp add: crit_def)
from this ‹seq1 a ∈ seq b› have "¬ P (seq1 a) (seq1 b)" ..
from this ‹P (seq1 a) (seq1 b)› show False ..
qed
then obtain i where "seq (Suc i) = seq i" ..
show ?thesis
proof
show "finite (seq i)" by (induct i, simp_all add: seq_def fun_def)
next
fix s
assume "s ∈ S"
let ?s = "Eps (crit (seq i))"
show "∃t∈seq i. P t s"
proof (rule ccontr, simp)
assume "∀t∈seq i. ¬ P t s"
with ‹s ∈ S› have "crit (seq i) s" by (simp only: crit_def)
hence "crit (seq i) ?s" and eq: "seq (Suc i) = insert ?s (seq i)"
by (auto simp add: seq_Suc fun_def intro: someI)
from this(1) have "?s ∉ seq i" by (rule critD)
hence "seq (Suc i) ≠ seq i" unfolding eq by blast
from this ‹seq (Suc i) = seq i› show False ..
qed
qed (fact sub)
qed

subsection ‹Lists›

lemma map_upt: "map (λi. f (xs ! i)) [0..<length xs] = map f xs"
by (auto intro: nth_equalityI)

lemma map_upt_zip:
assumes "length xs = length ys"
shows "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] = map (λ(x, y). f x y) (zip xs ys)" (is "?l = ?r")
proof -
have len_l: "length ?l = length ys" by simp
from assms have len_r: "length ?r = length ys" by simp
show ?thesis
proof (simp only: list_eq_iff_nth_eq len_l len_r, rule, rule, intro allI impI)
fix i
assume "i < length ys"
hence "i < length ?l" and "i < length ?r" by (simp_all only: len_l len_r)
thus "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] ! i = map (λ(x, y). f x y) (zip xs ys) ! i"
by simp
qed
qed

lemma distinct_sorted_wrt_irrefl:
assumes "irreflp rel" and "transp rel" and "sorted_wrt rel xs"
shows "distinct xs"
using assms(3)
proof (induct xs)
case Nil
show ?case by simp
next
case (Cons x xs)
from Cons(2) have "sorted_wrt rel xs" and *: "∀y∈set xs. rel x y"
by (simp_all)
from this(1) have "distinct xs" by (rule Cons(1))
show ?case
proof (simp add: ‹distinct xs›, rule)
assume "x ∈ set xs"
with * have "rel x x" ..
with assms(1) show False by (simp add: irreflp_def)
qed
qed

lemma distinct_sorted_wrt_imp_sorted_wrt_strict:
assumes "distinct xs" and "sorted_wrt rel xs"
shows "sorted_wrt (λx y. rel x y ∧ ¬ x = y) xs"
using assms
proof (induct xs)
case Nil
show ?case by simp
next
case step: (Cons x xs)
show ?case
proof (cases "xs")
case Nil
thus ?thesis by simp
next
case (Cons y zs)
from step(2) have "x ≠ y" and 1: "distinct (y # zs)" by (simp_all add: Cons)
from step(3) have "rel x y" and 2: "sorted_wrt rel (y # zs)" by (simp_all add: Cons)
from 1 2 have "sorted_wrt (λx y. rel x y ∧ x ≠ y) (y # zs)" by (rule step(1)[simplified Cons])
with ‹x ≠ y› ‹rel x y› show ?thesis using step.prems by (auto simp: Cons)
qed
qed

lemma sorted_wrt_distinct_set_unique:
assumes "antisymp rel"
assumes "sorted_wrt rel xs" "distinct xs" "sorted_wrt rel ys" "distinct ys" "set xs = set ys"
shows "xs = ys"
proof -
from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
from assms(2-6) show ?thesis
proof(induct rule:list_induct2[OF 1])
case 1
show ?case by simp
next
case (2 x xs y ys)
from 2(4) have "x ∉ set xs" and "distinct xs" by simp_all
from 2(6) have "y ∉ set ys" and "distinct ys" by simp_all
have "x = y"
proof (rule ccontr)
assume "x ≠ y"
from 2(3) have "∀z∈set xs. rel x z" by (simp)
moreover from ‹x ≠ y› have "y ∈ set xs" using 2(7) by auto
ultimately have *: "rel x y" ..
from 2(5) have "∀z∈set ys. rel y z" by (simp)
moreover from ‹x ≠ y› have "x ∈ set ys" using 2(7) by auto
ultimately have "rel y x" ..
with assms(1) * have "x = y" by (rule antisympD)
with ‹x ≠ y› show False ..
qed
from 2(3) have "sorted_wrt rel xs" by (simp)
moreover note ‹distinct xs›
moreover from 2(5) have "sorted_wrt rel ys" by (simp)
moreover note ‹distinct ys›
moreover from 2(7) ‹x ∉ set xs› ‹y ∉ set ys› have "set xs = set ys" by (auto simp add: ‹x = y›)
ultimately have "xs = ys" by (rule 2(2))
with ‹x = y› show ?case by simp
qed
qed

lemma sorted_wrt_refl_nth_mono:
assumes "reflp P" and "sorted_wrt P xs" and "i ≤ j" and "j < length xs"
shows "P (xs ! i) (xs ! j)"
proof (cases "i < j")
case True
from assms(2) this assms(4) show ?thesis by (rule sorted_wrt_nth_less)
next
case False
with assms(3) have "i = j" by simp
from assms(1) show ?thesis unfolding ‹i = j› by (rule reflpD)
qed

fun merge_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ 'a list" where
"merge_wrt _ xs [] = xs"|
"merge_wrt rel [] ys = ys"|
"merge_wrt rel (x # xs) (y # ys) =
(if x = y then
y # (merge_wrt rel xs ys)
else if rel x y then
x # (merge_wrt rel xs (y # ys))
else
y # (merge_wrt rel (x # xs) ys)
)"

lemma set_merge_wrt: "set (merge_wrt rel xs ys) = set xs ∪ set ys"
proof (induct rel xs ys rule: merge_wrt.induct)
case (1 rel xs)
show ?case by simp
next
case (2 rel y ys)
show ?case by simp
next
case (3 rel x xs y ys)
show ?case
proof (cases "x = y")
case True
thus ?thesis by (simp add: 3(1))
next
case False
show ?thesis
proof (cases "rel x y")
case True
with ‹x ≠ y› show ?thesis by (simp add: 3(2) insert_commute)
next
case False
with ‹x ≠ y› show ?thesis by (simp add: 3(3))
qed
qed
qed

lemma sorted_merge_wrt:
assumes "transp rel" and "⋀x y. x ≠ y ⟹ rel x y ∨ rel y x"
and "sorted_wrt rel xs" and "sorted_wrt rel ys"
shows "sorted_wrt rel (merge_wrt rel xs ys)"
using assms
proof (induct rel xs ys rule: merge_wrt.induct)
case (1 rel xs)
from 1(3) show ?case by simp
next
case (2 rel y ys)
from 2(4) show ?case by simp
next
case (3 rel x xs y ys)
show ?case
proof (cases "x = y")
case True
show ?thesis
fix z
assume "z ∈ set (merge_wrt rel xs ys)"
hence "z ∈ set xs ∪ set ys" by (simp only: set_merge_wrt)
thus "rel y z"
proof
assume "z ∈ set xs"
with 3(6) show ?thesis by (simp add: True)
next
assume "z ∈ set ys"
with 3(7) show ?thesis by (simp)
qed
next
note True 3(4, 5)
moreover from 3(6) have "sorted_wrt rel xs" by (simp)
moreover from 3(7) have "sorted_wrt rel ys" by (simp)
ultimately show "sorted_wrt rel (merge_wrt rel xs ys)" by (rule 3(1))
qed
next
case False
show ?thesis
proof (cases "rel x y")
case True
show ?thesis
proof (auto simp add: False True)
fix z
assume "z ∈ set (merge_wrt rel xs (y # ys))"
hence "z ∈ insert y (set xs ∪ set ys)" by (simp add: set_merge_wrt)
thus "rel x z"
proof
assume "z = y"
with True show ?thesis by simp
next
assume "z ∈ set xs ∪ set ys"
thus ?thesis
proof
assume "z ∈ set xs"
with 3(6) show ?thesis by (simp)
next
assume "z ∈ set ys"
with 3(7) have "rel y z" by (simp)
with 3(4) True show ?thesis by (rule transpD)
qed
qed
next
note False True 3(4, 5)
moreover from 3(6) have "sorted_wrt rel xs" by (simp)
ultimately show "sorted_wrt rel (merge_wrt rel xs (y # ys))" using 3(7) by (rule 3(2))
qed
next
assume "¬ rel x y"
from ‹x ≠ y› have "rel x y ∨ rel y x" by (rule 3(5))
with ‹¬ rel x y› have *: "rel y x" by simp
show ?thesis
proof (auto simp add: False ‹¬ rel x y›)
fix z
assume "z ∈ set (merge_wrt rel (x # xs) ys)"
hence "z ∈ insert x (set xs ∪ set ys)" by (simp add: set_merge_wrt)
thus "rel y z"
proof
assume "z = x"
with * show ?thesis by simp
next
assume "z ∈ set xs ∪ set ys"
thus ?thesis
proof
assume "z ∈ set xs"
with 3(6) have "rel x z" by (simp)
with 3(4) * show ?thesis by (rule transpD)
next
assume "z ∈ set ys"
with 3(7) show ?thesis by (simp)
qed
qed
next
note False ‹¬ rel x y› 3(4, 5, 6)
moreover from 3(7) have "sorted_wrt rel ys" by (simp)
ultimately show "sorted_wrt rel (merge_wrt rel (x # xs) ys)" by (rule 3(3))
qed
qed
qed
qed

lemma set_fold:
assumes "⋀x ys. set (f (g x) ys) = set (g x) ∪ set ys"
shows "set (fold (λx. f (g x)) xs ys) = (⋃x∈set xs. set (g x)) ∪ set ys"
proof (induct xs arbitrary: ys)
case Nil
show ?case by simp
next
case (Cons x xs)
have eq: "set (fold (λx. f (g x)) xs (f (g x) ys)) = (⋃x∈set xs. set (g x)) ∪ set (f (g x) ys)"
by (rule Cons)
show ?case by (simp add: o_def assms set_merge_wrt eq ac_simps)
qed

subsection ‹Sums and Products›

assumes "⋀x y. f (x + y) = f x + ((f (y::'a::monoid_add))::'b::cancel_comm_monoid_add)"
shows "f 0 = 0"
proof -
have "f (0 + 0) = f 0 + f 0" by (rule assms)
hence "f 0 = f 0 + f 0" by simp
thus "f 0 = 0" by simp
qed

lemma fun_sum_commute:
assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
shows "f (sum g A) = (∑a∈A. f (g a))"
proof (cases "finite A")
case True
thus ?thesis
proof (induct A)
case empty
thus ?case by (simp add: assms(1))
next
case step: (insert a A)
show ?case by (simp add: sum.insert[OF step(1) step(2)] assms(2) step(3))
qed
next
case False
thus ?thesis by (simp add: assms(1))
qed

lemma fun_sum_commute_canc:
assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)"
shows "f (sum g A) = (∑a∈A. f (g a))"
by (rule fun_sum_commute, rule additive_implies_homogenous, fact+)

lemma fun_sum_list_commute:
assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
shows "f (sum_list xs) = sum_list (map f xs)"
proof (induct xs)
case Nil
thus ?case by (simp add: assms(1))
next
case (Cons x xs)
thus ?case by (simp add: assms(2))
qed

lemma fun_sum_list_commute_canc:
assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)"
shows "f (sum_list xs) = sum_list (map f xs)"
by (rule fun_sum_list_commute, rule additive_implies_homogenous, fact+)

lemma sum_set_upt_eq_sum_list: "(∑i = m..<n. f i) = (∑i←[m..<n]. f i)"
using sum_set_upt_conv_sum_list_nat by auto

lemma sum_list_upt: "(∑i←[0..<(length xs)]. f (xs ! i)) = (∑x←xs. f x)"
by (simp only: map_upt)

lemma sum_list_upt_zip:
assumes "length xs = length ys"
shows "(∑i←[0..<(length ys)]. f (xs ! i) (ys ! i)) = (∑(x, y)←(zip xs ys). f x y)"
by (simp only: map_upt_zip[OF assms])

lemma sum_list_zeroI:
assumes "set xs ⊆ {0}"
shows "sum_list xs = 0"
using assms by (induct xs, auto)

lemma fun_prod_commute:
assumes "f 1 = 1" and "⋀x y. f (x * y) = f x * f y"
shows "f (prod g A) = (∏a∈A. f (g a))"
proof (cases "finite A")
case True
thus ?thesis
proof (induct A)
case empty
thus ?case by (simp add: assms(1))
next
case step: (insert a A)
show ?case by (simp add: prod.insert[OF step(1) step(2)] assms(2) step(3))
qed
next
case False
thus ?thesis by (simp add: assms(1))
qed

end (* theory *)
```