section ‹Preliminaries›
theory Decreasing_Diagrams_II_Aux
imports
Well_Quasi_Orders.Multiset_Extension
Well_Quasi_Orders.Well_Quasi_Orders
begin
subsection ‹Trivialities›
lemma asymI2: "(⋀a b. (a,b) ∈ R ⟹ (b,a) ∉ R) ⟹ asym R"
by (metis asymI irrefl_def)
abbreviation "strict_order R ≡ irrefl R ∧ trans R"
lemma order_asym: "trans R ⟹ asym R = irrefl R"
unfolding asym.simps irrefl_def trans_def by meson
lemma strict_order_strict: "strict_order q ⟹ strict (λa b. (a, b) ∈ q⇧=) = (λa b. (a, b) ∈ q)"
unfolding trans_def irrefl_def by fast
lemma mono_lex1: "mono (λr. lex_prod r s)"
by (auto simp add: mono_def)
lemma mono_lex2: "mono (lex_prod r)"
by (auto simp add: mono_def)
lemma irrefl_lex_prod: "irrefl R ⟹ irrefl S ⟹ irrefl (R <*lex*> S)"
by (auto simp add: lex_prod_def irrefl_def)
lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp
converse_converse converse_Id
subsection ‹Complete lattices and least fixed points›
context complete_lattice
begin
subsubsection ‹A chain-based induction principle›
abbreviation set_chain :: "'a set ⇒ bool" where
"set_chain C ≡ ∀x ∈ C. ∀y ∈ C. x ≤ y ∨ y ≤ x"
lemma lfp_chain_induct:
assumes mono: "mono f"
and step: "⋀x. P x ⟹ P (f x)"
and chain: "⋀C. set_chain C ⟹ ∀ x ∈ C. P x ⟹ P (Sup C)"
shows "P (lfp f)"
unfolding lfp_eq_fixp[OF mono]
proof (rule fixp_induct)
show "monotone (≤) (≤) f" using mono unfolding order_class.mono_def monotone_def .
next
show "P (Sup {})" using chain[of "{}"] by simp
next
show "ccpo.admissible Sup (≤) P"
by (auto simp add: chain ccpo.admissible_def Complete_Partial_Order.chain_def)
qed fact
subsubsection ‹Preservation of transitivity, asymmetry, irreflexivity by suprema›
lemma trans_Sup_of_chain:
assumes "set_chain C" and trans: "⋀R. R ∈ C ⟹ trans R"
shows "trans (Sup C)"
proof (intro transI)
fix x y z
assume "(x,y) ∈ Sup C" and "(y,z) ∈ Sup C"
from ‹(x,y) ∈ Sup C› obtain R where "R ∈ C" and "(x,y) ∈ R" by blast
from ‹(y,z) ∈ Sup C› obtain S where "S ∈ C" and "(y,z) ∈ S" by blast
from ‹R ∈ C› and ‹S ∈ C› and ‹set_chain C› have "R ∪ S = R ∨ R ∪ S = S" by blast
with ‹R ∈ C› and ‹S ∈ C› have "R ∪ S ∈ C" by fastforce
with ‹(x,y) ∈ R› and ‹(y,z) ∈ S› and trans[of "R ∪ S"]
have "(x,z) ∈ R ∪ S" unfolding trans_def by blast
with ‹R ∪ S ∈ C› show "(x,z) ∈ ⋃C" by blast
qed
lemma asym_Sup_of_chain:
assumes "set_chain C" and asym: "⋀ R. R ∈ C ⟹ asym R"
shows "asym (Sup C)"
proof (intro asymI2 notI)
fix a b
assume "(a,b) ∈ Sup C" then obtain "R" where "R ∈ C" and "(a,b) ∈ R" by blast
assume "(b,a) ∈ Sup C" then obtain "S" where "S ∈ C" and "(b,a) ∈ S" by blast
from ‹R ∈ C› and ‹S ∈ C› and ‹set_chain C› have "R ∪ S = R ∨ R ∪ S = S" by blast
with ‹R ∈ C› and ‹S ∈ C› have "R ∪ S ∈ C" by fastforce
with ‹(a,b) ∈ R› and ‹(b,a) ∈ S› and asym show "False" unfolding asym.simps by blast
qed
lemma strict_order_lfp:
assumes "mono f" and "⋀R. strict_order R ⟹ strict_order (f R)"
shows "strict_order (lfp f)"
proof (intro lfp_chain_induct[of f strict_order])
fix C :: "('b × 'b) set set"
assume "set_chain C" and "∀R ∈ C. strict_order R"
from this show "strict_order (Sup C)" by (metis asym_Sup_of_chain trans_Sup_of_chain order_asym)
qed fact+
lemma trans_lfp:
assumes "mono f" and "⋀R. trans R ⟹ trans (f R)"
shows "trans (lfp f)"
by (metis lfp_chain_induct[of f trans] assms trans_Sup_of_chain)
end
subsection ‹Multiset extension›
lemma mulex_iff_mult: "mulex r M N ⟷ (M,N) ∈ mult {(M,N) . r M N}"
by (auto simp add: mulex_on_def restrict_to_def mult_def mulex1_def tranclp_unfold)
lemma multI:
assumes "trans r" "M = I + K" "N = I + J" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k,j) ∈ r"
shows "(M,N) ∈ mult r"
using assms one_step_implies_mult by blast
lemma multE:
assumes "trans r" and "(M,N) ∈ mult r"
obtains I J K where "M = I + K" "N = I + J" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k,j) ∈ r"
using mult_implies_one_step[OF assms] by blast
lemma mult_on_union: "(M,N) ∈ mult r ⟹ (K + M, K + N) ∈ mult r"
using mulex_on_union[of "λx y. (x,y) ∈ r" UNIV] by (auto simp: mulex_iff_mult)
lemma mult_on_union': "(M,N) ∈ mult r ⟹ (M + K, N + K) ∈ mult r"
using mulex_on_union'[of "λx y. (x,y) ∈ r" UNIV] by (auto simp: mulex_iff_mult)
lemma mult_on_add_mset: "(M,N) ∈ mult r ⟹ (add_mset k M, add_mset k N) ∈ mult r"
unfolding add_mset_add_single[of k M] add_mset_add_single[of k N] by (rule mult_on_union')
lemma mult_empty[simp]: "(M,{#}) ∉ mult R"
by (metis mult_def not_less_empty trancl.cases)
lemma mult_singleton[simp]: "(x, y) ∈ r ⟹ (add_mset x M, add_mset y M) ∈ mult r"
unfolding add_mset_add_single[of x M] add_mset_add_single[of y M]
apply (rule mult_on_union)
using mult1_singleton[of x y r] by (auto simp add: mult_def mult_on_union)
lemma empty_mult[simp]: "({#},N) ∈ mult R ⟷ N ≠ {#}"
using empty_mulex_on[of N UNIV "λM N. (M,N) ∈ R"] by (auto simp add: mulex_iff_mult)
lemma trans_mult: "trans (mult R)"
unfolding mult_def by simp
lemma strict_order_mult:
assumes "irrefl R" and "trans R"
shows "irrefl (mult R)" and "trans (mult R)"
proof -
show "irrefl (mult R)" unfolding irrefl_def
proof (intro allI notI, elim multE[OF ‹trans R›])
fix M I J K
assume "M = I + J" "M = I + K" "J ≠ {#}" and *: "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ R"
from ‹M = I + J› and ‹M = I + K› have "J = K" by simp
have "finite (set_mset J)" by simp
then have "set_mset J = {}" using * unfolding ‹J = K›
by (induct rule: finite_induct)
(simp, metis assms insert_absorb insert_iff insert_not_empty irrefl_def transD)
then show "False" using ‹J ≠ {#}› by simp
qed
qed (simp add: trans_mult)
lemma mult_of_image_mset:
assumes "trans R" and "trans R'"
and "⋀x y. x ∈ set_mset N ⟹ y ∈ set_mset M ⟹ (x,y) ∈ R ⟹ (f x, f y) ∈ R'"
and "(N, M) ∈ mult R"
shows "(image_mset f N, image_mset f M) ∈ mult R'"
proof (insert assms(4), elim multE[OF assms(1)])
fix I J K
assume "N = I + K" "M = I + J" "J ≠ {#}" "∀k ∈ set_mset K. ∃j ∈ set_mset J. (k, j) ∈ R"
thus "(image_mset f N, image_mset f M) ∈ mult R'" using assms(2,3)
by (intro multI) (auto, blast)
qed
subsection ‹Incrementality of @{term mult1} and @{term mult}›
lemma mono_mult1: "mono mult1"
unfolding mono_def mult1_def by blast
lemma mono_mult: "mono mult"
unfolding mono_def mult_def
proof (intro allI impI subsetI)
fix R S :: "'a rel" and x
assume "R ⊆ S" and "x ∈ (mult1 R)⇧+"
then show "x ∈ (mult1 S)⇧+"
using mono_mult1[unfolded mono_def] trancl_mono[of x "mult1 R" "mult1 S"] by auto
qed
subsection ‹Well-orders and well-quasi-orders›
lemma wf_iff_wfp_on:
"wf p ⟷ wfp_on (λa b. (a, b) ∈ p) UNIV"
unfolding wfp_on_iff_inductive_on wf_def inductive_on_def by force
lemma well_order_implies_wqo:
assumes "well_order r"
shows "wqo_on (λa b. (a, b) ∈ r) UNIV"
proof (intro wqo_onI almost_full_onI)
show "transp_on (λa b. (a, b) ∈ r) UNIV" using assms
by (auto simp only: well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def
trans_def transp_on_def)
next
fix f :: "nat ⇒ 'a"
show "good (λa b. (a, b) ∈ r) f"
using assms unfolding well_order_on_def wf_iff_wfp_on wfp_on_def not_ex not_all de_Morgan_conj
proof (elim conjE allE exE)
fix x assume "linear_order r" and "f x ∉ UNIV ∨ (f (Suc x), f x) ∉ r - Id"
then have "(f x, f (Suc x)) ∈ r" using ‹linear_order r›
by (force simp: linear_order_on_def Relation.total_on_def partial_order_on_def preorder_on_def
refl_on_def)
then show "good (λa b. (a, b) ∈ r) f" by (auto simp: good_def)
qed
qed
subsection ‹Splitting lists into prefix, element, and suffix›
fun list_splits :: "'a list ⇒ ('a list × 'a × 'a list) list" where
"list_splits [] = []"
| "list_splits (x # xs) = ([], x, xs) # map (λ(xs, x', xs'). (x # xs, x', xs')) (list_splits xs)"
lemma list_splits_empty[simp]:
"list_splits xs = [] ⟷ xs = []"
by (cases xs) simp_all
lemma elem_list_splits_append:
assumes "(ys, y, zs) ∈ set (list_splits xs)"
shows "ys @ [y] @ zs = xs"
using assms by (induct xs arbitrary: ys) auto
lemma elem_list_splits_length:
assumes "(ys, y, zs) ∈ set (list_splits xs)"
shows "length ys < length xs" and "length zs < length xs"
using elem_list_splits_append[OF assms] by auto
lemma elem_list_splits_elem:
assumes "(xs, y, ys) ∈ set (list_splits zs)"
shows "y ∈ set zs"
using elem_list_splits_append[OF assms] by force
lemma list_splits_append:
"list_splits (xs @ ys) = map (λ(xs', x', ys'). (xs', x', ys' @ ys)) (list_splits xs) @
map (λ(xs', x', ys'). (xs @ xs', x', ys')) (list_splits ys)"
by (induct xs) auto
lemma list_splits_rev:
"list_splits (rev xs) = map (λ(xs, x, ys). (rev ys, x, rev xs)) (rev (list_splits xs))"
by (induct xs) (auto simp add: list_splits_append comp_def prod.case_distrib rev_map)
lemma list_splits_map:
"list_splits (map f xs) = map (λ(xs, x, ys). (map f xs, f x, map f ys)) (list_splits xs)"
by (induct xs) auto
end