# Theory Infinite_Sequences

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Infinite Sequences›

text ‹Some useful constructions on and facts about infinite sequences.›

theory Infinite_Sequences
imports Main
begin

text ‹The set of all infinite sequences over elements from @{term A}.›
definition "SEQ A = {f::nat ⇒ 'a. ∀i. f i ∈ A}"

lemma SEQ_iff [iff]:
"f ∈ SEQ A ⟷ (∀i. f i ∈ A)"
by (auto simp: SEQ_def)

text ‹The ‹i›-th "column" of a set ‹B› of infinite sequences.›
definition "ith B i = {f i | f. f ∈ B}"

lemma ithI [intro]:
"f ∈ B ⟹ f i = x ⟹ x ∈ ith B i"
by (auto simp: ith_def)

lemma ithE [elim]:
"⟦x ∈ ith B i; ⋀f. ⟦f ∈ B; f i = x⟧ ⟹ Q⟧ ⟹ Q"
by (auto simp: ith_def)

lemma ith_conv:
"x ∈ ith B i ⟷ (∃f ∈ B. x = f i)"
by auto

text ‹
The restriction of a set ‹B› of sequences to sequences that are equal to a given sequence
‹f› up to position ‹i›.
›
definition eq_upto :: "(nat ⇒ 'a) set ⇒ (nat ⇒ 'a) ⇒ nat ⇒ (nat ⇒ 'a) set"
where
"eq_upto B f i = {g ∈ B. ∀j < i. f j = g j}"

lemma eq_uptoI [intro]:
"⟦g ∈ B; ⋀j. j < i ⟹ f j = g j⟧ ⟹ g ∈ eq_upto B f i"
by (auto simp: eq_upto_def)

lemma eq_uptoE [elim]:
"⟦g ∈ eq_upto B f i; ⟦g ∈ B; ⋀j. j < i ⟹ f j = g j⟧ ⟹ Q⟧ ⟹ Q"
by (auto simp: eq_upto_def)

lemma eq_upto_Suc:
"⟦g ∈ eq_upto B f i; g i = f i⟧ ⟹ g ∈ eq_upto B f (Suc i)"
by (auto simp: eq_upto_def less_Suc_eq)

lemma eq_upto_0 [simp]:
"eq_upto B f 0 = B"
by (auto simp: eq_upto_def)

lemma eq_upto_cong [fundef_cong]:
assumes "⋀j. j < i ⟹ f j = g j" and "B = C"
shows "eq_upto B f i = eq_upto C g i"
using assms by (auto simp: eq_upto_def)

subsection ‹Lexicographic Order on Infinite Sequences›

definition "LEX P f g ⟷ (∃i::nat. P (f i) (g i) ∧ (∀j<i. f j = g j))"
abbreviation "LEXEQ P ≡ (LEX P)⇧=⇧="

lemma LEX_imp_not_LEX:
assumes "LEX P f g"
and [dest]: "⋀x y z. P x y ⟹ P y z ⟹ P x z"
and [simp]: "⋀x. ¬ P x x"
shows "¬ LEX P g f"
proof -
{ fix i j :: nat
assume "P (f i) (g i)" and "∀k<i. f k = g k"
and "P (g j) (f j)" and "∀k<j. g k = f k"
then have False by (cases "i < j") (auto simp: not_less dest!: le_imp_less_or_eq) }
then show "¬ LEX P g f" using ‹LEX P f g› unfolding LEX_def by blast
qed

lemma LEX_cases:
assumes "LEX P f g"
obtains (eq) "f = g" | (neq) k where "∀i<k. f i = g i" and "P (f k) (g k)"
using assms by (auto simp: LEX_def)

lemma LEX_imp_less:
assumes "∀x∈A. ¬ P x x" and "f ∈ SEQ A ∨ g ∈ SEQ A"
and "LEX P f g" and "∀i<k. f i = g i" and "f k ≠ g k"
shows "P (f k) (g k)"
using assms by (auto elim!: LEX_cases) (metis linorder_neqE_nat)+

end


# Theory Minimal_Elements

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Minimal elements of sets w.r.t. a well-founded and transitive relation›

theory Minimal_Elements
imports
Infinite_Sequences
Open_Induction.Restricted_Predicates
begin

locale minimal_element =
fixes P A
assumes po: "po_on P A"
and wf: "wfp_on P A"
begin

definition "min_elt B = (SOME x. x ∈ B ∧ (∀y ∈ A. P y x ⟶ y ∉ B))"

lemma minimal:
assumes "x ∈ A" and "Q x"
shows "∃y ∈ A. P⇧=⇧= y x ∧ Q y ∧ (∀z ∈ A. P z y ⟶ ¬ Q z)"
using wf and assms
proof (induction rule: wfp_on_induct)
case (less x)
then show ?case
proof (cases "∀y ∈ A. P y x ⟶ ¬ Q y")
case True
with less show ?thesis by blast
next
case False
then obtain y where "y ∈ A" and "P y x" and "Q y" by blast
with less show ?thesis
using po [THEN po_on_imp_transp_on, unfolded transp_on_def, rule_format, of _ y x] by blast
qed
qed

lemma min_elt_ex:
assumes "B ⊆ A" and "B ≠ {}"
shows "∃x. x ∈ B ∧ (∀y ∈ A. P y x ⟶ y ∉ B)"
using assms using minimal [of _ "λx. x ∈ B"] by auto

lemma min_elt_mem:
assumes "B ⊆ A" and "B ≠ {}"
shows "min_elt B ∈ B"
using someI_ex [OF min_elt_ex [OF assms]] by (auto simp: min_elt_def)

lemma min_elt_minimal:
assumes *: "B ⊆ A" "B ≠ {}"
assumes "y ∈ A" and "P y (min_elt B)"
shows "y ∉ B"
using someI_ex [OF min_elt_ex [OF *]] and assms by (auto simp: min_elt_def)

text ‹A lexicographically minimal sequence w.r.t.\ a given set of sequences ‹C››
fun lexmin
where
lexmin: "lexmin C i = min_elt (ith (eq_upto C (lexmin C) i) i)"
declare lexmin [simp del]

lemma eq_upto_lexmin_non_empty:
assumes "C ⊆ SEQ A" and "C ≠ {}"
shows "eq_upto C (lexmin C) i ≠ {}"
proof (induct i)
case 0
show ?case using assms by auto
next
let ?A = "λi. ith (eq_upto C (lexmin C) i) i"
case (Suc i)
then have "?A i ≠ {}" by force
moreover have "eq_upto C (lexmin C) i ⊆ eq_upto C (lexmin C) 0" by auto
ultimately have "?A i ⊆ A" and "?A i ≠ {}" using assms by (auto simp: ith_def)
from min_elt_mem [OF this, folded lexmin]
obtain f where "f ∈ eq_upto C (lexmin C) (Suc i)" by (auto dest: eq_upto_Suc)
then show ?case by blast
qed

lemma lexmin_SEQ_mem:
assumes "C ⊆ SEQ A" and "C ≠ {}"
shows "lexmin C ∈ SEQ A"
proof -
{ fix i
let ?X = "ith (eq_upto C (lexmin C) i) i"
have "?X ⊆ A" using assms by (auto simp: ith_def)
moreover have "?X ≠ {}" using eq_upto_lexmin_non_empty [OF assms] by auto
ultimately have "lexmin C i ∈ A" using min_elt_mem [of ?X] by (subst lexmin) blast }
then show ?thesis by auto
qed

lemma non_empty_ith:
assumes "C ⊆ SEQ A" and "C ≠ {}"
shows "ith (eq_upto C (lexmin C) i) i ⊆ A"
and "ith (eq_upto C (lexmin C) i) i ≠ {}"
using eq_upto_lexmin_non_empty [OF assms, of i] and assms by (auto simp: ith_def)

lemma lexmin_minimal:
"C ⊆ SEQ A ⟹ C ≠ {} ⟹ y ∈ A ⟹ P y (lexmin C i) ⟹ y ∉ ith (eq_upto C (lexmin C) i) i"
using min_elt_minimal [OF non_empty_ith, folded lexmin] .

lemma lexmin_mem:
"C ⊆ SEQ A ⟹ C ≠ {} ⟹ lexmin C i ∈ ith (eq_upto C (lexmin C) i) i"
using min_elt_mem [OF non_empty_ith, folded lexmin] .

lemma LEX_chain_on_eq_upto_imp_ith_chain_on:
assumes "chain_on (LEX P) (eq_upto C f i) (SEQ A)"
shows "chain_on P (ith (eq_upto C f i) i) A"
using assms
proof -
{ fix x y assume "x ∈ ith (eq_upto C f i) i" and "y ∈ ith (eq_upto C f i) i"
and "¬ P x y" and "y ≠ x"
then obtain g h where *: "g ∈ eq_upto C f i" "h ∈ eq_upto C f i"
and [simp]: "x = g i" "y = h i" and eq: "∀j<i. g j = f j ∧ h j = f j"
by (auto simp: ith_def eq_upto_def)
with assms and ‹y ≠ x› consider "LEX P g h" | "LEX P h g" by (force simp: chain_on_def)
then have "P y x"
proof (cases)
assume "LEX P g h"
with eq and ‹y ≠ x› have "P x y" using assms and *
by (auto simp: LEX_def)
(metis SEQ_iff chain_on_imp_subset linorder_neqE_nat minimal subsetCE)
with ‹¬ P x y› show "P y x" ..
next
assume "LEX P h g"
with eq and ‹y ≠ x› show "P y x" using assms and *
by (auto simp: LEX_def)
(metis SEQ_iff chain_on_imp_subset linorder_neqE_nat minimal subsetCE)
qed }
then show ?thesis using assms by (auto simp: chain_on_def) blast
qed

end

end


# Theory Least_Enum

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Enumerations of Well-Ordered Sets in Increasing Order›

theory Least_Enum
imports Main
begin

locale infinitely_many1 =
fixes P :: "'a :: wellorder ⇒ bool"
assumes infm: "∀i. ∃j>i. P j"
begin

text ‹
Enumerate the elements of a well-ordered infinite set in increasing order.
›
fun enum :: "nat ⇒ 'a" where
"enum 0 = (LEAST n. P n)" |
"enum (Suc i) = (LEAST n. n > enum i ∧ P n)"

lemma enum_mono:
shows "enum i < enum (Suc i)"
using infm by (cases i, auto) (metis (lifting) LeastI)+

lemma enum_less:
"i < j ⟹ enum i < enum j"
using enum_mono by (metis lift_Suc_mono_less)

lemma enum_P:
shows "P (enum i)"
using infm by (cases i, auto) (metis (lifting) LeastI)+

end

locale infinitely_many2 =
fixes P :: "'a :: wellorder ⇒ 'a ⇒ bool"
and N :: "'a"
assumes infm: "∀i≥N. ∃j>i. P i j"
begin

text ‹
Enumerate the elements of a well-ordered infinite set that form a chain w.r.t.\ a given predicate
@{term P} starting from a given index @{term N} in increasing order.
›
fun enumchain :: "nat ⇒ 'a" where
"enumchain 0 = N" |
"enumchain (Suc n) = (LEAST m. m > enumchain n ∧ P (enumchain n) m)"

lemma enumchain_mono:
shows "N ≤ enumchain i ∧ enumchain i < enumchain (Suc i)"
proof (induct i)
case 0
have "enumchain 0 ≥ N" by simp
moreover then have "∃m>enumchain 0. P (enumchain 0) m" using infm by blast
ultimately show ?case by auto (metis (lifting) LeastI)
next
case (Suc i)
then have "N ≤ enumchain (Suc i)" by auto
moreover then have "∃m>enumchain (Suc i). P (enumchain (Suc i)) m" using infm by blast
ultimately show ?case by (auto) (metis (lifting) LeastI)
qed

lemma enumchain_chain:
shows "P (enumchain i) (enumchain (Suc i))"
proof (cases i)
case 0
moreover have "∃m>enumchain 0. P (enumchain 0) m" using infm by auto
ultimately show ?thesis by auto (metis (lifting) LeastI)
next
case (Suc i)
moreover have "enumchain (Suc i) > N" using enumchain_mono by (metis le_less_trans)
moreover then have "∃m>enumchain (Suc i). P (enumchain (Suc i)) m" using infm by auto
ultimately show ?thesis by (auto) (metis (lifting) LeastI)
qed

end

end



# Theory Almost_Full

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹The Almost-Full Property›

theory Almost_Full
imports
"HOL-Library.Sublist"
"HOL-Library.Ramsey"
"Regular-Sets.Regexp_Method"
"Abstract-Rewriting.Seq"
Least_Enum
Infinite_Sequences
Open_Induction.Restricted_Predicates
begin

(*TODO: move*)
lemma le_Suc_eq':
"x ≤ Suc y ⟷ x = 0 ∨ (∃x'. x = Suc x' ∧ x' ≤ y)"
by (cases x) auto

lemma ex_leq_Suc:
"(∃i≤Suc j. P i) ⟷ P 0 ∨ (∃i≤j. P (Suc i))"
by (auto simp: le_Suc_eq')

lemma ex_less_Suc:
"(∃i<Suc j. P i) ⟷ P 0 ∨ (∃i<j. P (Suc i))"
by (auto simp: less_Suc_eq_0_disj)

subsection ‹Basic Definitions and Facts›

text ‹
An infinite sequence is \emph{good} whenever there are indices @{term "i < j"} such that
@{term "P (f i) (f j)"}.
›
definition good :: "('a ⇒ 'a ⇒ bool) ⇒ (nat ⇒ 'a) ⇒ bool"
where
"good P f ⟷ (∃i j. i < j ∧ P (f i) (f j))"

text ‹A sequence that is not good is called \emph{bad}.›
abbreviation "bad P f ≡ ¬ good P f"

lemma goodI:
"⟦i < j; P (f i) (f j)⟧ ⟹ good P f"
by (auto simp: good_def)

lemma goodE [elim]:
"good P f ⟹ (⋀i j. ⟦i < j; P (f i) (f j)⟧ ⟹ Q) ⟹ Q"
by (auto simp: good_def)

"bad P f ⟹ ((⋀i j. i < j ⟹ ¬ P (f i) (f j)) ⟹ Q) ⟹ Q"
by (auto simp: good_def)

definition almost_full_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
"almost_full_on P A ⟷ (∀f ∈ SEQ A. good P f)"

lemma almost_full_onI [Pure.intro]:
"(⋀f. ∀i. f i ∈ A ⟹ good P f) ⟹ almost_full_on P A"
unfolding almost_full_on_def by blast

lemma almost_full_onD:
fixes f :: "nat ⇒ 'a" and A :: "'a set"
assumes "almost_full_on P A" and "⋀i. f i ∈ A"
obtains i j where "i < j" and "P (f i) (f j)"
using assms unfolding almost_full_on_def by blast

subsection ‹An equivalent inductive definition›

inductive af for A
where
now: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ P x y) ⟹ af A P"
| later: "(⋀x. x ∈ A ⟹ af A (λy z. P y z ∨ P x y)) ⟹ af A P"

lemma af_imp_almost_full_on:
assumes "af A P"
shows "almost_full_on P A"
proof
fix f :: "nat ⇒ 'a" assume "∀i. f i ∈ A"
with assms obtain i and j where "i < j" and "P (f i) (f j)"
proof (induct arbitrary: f thesis)
case (later P)
define g where [simp]: "g i = f (Suc i)" for i
have "f 0 ∈ A" and "∀i. g i ∈ A" using later by auto
then obtain i and j where "i < j" and "P (g i) (g j) ∨ P (f 0) (g i)" using later by blast
then consider "P (g i) (g j)" | "P (f 0) (g i)" by blast
then show ?case using ‹i < j› by (cases) (auto intro: later)
qed blast
then show "good P f" by (auto simp: good_def)
qed

lemma af_mono:
assumes "af A P"
and "∀x y. x ∈ A ∧ y ∈ A ∧ P x y ⟶ Q x y"
shows "af A Q"
using assms
proof (induct arbitrary: Q)
case (now P)
then have "⋀x y. x ∈ A ⟹ y ∈ A ⟹ Q x y" by blast
then show ?case by (rule af.now)
next
case (later P)
show ?case
proof (intro af.later [of A Q])
fix x assume "x ∈ A"
then show "af A (λy z. Q y z ∨ Q x y)"
using later(3) by (intro later(2) [of x]) auto
qed
qed

lemma accessible_on_imp_af:
assumes "accessible_on P A x"
shows "af A (λu v. ¬ P v u ∨ ¬ P u x)"
using assms
proof (induct)
case (1 x)
then have "af A (λu v. (¬ P v u ∨ ¬ P u x) ∨ ¬ P u y ∨ ¬ P y x)" if "y ∈ A" for y
using that by (cases "P y x") (auto intro: af.now af_mono)
then show ?case by (rule af.later)
qed

lemma wfp_on_imp_af:
assumes "wfp_on P A"
shows "af A (λx y. ¬ P y x)"
using assms by (auto simp: wfp_on_accessible_on_iff intro: accessible_on_imp_af af.later)

lemma af_leq:
"af UNIV ((≤) :: nat ⇒ nat ⇒ bool)"
using wf_less [folded wfP_def wfp_on_UNIV, THEN wfp_on_imp_af] by (simp add: not_less)

definition "NOTAF A P = (SOME x. x ∈ A ∧ ¬ af A (λy z. P y z ∨ P x y))"

lemma not_af:
"¬ af A P ⟹ (∃x y. x ∈ A ∧ y ∈ A ∧ ¬ P x y) ∧ (∃x∈A. ¬ af A (λy z. P y z ∨ P x y))"
unfolding af.simps [of A P] by blast

fun F
where
"F A P 0 = NOTAF A P"
| "F A P (Suc i) = (let x = NOTAF A P in F A (λy z. P y z ∨ P x y) i)"

lemma almost_full_on_imp_af:
assumes af: "almost_full_on P A"
shows "af A P"
proof (rule ccontr)
assume "¬ af A P"
then have *: "F A P n ∈ A ∧
¬ af A (λy z. P y z ∨ (∃i≤n. P (F A P i) y) ∨ (∃j≤n. ∃i. i < j ∧ P (F A P i) (F A P j)))" for n
proof (induct n arbitrary: P)
case 0
from ‹¬ af A P› have "∃x. x ∈ A ∧ ¬ af A (λy z. P y z ∨ P x y)" by (auto intro: af.intros)
then have "NOTAF A P ∈ A ∧ ¬ af A (λy z. P y z ∨ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex)
with 0 show ?case by simp
next
case (Suc n)
from ‹¬ af A P› have "∃x. x ∈ A ∧ ¬ af A (λy z. P y z ∨ P x y)" by (auto intro: af.intros)
then have "NOTAF A P ∈ A ∧ ¬ af A (λy z. P y z ∨ P (NOTAF A P) y)" unfolding NOTAF_def by (rule someI_ex)
from Suc(1) [OF this [THEN conjunct2]]
show ?case
by (fastforce simp: ex_leq_Suc ex_less_Suc elim!: back_subst [where P = "λx. ¬ af A x"])
qed
then have "F A P ∈ SEQ A" by auto
from af [unfolded almost_full_on_def, THEN bspec, OF this] and not_af [OF * [THEN conjunct2]]
show False unfolding good_def by blast
qed

hide_const NOTAF F

lemma almost_full_on_UNIV:
"almost_full_on (λ_ _. True) UNIV"
by (auto simp: almost_full_on_def good_def)

lemma almost_full_on_imp_reflp_on:
assumes "almost_full_on P A"
shows "reflp_on P A"
using assms by (auto simp: almost_full_on_def reflp_on_def)

lemma almost_full_on_subset:
"A ⊆ B ⟹ almost_full_on P B ⟹ almost_full_on P A"
by (auto simp: almost_full_on_def)

lemma almost_full_on_mono:
assumes "A ⊆ B" and "⋀x y. Q x y ⟹ P x y"
and "almost_full_on Q B"
shows "almost_full_on P A"
using assms by (metis almost_full_on_def almost_full_on_subset good_def)

text ‹
Every sequence over elements of an almost-full set has a homogeneous subsequence.
›
lemma almost_full_on_imp_homogeneous_subseq:
assumes "almost_full_on P A"
and "∀i::nat. f i ∈ A"
shows "∃φ::nat ⇒ nat. ∀i j. i < j ⟶ φ i < φ j ∧ P (f (φ i)) (f (φ j))"
proof -
define X where "X = {{i, j} | i j::nat. i < j ∧ P (f i) (f j)}"
define Y where "Y = - X"
define h where "h = (λZ. if Z ∈ X then 0 else Suc 0)"

have [iff]: "⋀x y. h {x, y} = 0 ⟷ {x, y} ∈ X" by (auto simp: h_def)
have [iff]: "⋀x y. h {x, y} = Suc 0 ⟷ {x, y} ∈ Y" by (auto simp: h_def Y_def)

have "∀x∈UNIV. ∀y∈UNIV. x ≠ y ⟶ h {x, y} < 2" by (simp add: h_def)
from Ramsey2 [OF infinite_UNIV_nat this] obtain I c
where "infinite I" and "c < 2"
and *: "∀x∈I. ∀y∈I. x ≠ y ⟶ h {x, y} = c" by blast
then interpret infinitely_many1 "λi. i ∈ I"

have "c = 0 ∨ c = 1" using ‹c < 2› by arith
then show ?thesis
proof
assume [simp]: "c = 0"
have "∀i j. i < j ⟶ P (f (enum i)) (f (enum j))"
proof (intro allI impI)
fix i j :: nat
assume "i < j"
from * and enum_P and enum_less [OF ‹i < j›] have "{enum i, enum j} ∈ X" by auto
with enum_less [OF ‹i < j›]
show "P (f (enum i)) (f (enum j))" by (auto simp: X_def doubleton_eq_iff)
qed
then show ?thesis using enum_less by blast
next
assume [simp]: "c = 1"
have "∀i j. i < j ⟶ ¬ P (f (enum i)) (f (enum j))"
proof (intro allI impI)
fix i j :: nat
assume "i < j"
from * and enum_P and enum_less [OF ‹i < j›] have "{enum i, enum j} ∈ Y" by auto
with enum_less [OF ‹i < j›]
show "¬ P (f (enum i)) (f (enum j))" by (auto simp: Y_def X_def doubleton_eq_iff)
qed
then have "¬ good P (f ∘ enum)" by auto
moreover have "∀i. f (enum i) ∈ A" using assms by auto
ultimately show ?thesis using ‹almost_full_on P A› by (simp add: almost_full_on_def)
qed
qed

text ‹
Almost full relations do not admit infinite antichains.
›
lemma almost_full_on_imp_no_antichain_on:
assumes "almost_full_on P A"
shows "¬ antichain_on P f A"
proof
assume *: "antichain_on P f A"
then have "∀i. f i ∈ A" by simp
with assms have "good P f" by (auto simp: almost_full_on_def)
then obtain i j where "i < j" and "P (f i) (f j)"
unfolding good_def by auto
moreover with * have "incomparable P (f i) (f j)" by auto
ultimately show False by blast
qed

text ‹
If the image of a function is almost-full then also its preimage is almost-full.
›
lemma almost_full_on_map:
assumes "almost_full_on Q B"
and "h  A ⊆ B"
shows "almost_full_on (λx y. Q (h x) (h y)) A" (is "almost_full_on ?P A")
proof
fix f
assume "∀i::nat. f i ∈ A"
then have "⋀i. h (f i) ∈ B" using ‹h  A ⊆ B› by auto
with ‹almost_full_on Q B› [unfolded almost_full_on_def, THEN bspec, of "h ∘ f"]
show "good ?P f" unfolding good_def comp_def by blast
qed

text ‹
The homomorphic image of an almost-full set is almost-full.
›
lemma almost_full_on_hom:
fixes h :: "'a ⇒ 'b"
assumes hom: "⋀x y. ⟦x ∈ A; y ∈ A; P x y⟧ ⟹ Q (h x) (h y)"
and af: "almost_full_on P A"
shows "almost_full_on Q (h  A)"
proof
fix f :: "nat ⇒ 'b"
assume "∀i. f i ∈ h  A"
then have "∀i. ∃x. x ∈ A ∧ f i = h x" by (auto simp: image_def)
from choice [OF this] obtain g
where *: "∀i. g i ∈ A ∧ f i = h (g i)" by blast
show "good Q f"
proof (rule ccontr)
{ fix i j :: nat
assume "i < j"
from bad have "¬ Q (f i) (f j)" using ‹i < j› by (auto simp: good_def)
with hom have "¬ P (g i) (g j)" using * by auto }
then have "bad P g" by (auto simp: good_def)
with af and * show False by (auto simp: good_def almost_full_on_def)
qed
qed

text ‹
The monomorphic preimage of an almost-full set is almost-full.
›
lemma almost_full_on_mon:
assumes mon: "⋀x y. ⟦x ∈ A; y ∈ A⟧ ⟹ P x y = Q (h x) (h y)" "bij_betw h A B"
and af: "almost_full_on Q B"
shows "almost_full_on P A"
proof
fix f :: "nat ⇒ 'a"
assume *: "∀i. f i ∈ A"
then have **: "∀i. (h ∘ f) i ∈ B" using mon by (auto simp: bij_betw_def)
show "good P f"
proof (rule ccontr)
{ fix i j :: nat
assume "i < j"
from bad have "¬ P (f i) (f j)" using ‹i < j› by (auto simp: good_def)
with mon have "¬ Q (h (f i)) (h (f j))"
using * by (auto simp: bij_betw_def inj_on_def) }
then have "bad Q (h ∘ f)" by (auto simp: good_def)
with af and ** show False by (auto simp: good_def almost_full_on_def)
qed
qed

text ‹
Every total and well-founded relation is almost-full.
›
lemma total_on_and_wfp_on_imp_almost_full_on:
assumes "total_on P A" and "wfp_on P A"
shows "almost_full_on P⇧=⇧= A"
proof (rule ccontr)
assume "¬ almost_full_on P⇧=⇧= A"
then obtain f :: "nat ⇒ 'a" where *: "⋀i. f i ∈ A"
and "∀i j. i < j ⟶ ¬ P⇧=⇧= (f i) (f j)"
unfolding almost_full_on_def by (auto dest: badE)
with ‹total_on P A› have "∀i j. i < j ⟶ P (f j) (f i)"
unfolding total_on_def by blast
then have "⋀i. P (f (Suc i)) (f i)" by auto
with ‹wfp_on P A› and * show False
unfolding wfp_on_def by blast
qed

lemma Nil_imp_good_list_emb [simp]:
assumes "f i = []"
shows "good (list_emb P) f"
proof (rule ccontr)
moreover have "(list_emb P) (f i) (f (Suc i))"
unfolding assms by auto
ultimately show False
unfolding good_def by auto
qed

lemma ne_lists:
assumes "xs ≠ []" and "xs ∈ lists A"
shows "hd xs ∈ A" and "tl xs ∈ lists A"
using assms by (case_tac [!] xs) simp_all

lemma list_emb_eq_length_induct [consumes 2, case_names Nil Cons]:
assumes "length xs = length ys"
and "list_emb P xs ys"
and "Q [] []"
and "⋀x y xs ys. ⟦P x y; list_emb P xs ys; Q xs ys⟧ ⟹ Q (x#xs) (y#ys)"
shows "Q xs ys"
using assms(2, 1, 3-) by (induct) (auto dest: list_emb_length)

lemma list_emb_eq_length_P:
assumes "length xs = length ys"
and "list_emb P xs ys"
shows "∀i<length xs. P (xs ! i) (ys ! i)"
using assms
proof (induct rule: list_emb_eq_length_induct)
case (Cons x y xs ys)
show ?case
proof (intro allI impI)
fix i assume "i < length (x # xs)"
with Cons show "P ((x#xs)!i) ((y#ys)!i)"
by (cases i) simp_all
qed
qed simp

subsection ‹Special Case: Finite Sets›

text ‹
Every reflexive relation on a finite set is almost-full.
›
lemma finite_almost_full_on:
assumes finite: "finite A"
and refl: "reflp_on P A"
shows "almost_full_on P A"
proof
fix f :: "nat ⇒ 'a"
assume *: "∀i. f i ∈ A"
let ?I = "UNIV::nat set"
have "f  ?I ⊆ A" using * by auto
with finite and finite_subset have 1: "finite (f  ?I)" by blast
have "infinite ?I" by auto
from pigeonhole_infinite [OF this 1]
obtain k where "infinite {j. f j = f k}" by auto
then obtain l where "k < l" and "f l = f k"
unfolding infinite_nat_iff_unbounded by auto
then have "P (f k) (f l)" using refl and * by (auto simp: reflp_on_def)
with ‹k < l› show "good P f" by (auto simp: good_def)
qed

lemma eq_almost_full_on_finite_set:
assumes "finite A"
shows "almost_full_on (=) A"
using finite_almost_full_on [OF assms, of "(=)"]
by (auto simp: reflp_on_def)

subsection ‹Further Results›

lemma af_trans_extension_imp_wf:
assumes subrel: "⋀x y. P x y ⟹ Q x y"
and af: "almost_full_on P A"
and trans: "transp_on Q A"
shows "wfp_on (strict Q) A"
proof (unfold wfp_on_def, rule notI)
assume "∃f. ∀i. f i ∈ A ∧ strict Q (f (Suc i)) (f i)"
then obtain f where *: "∀i. f i ∈ A ∧ ((strict Q)¯¯) (f i) (f (Suc i))" by blast
from chain_transp_on_less [OF this]
and transp_on_strict [THEN transp_on_converse, OF trans]
have "∀i j. i < j ⟶ ¬ Q (f i) (f j)" by blast
with subrel have "∀i j. i < j ⟶ ¬ P (f i) (f j)" by blast
with af show False
using * by (auto simp: almost_full_on_def good_def)
qed

lemma af_trans_imp_wf:
assumes "almost_full_on P A"
and "transp_on P A"
shows "wfp_on (strict P) A"
using assms by (intro af_trans_extension_imp_wf)

lemma wf_and_no_antichain_imp_qo_extension_wf:
assumes wf: "wfp_on (strict P) A"
and anti: "¬ (∃f. antichain_on P f A)"
and subrel: "∀x∈A. ∀y∈A. P x y ⟶ Q x y"
and qo: "qo_on Q A"
shows "wfp_on (strict Q) A"
proof (rule ccontr)
have "transp_on (strict Q) A"
using qo unfolding qo_on_def transp_on_def by blast
then have *: "transp_on ((strict Q)¯¯) A" by (rule transp_on_converse)
assume "¬ wfp_on (strict Q) A"
then obtain f :: "nat ⇒ 'a" where A: "⋀i. f i ∈ A"
and "∀i. strict Q (f (Suc i)) (f i)" unfolding wfp_on_def by blast+
then have "∀i. f i ∈ A ∧ ((strict Q)¯¯) (f i) (f (Suc i))" by auto
from chain_transp_on_less [OF this *]
have *: "⋀i j. i < j ⟹ ¬ P (f i) (f j)"
using subrel and A by blast
show False
proof (cases)
assume "∃k. ∀i>k. ∃j>i. P (f j) (f i)"
then obtain k where "∀i>k. ∃j>i. P (f j) (f i)" by auto
from subchain [of k _ f, OF this] obtain g
where "⋀i j. i < j ⟹ g i < g j"
and "⋀i. P (f (g (Suc i))) (f (g i))" by auto
with * have "⋀i. strict P (f (g (Suc i))) (f (g i))" by blast
with wf [unfolded wfp_on_def not_ex, THEN spec, of "λi. f (g i)"] and A
show False by fast
next
assume "¬ (∃k. ∀i>k. ∃j>i. P (f j) (f i))"
then have "∀k. ∃i>k. ∀j>i. ¬ P (f j) (f i)" by auto
from choice [OF this] obtain h
where "∀k. h k > k"
and **: "∀k. (∀j>h k. ¬ P (f j) (f (h k)))" by auto
define φ where [simp]: "φ = (λi. (h ^^ Suc i) 0)"
have "⋀i. φ i < φ (Suc i)"
using ‹∀k. h k > k› by (induct_tac i) auto
then have mono: "⋀i j. i < j ⟹ φ i < φ j" by (metis lift_Suc_mono_less)
then have "∀i j. i < j ⟶ ¬ P (f (φ j)) (f (φ i))"
using ** by auto
with mono [THEN *]
have "∀i j. i < j ⟶ incomparable P (f (φ j)) (f (φ i))" by blast
moreover have "∃i j. i < j ∧ ¬ incomparable P (f (φ i)) (f (φ j))"
using anti [unfolded not_ex, THEN spec, of "λi. f (φ i)"] and A by blast
ultimately show False by blast
qed
qed

lemma every_qo_extension_wf_imp_af:
assumes ext: "∀Q. (∀x∈A. ∀y∈A. P x y ⟶ Q x y) ∧
qo_on Q A ⟶ wfp_on (strict Q) A"
and "qo_on P A"
shows "almost_full_on P A"
proof
from ‹qo_on P A›
have refl: "reflp_on P A"
and trans: "transp_on P A"
by (auto intro: qo_on_imp_reflp_on qo_on_imp_transp_on)

fix f :: "nat ⇒ 'a"
assume "∀i. f i ∈ A"
then have A: "⋀i. f i ∈ A" ..
show "good P f"
proof (rule ccontr)
assume "¬ ?thesis"
then have bad: "∀i j. i < j ⟶ ¬ P (f i) (f j)" by (auto simp: good_def)
then have *: "⋀i j. P (f i) (f j) ⟹ i ≥ j" by (metis not_le_imp_less)

define D where [simp]: "D = (λx y. ∃i. x = f (Suc i) ∧ y = f i)"
define P' where "P' = restrict_to P A"
define Q where [simp]: "Q = (sup P' D)⇧*⇧*"

have **: "⋀i j. (D OO P'⇧*⇧*)⇧+⇧+ (f i) (f j) ⟹ i > j"
proof -
fix i j
assume "(D OO P'⇧*⇧*)⇧+⇧+ (f i) (f j)"
then show "i > j"
apply (induct "f i" "f j" arbitrary: j)
apply (insert A, auto dest!: * simp: P'_def reflp_on_restrict_to_rtranclp [OF refl trans])
apply (metis "*" dual_order.strict_trans1 less_Suc_eq_le refl reflp_on_def)
by (metis le_imp_less_Suc less_trans)
qed

have "∀x∈A. ∀y∈A. P x y ⟶ Q x y" by (auto simp: P'_def)
moreover have "qo_on Q A" by (auto simp: qo_on_def reflp_on_def transp_on_def)
ultimately have "wfp_on (strict Q) A"
using ext [THEN spec, of Q] by blast
moreover have "∀i. f i ∈ A ∧ strict Q (f (Suc i)) (f i)"
proof
fix i
have "¬ Q (f i) (f (Suc i))"
proof
assume "Q (f i) (f (Suc i))"
then have "(sup P' D)⇧*⇧* (f i) (f (Suc i))" by auto
moreover have "(sup P' D)⇧*⇧* = sup (P'⇧*⇧*) (P'⇧*⇧* OO (D OO P'⇧*⇧*)⇧+⇧+)"
proof -
have "⋀A B. (A ∪ B)⇧* = A⇧* ∪ A⇧* O (B O A⇧*)⇧+" by regexp
from this [to_pred] show ?thesis by blast
qed
ultimately have "sup (P'⇧*⇧*) (P'⇧*⇧* OO (D OO P'⇧*⇧*)⇧+⇧+) (f i) (f (Suc i))" by simp
then have "(P'⇧*⇧* OO (D OO P'⇧*⇧*)⇧+⇧+) (f i) (f (Suc i))" by auto
then have "Suc i < i"
using ** apply auto
by (metis (lifting, mono_tags) less_le relcompp.relcompI tranclp_into_tranclp2)
then show False by auto
qed
with A [of i] show "f i ∈ A ∧ strict Q (f (Suc i)) (f i)" by auto
qed
ultimately show False unfolding wfp_on_def by blast
qed
qed

end


(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

imports
Almost_Full
Minimal_Elements
begin

text ‹
A locale capturing the construction of minimal bad sequences over values from @{term "A"}. Where
minimality is to be understood w.r.t.\ @{term size} of an element.
›
locale mbs =
fixes A :: "('a :: size) set"
begin

text ‹
Since the @{term size} is a well-founded measure, whenever some element satisfies a property
@{term P}, then there is a size-minimal such element.
›
lemma minimal:
assumes "x ∈ A" and "P x"
shows "∃y ∈ A. size y ≤ size x ∧ P y ∧ (∀z ∈ A. size z < size y ⟶ ¬ P z)"
using assms
proof (induction x taking: size rule: measure_induct)
case (1 x)
then show ?case
proof (cases "∀y ∈ A. size y < size x ⟶ ¬ P y")
case True
with 1 show ?thesis by blast
next
case False
then obtain y where "y ∈ A" and "size y < size x" and "P y" by blast
with "1.IH" show ?thesis by (fastforce elim!: order_trans)
qed
qed

lemma less_not_eq [simp]:
"x ∈ A ⟹ size x < size y ⟹ x = y ⟹ False"
by simp

text ‹
The set of all bad sequences over @{term A}.
›

"f ∈ BAD P ⟷ (∀i. f i ∈ A) ∧ bad P f"

text ‹
A partial order on infinite bad sequences.
›
definition geseq :: "((nat ⇒ 'a) × (nat ⇒ 'a)) set"
where
"geseq =
{(f, g). f ∈ SEQ A ∧ g ∈ SEQ A ∧ (f = g ∨ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j)))}"

text ‹
The strict part of the above order.
›
definition gseq :: "((nat ⇒ 'a) × (nat ⇒ 'a)) set" where
"gseq = {(f, g). f ∈ SEQ A ∧ g ∈ SEQ A ∧ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j))}"

lemma geseq_iff:
"(f, g) ∈ geseq ⟷
f ∈ SEQ A ∧ g ∈ SEQ A ∧ (f = g ∨ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j)))"
by (auto simp: geseq_def)

lemma gseq_iff:
"(f, g) ∈ gseq ⟷ f ∈ SEQ A ∧ g ∈ SEQ A ∧ (∃i. size (g i) < size (f i) ∧ (∀j < i. f j = g j))"
by (auto simp: gseq_def)

lemma geseqE:
assumes "(f, g) ∈ geseq"
and "⟦∀i. f i ∈ A; ∀i. g i ∈ A; f = g⟧ ⟹ Q"
and "⋀i. ⟦∀i. f i ∈ A; ∀i. g i ∈ A; size (g i) < size (f i); ∀j < i. f j = g j⟧ ⟹ Q"
shows "Q"
using assms by (auto simp: geseq_iff)

lemma gseqE:
assumes "(f, g) ∈ gseq"
and "⋀i. ⟦∀i. f i ∈ A; ∀i. g i ∈ A; size (g i) < size (f i); ∀j < i. f j = g j⟧ ⟹ Q"
shows "Q"
using assms by (auto simp: gseq_iff)

sublocale min_elt_size?: minimal_element "measure_on size UNIV" A
rewrites "measure_on size UNIV ≡ λx y. size x < size y"
apply (unfold_locales)
apply (auto simp: po_on_def irreflp_on_def transp_on_def simp del: wfp_on_UNIV intro: wfp_on_subset)
apply (auto simp: measure_on_def inv_image_betw_def)
done

context
fixes P :: "'a ⇒ 'a ⇒ bool"
begin

text ‹
A lower bound to all sequences in a set of sequences @{term B}.
›
abbreviation "lb ≡ lexmin (BAD P)"

assumes "f ∈ eq_upto (BAD P) g i"
shows "f j ∈ A"
using assms by (auto)

text ‹
Assume that there is some infinite bad sequence @{term h}.
›
context
fixes h :: "nat ⇒ 'a"
begin

text ‹
When there is a bad sequence, then filtering @{term "BAD P"} w.r.t.~positions in @{term lb} never
yields an empty set of sequences.
›
"eq_upto (BAD P) lb i ≠ {}"

lemma non_empty_ith:
shows "ith (eq_upto (BAD P) lb i) i ⊆ A"
and "ith (eq_upto (BAD P) lb i) i ≠ {}"
using eq_upto_BAD_non_empty [of i] by auto

lemmas
lb_minimal = min_elt_minimal [OF non_empty_ith, folded lexmin] and
lb_mem = min_elt_mem [OF non_empty_ith, folded lexmin]

text ‹
@{term "lb"} is a infinite bad sequence.
›
proof -
have *: "⋀j. lb j ∈ ith (eq_upto (BAD P) lb j) j" by (rule lb_mem)
then have "∀i. lb i ∈ A" by (auto simp: ith_conv) (metis eq_upto_BAD_mem)
moreover
{ assume "good P lb"
then obtain i j where "i < j" and "P (lb i) (lb j)" by (auto simp: good_def)
from * have "lb j ∈ ith (eq_upto (BAD P) lb j) j" by (auto)
then obtain g where "g ∈ eq_upto (BAD P) lb j" and "g j = lb j" by force
then have "∀k ≤ j. g k = lb k" by (auto simp: order_le_less)
with ‹i < j› and ‹P (lb i) (lb j)› have "P (g i) (g j)" by auto
with ‹i < j› have "good P g" by (auto simp: good_def)
with ‹g ∈ eq_upto (BAD P) lb j› have False by auto }
ultimately show ?thesis by blast
qed

text ‹
There is no infinite bad sequence that is strictly smaller than @{term lb}.
›
lemma lb_lower_bound:
"∀g. (lb, g) ∈ gseq ⟶ g ∉ BAD P"
proof (intro allI impI)
fix g
assume "(lb, g) ∈ gseq"
then obtain i where "g i ∈ A" and "size (g i) < size (lb i)"
and "∀j < i. lb j = g j" by (auto simp: gseq_iff)
moreover with lb_minimal
have "g i ∉ ith (eq_upto (BAD P) lb i) i" by auto
ultimately show "g ∉ BAD P" by blast
qed

text ‹
If there is at least one bad sequence, then there is also a minimal one.
›
lemma lower_bound_ex:
"∃f ∈ BAD P. ∀g. (f, g) ∈ gseq ⟶ g ∉ BAD P"
using lb_BAD and lb_lower_bound by blast

lemma gseq_conv:
"(f, g) ∈ gseq ⟷ f ≠ g ∧ (f, g) ∈ geseq"
by (auto simp: gseq_def geseq_def dest: less_not_eq)

text ‹There is a minimal bad sequence.›
lemma mbs:
"∃f ∈ BAD P. ∀g. (f, g) ∈ gseq ⟶ good P g"
using lower_bound_ex by (auto simp: gseq_conv geseq_iff)

end

end

end

end


# Theory Higman_OI

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹A Proof of Higman's Lemma via Open Induction›

theory Higman_OI
imports
Open_Induction.Open_Induction
Minimal_Elements
Almost_Full
begin

subsection ‹Some facts about the suffix relation›

lemma wfp_on_strict_suffix:
"wfp_on strict_suffix A"
by (rule wfp_on_mono [OF subset_refl, of _ _ "measure_on length A"])
(auto simp: strict_suffix_def suffix_def)

lemma po_on_strict_suffix:
"po_on strict_suffix A"
by (force simp: strict_suffix_def po_on_def transp_on_def irreflp_on_def)

subsection ‹Lexicographic Order on Infinite Sequences›

lemma antisymp_on_LEX:
assumes "irreflp_on P A" and "antisymp_on P A"
shows "antisymp_on (LEX P) (SEQ A)"
proof
fix f g assume SEQ: "f ∈ SEQ A" "g ∈ SEQ A" and "LEX P f g" and "LEX P g f"
then obtain i j where "P (f i) (g i)" and "P (g j) (f j)"
and "∀k<i. f k = g k" and "∀k<j. g k = f k" by (auto simp: LEX_def)
then have "P (f (min i j)) (f (min i j))"
using assms(2) and SEQ by (cases "i = j") (auto simp: antisymp_on_def min_def, force)
with assms(1) and SEQ show  "f = g" by (auto simp: irreflp_on_def)
qed

lemma LEX_trans:
assumes "transp_on P A" and "f ∈ SEQ A" and "g ∈ SEQ A" and "h ∈ SEQ A"
and "LEX P f g" and "LEX P g h"
shows "LEX P f h"
using assms by (auto simp: LEX_def transp_on_def) (metis less_trans linorder_neqE_nat)

lemma qo_on_LEXEQ:
"transp_on P A ⟹ qo_on (LEXEQ P) (SEQ A)"
by (auto simp: qo_on_def reflp_on_def transp_on_def [of "LEXEQ P"] dest: LEX_trans)

context minimal_element
begin

lemma glb_LEX_lexmin:
assumes "chain_on (LEX P) C (SEQ A)" and "C ≠ {}"
shows "glb (LEX P) C (lexmin C)"
proof
have "C ⊆ SEQ A" using assms by (auto simp: chain_on_def)
then have "lexmin C ∈ SEQ A" using ‹C ≠ {}› by (intro lexmin_SEQ_mem)
note * = ‹C ⊆ SEQ A› ‹C ≠ {}›
note lex = LEX_imp_less [folded irreflp_on_def, OF po [THEN po_on_imp_irreflp_on]]
― ‹‹lexmin C› is a lower bound›
show "lb (LEX P) C (lexmin C)"
proof
fix f assume "f ∈ C"
then show "LEXEQ P (lexmin C) f"
proof (cases "f = lexmin C")
define i where "i = (LEAST i. f i ≠ lexmin C i)"
case False
then have neq: "∃i. f i ≠ lexmin C i" by blast
from LeastI_ex [OF this, folded i_def]
and not_less_Least [where P = "λi. f i ≠ lexmin C i", folded i_def]
have neq: "f i ≠ lexmin C i" and eq: "∀j<i. f j = lexmin C j" by auto
then have **: "f ∈ eq_upto C (lexmin C) i" "f i ∈ ith (eq_upto C (lexmin C) i) i"
using ‹f ∈ C› by force+
moreover from ** have "¬ P (f i) (lexmin C i)"
using lexmin_minimal [OF *, of "f i" i] and ‹f ∈ C› and ‹C ⊆ SEQ A› by blast
moreover obtain g where "g ∈ eq_upto C (lexmin C) (Suc i)"
using eq_upto_lexmin_non_empty [OF *] by blast
ultimately have "P (lexmin C i) (f i)"
using neq and ‹C ⊆ SEQ A› and assms(1) and lex [of g f i] and lex [of f g i]
by (auto simp: eq_upto_def chain_on_def)
with eq show ?thesis by (auto simp: LEX_def)
qed simp
qed

― ‹‹lexmin C› is greater than or equal to any other lower bound›
fix f assume lb: "lb (LEX P) C f"
then show "LEXEQ P f (lexmin C)"
proof (cases "f = lexmin C")
define i where "i = (LEAST i. f i ≠ lexmin C i)"
case False
then have neq: "∃i. f i ≠ lexmin C i" by blast
from LeastI_ex [OF this, folded i_def]
and not_less_Least [where P = "λi. f i ≠ lexmin C i", folded i_def]
have neq: "f i ≠ lexmin C i" and eq: "∀j<i. f j = lexmin C j" by auto
obtain h where "h ∈ eq_upto C (lexmin C) (Suc i)" and "h ∈ C"
using eq_upto_lexmin_non_empty [OF *] by (auto simp: eq_upto_def)
then have [simp]: "⋀j. j < Suc i ⟹ h j = lexmin C j" by auto
with lb and ‹h ∈ C› have "LEX P f h" using neq by (auto simp: lb_def)
then have "P (f i) (h i)"
using neq and eq and ‹C ⊆ SEQ A› and ‹h ∈ C› by (intro lex) auto
with eq show ?thesis by (auto simp: LEX_def)
qed simp
qed

lemma dc_on_LEXEQ:
"dc_on (LEXEQ P) (SEQ A)"
proof
fix C assume "chain_on (LEXEQ P) C (SEQ A)" and "C ≠ {}"
then have chain: "chain_on (LEX P) C (SEQ A)" by (auto simp: chain_on_def)
then have "C ⊆ SEQ A" by (auto simp: chain_on_def)
then have "lexmin C ∈ SEQ A" using ‹C ≠ {}› by (intro lexmin_SEQ_mem)
have "glb (LEX P) C (lexmin C)" by (rule glb_LEX_lexmin [OF chain ‹C ≠ {}›])
then have "glb (LEXEQ P) C (lexmin C)" by (auto simp: glb_def lb_def)
with ‹lexmin C ∈ SEQ A› show "∃f ∈ SEQ A. glb (LEXEQ P) C f" by blast
qed

end

text ‹
Properties that only depend on finite initial segments of a sequence
(i.e., which are open with respect to the product topology).
›
definition "pt_open_on Q A ⟷ (∀f∈A. Q f ⟷ (∃n. (∀g∈A. (∀i<n. g i = f i) ⟶ Q g)))"

lemma pt_open_onD:
"pt_open_on Q A ⟹ Q f ⟹ f ∈ A ⟹ (∃n. (∀g∈A. (∀i<n. g i = f i) ⟶ Q g))"
unfolding pt_open_on_def by blast

lemma pt_open_on_good:
"pt_open_on (good Q) (SEQ A)"
proof (unfold pt_open_on_def, intro ballI)
fix f assume f: "f ∈ SEQ A"
show "good Q f = (∃n. ∀g∈SEQ A. (∀i<n. g i = f i) ⟶ good Q g)"
proof
assume "good Q f"
then obtain i and j where *: "i < j" "Q (f i) (f j)" by auto
have "∀g∈SEQ A. (∀i<Suc j. g i = f i) ⟶ good Q g"
proof (intro ballI impI)
fix g assume "g ∈ SEQ A" and "∀i<Suc j. g i = f i"
then show "good Q g" using * by (force simp: good_def)
qed
then show "∃n. ∀g∈SEQ A. (∀i<n. g i = f i) ⟶ good Q g" ..
next
assume "∃n. ∀g∈SEQ A. (∀i<n. g i = f i) ⟶ good Q g"
with f show "good Q f" by blast
qed
qed

context minimal_element
begin

lemma pt_open_on_imp_open_on_LEXEQ:
assumes "pt_open_on Q (SEQ A)"
shows "open_on (LEXEQ P) Q (SEQ A)"
proof
fix C assume chain: "chain_on (LEXEQ P) C (SEQ A)" and ne: "C ≠ {}"
and "∃g∈SEQ A. glb (LEXEQ P) C g ∧ Q g"
then obtain g where g: "g ∈ SEQ A" and "glb (LEXEQ P) C g"
and Q: "Q g" by blast
then have glb: "glb (LEX P) C g" by (auto simp: glb_def lb_def)
from chain have "chain_on (LEX P) C (SEQ A)" and C: "C ⊆ SEQ A" by (auto simp: chain_on_def)
note * = glb_LEX_lexmin [OF this(1) ne]
have "lexmin C ∈ SEQ A" using ne and C by (intro lexmin_SEQ_mem)
from glb_unique [OF _ g this glb *]
and antisymp_on_LEX [OF po_on_imp_irreflp_on [OF po] po_on_imp_antisymp_on [OF po]]
have [simp]: "lexmin C = g" by auto
from assms [THEN pt_open_onD, OF Q g]
obtain n :: nat where **: "⋀h. h ∈ SEQ A ⟹ (∀i<n. h i = g i) ⟶ Q h" by blast
from eq_upto_lexmin_non_empty [OF C ne, of n]
obtain f where "f ∈ eq_upto C g n" by auto
then have "f ∈ C" and "Q f" using ** [of f] and C by force+
then show "∃f∈C. Q f" by blast
qed

lemma open_on_good:
"open_on (LEXEQ P) (good Q) (SEQ A)"
by (intro pt_open_on_imp_open_on_LEXEQ pt_open_on_good)

end

lemma open_on_LEXEQ_imp_pt_open_on_counterexample:
fixes a b :: "'a"
defines "A ≡ {a, b}" and "P ≡ (λx y. False)" and "Q ≡ (λf. ∀i. f i = b)"
assumes [simp]: "a ≠ b"
shows "minimal_element P A" and "open_on (LEXEQ P) Q (SEQ A)"
and "¬ pt_open_on Q (SEQ A)"
proof -
show "minimal_element P A"
by standard (auto simp: P_def po_on_def irreflp_on_def transp_on_def wfp_on_def)
show "open_on (LEXEQ P) Q (SEQ A)"
by (auto simp: P_def open_on_def chain_on_def SEQ_def glb_def lb_def LEX_def)
show "¬ pt_open_on Q (SEQ A)"
proof
define f :: "nat ⇒ 'a" where "f ≡ (λx. b)"
have "f ∈ SEQ A" by (auto simp: A_def f_def)
moreover assume "pt_open_on Q (SEQ A)"
ultimately have "Q f ⟷ (∃n. (∀g∈SEQ A. (∀i<n. g i = f i) ⟶ Q g))"
unfolding pt_open_on_def by blast
moreover have "Q f" by (auto simp: Q_def f_def)
moreover have "∃g∈SEQ A. (∀i<n. g i = f i) ∧ ¬ Q g" for n
by (intro bexI [of _ "f(n := a)"]) (auto simp: f_def Q_def A_def)
ultimately show False by blast
qed
qed

lemma higman:
assumes "almost_full_on P A"
shows "almost_full_on (list_emb P) (lists A)"
proof
interpret minimal_element strict_suffix "lists A"
by (unfold_locales) (intro po_on_strict_suffix wfp_on_strict_suffix)+
fix f presume "f ∈ SEQ (lists A)"
with qo_on_LEXEQ [OF po_on_imp_transp_on [OF po_on_strict_suffix]] and dc_on_LEXEQ and open_on_good
show "good (list_emb P) f"
proof (induct rule: open_induct_on)
case (less f)
define h where "h i = hd (f i)" for i
show ?case
proof (cases "∃i. f i = []")
case False
then have ne: "∀i. f i ≠ []" by auto
with ‹f ∈ SEQ (lists A)› have "∀i. h i ∈ A" by (auto simp: h_def ne_lists)
from almost_full_on_imp_homogeneous_subseq [OF assms this]
obtain φ :: "nat ⇒ nat" where mono: "⋀i j. i < j ⟹ φ i < φ j"
and P: "⋀i j. i < j ⟹ P (h (φ i)) (h (φ j))" by blast
define f' where "f' i = (if i < φ 0 then f i else tl (f (φ (i - φ 0))))" for i
have f': "f' ∈ SEQ (lists A)" using ne and ‹f ∈ SEQ (lists A)›
by (auto simp: f'_def dest: list.set_sel)
have [simp]: "⋀i. φ 0 ≤ i ⟹ h (φ (i - φ 0)) # f' i = f (φ (i - φ 0))"
"⋀i. i < φ 0 ⟹ f' i = f i" using ne by (auto simp: f'_def h_def)
moreover have "strict_suffix (f' (φ 0)) (f (φ 0))" using ne by (auto simp: f'_def)
ultimately have "LEX strict_suffix f' f" by (auto simp: LEX_def)
with LEX_imp_not_LEX [OF this] have "strict (LEXEQ strict_suffix) f' f"
using po_on_strict_suffix [of UNIV] unfolding po_on_def irreflp_on_def transp_on_def by blast
from less(2) [OF f' this] have "good (list_emb P) f'" .
then obtain i j where "i < j" and emb: "list_emb P (f' i) (f' j)" by (auto simp: good_def)
consider "j < φ 0" | "φ 0 ≤ i" | "i < φ 0" and "φ 0 ≤ j" by arith
then show ?thesis
proof (cases)
case 1 with ‹i < j› and emb show ?thesis by (auto simp: good_def)
next
case 2
with ‹i < j› and P have "P (h (φ (i - φ 0))) (h (φ (j - φ 0)))" by auto
with emb have "list_emb P (h (φ (i - φ 0)) # f' i) (h (φ (j - φ 0)) # f' j)" by auto
then have "list_emb P (f (φ (i - φ 0))) (f (φ (j - φ 0)))" using 2 and ‹i < j› by auto
moreover with 2 and ‹i <j› have "φ (i - φ 0) < φ (j - φ 0)" using mono by auto
ultimately show ?thesis by (auto simp: good_def)
next
case 3
with emb have "list_emb P (f i) (f' j)" by auto
moreover have "f (φ (j - φ 0)) = h (φ (j - φ 0)) # f' j" using 3 by auto
ultimately have "list_emb P (f i) (f (φ (j - φ 0)))" by auto
moreover have "i < φ (j - φ 0)" using mono [of 0 "j - φ 0"] and 3 by force
ultimately show ?thesis by (auto simp: good_def)
qed
qed auto
qed
qed blast

end


# Theory Almost_Full_Relations

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Almost-Full Relations›

theory Almost_Full_Relations
begin

lemma (in mbs) mbs':
assumes "¬ almost_full_on P A"
shows "∃m ∈ BAD P. ∀g. (m, g) ∈ gseq ⟶ good P g"
using assms and mbs unfolding almost_full_on_def by blast

(*TODO: move to Option.thy of Isabelle/HOL?*)
subsection ‹Adding a Bottom Element to a Set›

definition with_bot :: "'a set ⇒ 'a option set" ("_⇩⊥"  1000)
where
"A⇩⊥ = {None} ∪ Some  A"

lemma with_bot_iff [iff]:
"Some x ∈ A⇩⊥ ⟷ x ∈ A"
by (auto simp: with_bot_def)

lemma NoneI [simp, intro]:
"None ∈ A⇩⊥"

lemma not_None_the_mem [simp]:
"x ≠ None ⟹ the x ∈ A ⟷ x ∈ A⇩⊥"
by auto

lemma with_bot_cases:
"u ∈ A⇩⊥ ⟹ (⋀x. x ∈ A ⟹ u = Some x ⟹ P) ⟹ (u = None ⟹ P) ⟹ P"
by auto

lemma with_bot_empty_conv [iff]:
"A⇩⊥ = {None} ⟷ A = {}"
by (auto elim: with_bot_cases)

lemma with_bot_UNIV [simp]:
"UNIV⇩⊥ = UNIV"
proof (rule set_eqI)
fix x :: "'a option"
show "x ∈ UNIV⇩⊥ ⟷ x ∈ UNIV" by (cases x) auto
qed

subsection ‹Adding a Bottom Element to an Almost-Full Set›

fun
option_le :: "('a ⇒ 'a ⇒ bool) ⇒ 'a option ⇒ 'a option ⇒ bool"
where
"option_le P None y = True" |
"option_le P (Some x) None = False" |
"option_le P (Some x) (Some y) = P x y"

lemma None_imp_good_option_le [simp]:
assumes "f i = None"
shows "good (option_le P) f"
by (rule goodI [of i "Suc i"]) (auto simp: assms)

lemma almost_full_on_with_bot:
assumes "almost_full_on P A"
shows "almost_full_on (option_le P) A⇩⊥" (is "almost_full_on ?P ?A")
proof
fix f :: "nat ⇒ 'a option"
assume *: "∀i. f i ∈ ?A"
show "good ?P f"
proof (cases "∀i. f i ≠ None")
case True
then have **: "⋀i. Some (the (f i)) = f i"
and "⋀i. the (f i) ∈ A" using * by auto
with almost_full_onD [OF assms, of "the ∘ f"] obtain i j where "i < j"
and "P (the (f i)) (the (f j))" by auto
then have "?P (Some (the (f i))) (Some (the (f j)))" by simp
then have "?P (f i) (f j)" unfolding ** .
with ‹i < j› show "good ?P f" by (auto simp: good_def)
qed auto
qed

subsection ‹Disjoint Union of Almost-Full Sets›

fun
sum_le :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'a + 'b ⇒ 'a + 'b ⇒ bool"
where
"sum_le P Q (Inl x) (Inl y) = P x y" |
"sum_le P Q (Inr x) (Inr y) = Q x y" |
"sum_le P Q x y = False"

lemma not_sum_le_cases:
assumes "¬ sum_le P Q a b"
and "⋀x y. ⟦a = Inl x; b = Inl y; ¬ P x y⟧ ⟹ thesis"
and "⋀x y. ⟦a = Inr x; b = Inr y; ¬ Q x y⟧ ⟹ thesis"
and "⋀x y. ⟦a = Inl x; b = Inr y⟧ ⟹ thesis"
and "⋀x y. ⟦a = Inr x; b = Inl y⟧ ⟹ thesis"
shows thesis
using assms by (cases a b rule: sum.exhaust [case_product sum.exhaust]) auto

text ‹
When two sets are almost-full, then their disjoint sum is almost-full.
›
lemma almost_full_on_Plus:
assumes "almost_full_on P A" and "almost_full_on Q B"
shows "almost_full_on (sum_le P Q) (A <+> B)" (is "almost_full_on ?P ?A")
proof
fix f :: "nat ⇒ ('a + 'b)"
let ?I = "f - Inl  A"
let ?J = "f - Inr  B"
assume "∀i. f i ∈ ?A"
then have *: "?J = (UNIV::nat set) - ?I" by (fastforce)
show "good ?P f"
proof (rule ccontr)
show False
proof (cases "finite ?I")
assume "finite ?I"
then have "infinite ?J" by (auto simp: *)
then interpret infinitely_many1 "λi. f i ∈ Inr  B"
have [dest]: "⋀i x. f (enum i) = Inl x ⟹ False"
using enum_P by (auto simp: image_iff) (metis Inr_Inl_False)
let ?f = "λi. projr (f (enum i))"
have B: "⋀i. ?f i ∈ B" using enum_P by (auto simp: image_iff) (metis sum.sel(2))
{ fix i j :: nat
assume "i < j"
then have "enum i < enum j" using enum_less by auto
with bad have "¬ ?P (f (enum i)) (f (enum j))" by (auto simp: good_def)
then have "¬ Q (?f i) (?f j)" by (auto elim: not_sum_le_cases) }
then have "bad Q ?f" by (auto simp: good_def)
moreover from ‹almost_full_on Q B› and B
have "good Q ?f" by (auto simp: good_def almost_full_on_def)
ultimately show False by blast
next
assume "infinite ?I"
then interpret infinitely_many1 "λi. f i ∈ Inl  A"
have [dest]: "⋀i x. f (enum i) = Inr x ⟹ False"
using enum_P by (auto simp: image_iff) (metis Inr_Inl_False)
let ?f = "λi. projl (f (enum i))"
have A: "∀i. ?f i ∈ A" using enum_P by (auto simp: image_iff) (metis sum.sel(1))
{ fix i j :: nat
assume "i < j"
then have "enum i < enum j" using enum_less by auto
with bad have "¬ ?P (f (enum i)) (f (enum j))" by (auto simp: good_def)
then have "¬ P (?f i) (?f j)" by (auto elim: not_sum_le_cases) }
then have "bad P ?f" by (auto simp: good_def)
moreover from ‹almost_full_on P A› and A
have "good P ?f" by (auto simp: good_def almost_full_on_def)
ultimately show False by blast
qed
qed
qed

subsection ‹Dickson's Lemma for Almost-Full Relations›

text ‹
When two sets are almost-full, then their Cartesian product is almost-full.
›

definition
prod_le :: "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'a × 'b ⇒ 'a × 'b ⇒ bool"
where
"prod_le P1 P2 = (λ(p1, p2) (q1, q2). P1 p1 q1 ∧ P2 p2 q2)"

lemma prod_le_True [simp]:
"prod_le P (λ_ _. True) a b = P (fst a) (fst b)"
by (auto simp: prod_le_def)

lemma almost_full_on_Sigma:
assumes "almost_full_on P1 A1" and "almost_full_on P2 A2"
shows "almost_full_on (prod_le P1 P2) (A1 × A2)" (is "almost_full_on ?P ?A")
proof (rule ccontr)
assume "¬ almost_full_on ?P ?A"
then obtain f where f: "∀i. f i ∈ ?A"
let ?W = "λx y. P1 (fst x) (fst y)"
let ?B = "λx y. P2 (snd x) (snd y)"
from f have fst: "∀i. fst (f i) ∈ A1" and snd: "∀i. snd (f i) ∈ A2"
by (metis SigmaE fst_conv, metis SigmaE snd_conv)
from almost_full_on_imp_homogeneous_subseq [OF assms(1) fst]
obtain φ :: "nat ⇒ nat" where mono: "⋀i j. i < j ⟹ φ i < φ j"
and *: "⋀i j. i < j ⟹ ?W (f (φ i)) (f (φ j))" by auto
from snd have "∀i. snd (f (φ i)) ∈ A2" by auto
then have "snd ∘ f ∘ φ ∈ SEQ A2" by auto
with assms(2) have "good P2 (snd ∘ f ∘ φ)" by (auto simp: almost_full_on_def)
then obtain i j :: nat
where "i < j" and "?B (f (φ i)) (f (φ j))" by auto
with * [OF ‹i < j›] have "?P (f (φ i)) (f (φ j))" by (simp add: case_prod_beta prod_le_def)
with mono [OF ‹i < j›] and bad show False by auto
qed

subsection ‹Higman's Lemma for Almost-Full Relations›

lemma almost_full_on_lists:
assumes "almost_full_on P A"
shows "almost_full_on (list_emb P) (lists A)" (is "almost_full_on ?P ?A")
proof (rule ccontr)
interpret mbs ?A .
assume "¬ ?thesis"
from mbs' [OF this] obtain m
and min: "∀g. (m, g) ∈ gseq ⟶ good ?P g" ..
then have lists: "⋀i. m i ∈ lists A"
and ne: "⋀i. m i ≠ []" by auto

define h t where "h = (λi. hd (m i))" and "t = (λi. tl (m i))"
have m: "⋀i. m i = h i # t i" using ne by (simp add: h_def t_def)

have "∀i. h i ∈ A" using ne_lists [OF ne] and lists by (auto simp add: h_def)
from almost_full_on_imp_homogeneous_subseq [OF assms this] obtain φ :: "nat ⇒ nat"
where less: "⋀i j. i < j ⟹ φ i < φ j"
and P: "∀i j. i < j ⟶ P (h (φ i)) (h (φ j))" by blast

proof
assume "good ?P (t ∘ φ)"
then obtain i j where "i < j" and "?P (t (φ i)) (t (φ j))" by auto
moreover with P have "P (h (φ i)) (h (φ j))" by blast
ultimately have "?P (m (φ i)) (m (φ j))"
by (subst (1 2) m) (rule list_emb_Cons2, auto)
with less and ‹i < j› have "good ?P m" by (auto simp: good_def)
with bad show False by blast
qed

define m' where "m' = (λi. if i < φ 0 then m i else t (φ (i - φ 0)))"

have m'_less: "⋀i. i < φ 0 ⟹ m' i = m i" by (simp add: m'_def)
have m'_geq: "⋀i. i ≥ φ 0 ⟹ m' i = t (φ (i - φ 0))" by (simp add: m'_def)

have "∀i. m' i ∈ lists A" using ne_lists [OF ne] and lists by (auto simp: m'_def t_def)
moreover have "length (m' (φ 0)) < length (m (φ 0))" using ne by (simp add: t_def m'_geq)
moreover have "∀j<φ 0. m' j = m j" by (auto simp: m'_less)
ultimately have "(m, m') ∈ gseq" using lists by (auto simp: gseq_def)
proof
assume "good ?P m'"
then obtain i j where "i < j" and emb: "?P (m' i) (m' j)" by (auto simp: good_def)
{ assume "j < φ 0"
with ‹i < j› and emb have "?P (m i) (m j)" by (auto simp: m'_less)
with ‹i < j› and bad have False by blast }
moreover
{ assume "φ 0 ≤ i"
with ‹i < j› and emb have "?P (t (φ (i - φ 0))) (t (φ (j - φ 0)))"
and "i - φ 0 < j - φ 0" by (auto simp: m'_geq)
with bad_t have False by auto }
moreover
{ assume "i < φ 0" and "φ 0 ≤ j"
with ‹i < j› and emb have "?P (m i) (t (φ (j - φ 0)))" by (simp add: m'_less m'_geq)
from list_emb_Cons [OF this, of "h (φ (j - φ 0))"]
have "?P (m i) (m (φ (j - φ 0)))" using ne by (simp add: h_def t_def)
moreover have "i < φ (j - φ 0)"
using less [of 0 "j - φ 0"] and ‹i < φ 0› and ‹φ 0 ≤ j›
by (cases "j = φ 0") auto
ultimately have False using bad by blast }
ultimately show False using ‹i < j› by arith
qed
ultimately show False using min by blast
qed

subsection ‹Natural Numbers›

lemma almost_full_on_UNIV_nat:
"almost_full_on (≤) (UNIV :: nat set)"
proof -
let ?P = "subseq :: bool list ⇒ bool list ⇒ bool"
have *: "length  (UNIV :: bool list set) = (UNIV :: nat set)"
by (metis Ex_list_of_length surj_def)
have "almost_full_on (≤) (length  (UNIV :: bool list set))"
proof (rule almost_full_on_hom)
fix xs ys :: "bool list"
assume "?P xs ys"
then show "length xs ≤ length ys"
by (metis list_emb_length)
next
have "finite (UNIV :: bool set)" by auto
from almost_full_on_lists [OF eq_almost_full_on_finite_set [OF this]]
show "almost_full_on ?P UNIV" unfolding lists_UNIV .
qed
then show ?thesis unfolding * .
qed

end


# Theory Well_Quasi_Orders

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Well-Quasi-Orders›

theory Well_Quasi_Orders
imports Almost_Full_Relations
begin

subsection ‹Basic Definitions›

definition wqo_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"wqo_on P A ⟷ transp_on P A ∧ almost_full_on P A"

lemma wqo_on_UNIV:
"wqo_on (λ_ _. True) UNIV"
using almost_full_on_UNIV by (auto simp: wqo_on_def transp_on_def)

lemma wqo_onI [Pure.intro]:
"⟦transp_on P A; almost_full_on P A⟧ ⟹ wqo_on P A"
unfolding wqo_on_def almost_full_on_def by blast

lemma wqo_on_imp_reflp_on:
"wqo_on P A ⟹ reflp_on P A"
using almost_full_on_imp_reflp_on by (auto simp: wqo_on_def)

lemma wqo_on_imp_transp_on:
"wqo_on P A ⟹ transp_on P A"
by (auto simp: wqo_on_def)

lemma wqo_on_imp_almost_full_on:
"wqo_on P A ⟹ almost_full_on P A"
by (auto simp: wqo_on_def)

lemma wqo_on_imp_qo_on:
"wqo_on P A ⟹ qo_on P A"
by (metis qo_on_def wqo_on_imp_reflp_on wqo_on_imp_transp_on)

lemma wqo_on_imp_good:
"wqo_on P A ⟹ ∀i. f i ∈ A ⟹ good P f"
by (auto simp: wqo_on_def almost_full_on_def)

lemma wqo_on_subset:
"A ⊆ B ⟹ wqo_on P B ⟹ wqo_on P A"
using almost_full_on_subset [of A B P]
and transp_on_subset [of A B P]
unfolding wqo_on_def by blast

subsection ‹Equivalent Definitions›

text ‹
Given a quasi-order @{term P}, the following statements are equivalent:
\begin{enumerate}
\item @{term P} is a almost-full.
\item @{term P} does neither allow decreasing chains nor antichains.
\item Every quasi-order extending @{term P} is well-founded.
\end{enumerate}
›

lemma wqo_af_conv:
assumes "qo_on P A"
shows "wqo_on P A ⟷ almost_full_on P A"
using assms by (metis qo_on_def wqo_on_def)

lemma wqo_wf_and_no_antichain_conv:
assumes "qo_on P A"
shows "wqo_on P A ⟷ wfp_on (strict P) A ∧ ¬ (∃f. antichain_on P f A)"
unfolding wqo_af_conv [OF assms]
using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]]
and almost_full_on_imp_no_antichain_on [of P A]
and wf_and_no_antichain_imp_qo_extension_wf [of P A]
and every_qo_extension_wf_imp_af [OF _ assms]
by blast

lemma wqo_extensions_wf_conv:
assumes "qo_on P A"
shows "wqo_on P A ⟷ (∀Q. (∀x∈A. ∀y∈A. P x y ⟶ Q x y) ∧ qo_on Q A ⟶ wfp_on (strict Q) A)"
unfolding wqo_af_conv [OF assms]
using af_trans_imp_wf [OF _ assms [THEN qo_on_imp_transp_on]]
and almost_full_on_imp_no_antichain_on [of P A]
and wf_and_no_antichain_imp_qo_extension_wf [of P A]
and every_qo_extension_wf_imp_af [OF _ assms]
by blast

lemma wqo_on_imp_wfp_on:
"wqo_on P A ⟹ wfp_on (strict P) A"
by (metis (no_types) wqo_on_imp_qo_on wqo_wf_and_no_antichain_conv)

text ‹
The homomorphic image of a wqo set is wqo.
›
lemma wqo_on_hom:
assumes "transp_on Q (h  A)"
and "∀x∈A. ∀y∈A. P x y ⟶ Q (h x) (h y)"
and "wqo_on P A"
shows "wqo_on Q (h  A)"
using assms and almost_full_on_hom [of A P Q h]
unfolding wqo_on_def by blast

text ‹
The monomorphic preimage of a wqo set is wqo.
›
lemma wqo_on_mon:
assumes *: "∀x∈A. ∀y∈A. P x y ⟷ Q (h x) (h y)"
and bij: "bij_betw h A B"
and wqo: "wqo_on Q B"
shows "wqo_on P A"
proof -
have "transp_on P A"
proof
fix x y z assume [intro!]: "x ∈ A" "y ∈ A" "z ∈ A"
and "P x y" and "P y z"
with * have "Q (h x) (h y)" and "Q (h y) (h z)" by blast+
with wqo_on_imp_transp_on [OF wqo] have "Q (h x) (h z)"
using bij by (auto simp: bij_betw_def transp_on_def)
with * show "P x z" by blast
qed
with assms and almost_full_on_mon [of A P Q h]
show ?thesis unfolding wqo_on_def by blast
qed

subsection ‹A Type Class for Well-Quasi-Orders›

text ‹
In a well-quasi-order (wqo) every infinite sequence is good.
›
class wqo = preorder +
assumes good: "good (≤) f"

lemma wqo_on_class [simp, intro]:
"wqo_on (≤) (UNIV :: ('a :: wqo) set)"
using good by (auto simp: wqo_on_def transp_on_def almost_full_on_def dest: order_trans)

lemma wqo_on_UNIV_class_wqo [intro!]:
"wqo_on P UNIV ⟹ class.wqo P (strict P)"
by (unfold_locales) (auto simp: wqo_on_def almost_full_on_def, unfold transp_on_def, blast)

text ‹
The following lemma converts between @{const wqo_on} (for the special case that the domain is the
universe of a type) and the class predicate @{const class.wqo}.
›
lemma wqo_on_UNIV_conv:
"wqo_on P UNIV ⟷ class.wqo P (strict P)" (is "?lhs = ?rhs")
proof
assume "?lhs" then show "?rhs" by auto
next
assume "?rhs" then show "?lhs"
unfolding class.wqo_def class.preorder_def class.wqo_axioms_def
by (auto simp: wqo_on_def almost_full_on_def transp_on_def)
qed

text ‹
The strict part of a wqo is well-founded.
›
lemma (in wqo) "wfP (<)"
proof -
have "class.wqo (≤) (<)" ..
hence "wqo_on (≤) UNIV"
unfolding less_le_not_le [abs_def] wqo_on_UNIV_conv [symmetric] .
from wqo_on_imp_wfp_on [OF this]
show ?thesis unfolding less_le_not_le [abs_def] wfp_on_UNIV .
qed

lemma wqo_on_with_bot:
assumes "wqo_on P A"
shows "wqo_on (option_le P) A⇩⊥" (is "wqo_on ?P ?A")
proof -
{ from assms have trans [unfolded transp_on_def]: "transp_on P A"
by (auto simp: wqo_on_def)
have "transp_on ?P ?A"
by (auto simp: transp_on_def elim!: with_bot_cases, insert trans) blast }
moreover
{ from assms and almost_full_on_with_bot
have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
ultimately
show ?thesis by (auto simp: wqo_on_def)
qed

lemma wqo_on_option_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on (option_le P) UNIV"
using wqo_on_with_bot [of P UNIV] by simp

text ‹
When two sets are wqo, then their disjoint sum is wqo.
›
lemma wqo_on_Plus:
assumes "wqo_on P A" and "wqo_on Q B"
shows "wqo_on (sum_le P Q) (A <+> B)" (is "wqo_on ?P ?A")
proof -
{ from assms have trans [unfolded transp_on_def]: "transp_on P A" "transp_on Q B"
by (auto simp: wqo_on_def)
have "transp_on ?P ?A"
unfolding transp_on_def by (auto, insert trans) (blast+) }
moreover
{ from assms and almost_full_on_Plus have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
ultimately
show ?thesis by (auto simp: wqo_on_def)
qed

lemma wqo_on_sum_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on Q UNIV ⟹ wqo_on (sum_le P Q) UNIV"
using wqo_on_Plus [of P UNIV Q UNIV] by simp

subsection ‹Dickson's Lemma›

lemma wqo_on_Sigma:
fixes A1 :: "'a set" and A2 :: "'b set"
assumes "wqo_on P1 A1" and "wqo_on P2 A2"
shows "wqo_on (prod_le P1 P2) (A1 × A2)" (is "wqo_on ?P ?A")
proof -
{ from assms have "transp_on P1 A1" and "transp_on P2 A2" by (auto simp: wqo_on_def)
hence "transp_on ?P ?A" unfolding transp_on_def prod_le_def by blast }
moreover
{ from assms and almost_full_on_Sigma [of P1 A1 P2 A2]
have "almost_full_on ?P ?A" by (auto simp: wqo_on_def) }
ultimately
show ?thesis by (auto simp: wqo_on_def)
qed

lemmas dickson = wqo_on_Sigma

lemma wqo_on_prod_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on Q UNIV ⟹ wqo_on (prod_le P Q) UNIV"
using wqo_on_Sigma [of P UNIV Q UNIV] by simp

subsection ‹Higman's Lemma›

lemma transp_on_list_emb:
assumes "transp_on P A"
shows "transp_on (list_emb P) (lists A)"
using assms and list_emb_trans [of _ _ _ P]
unfolding transp_on_def by blast

lemma wqo_on_lists:
assumes "wqo_on P A" shows "wqo_on (list_emb P) (lists A)"
using assms and almost_full_on_lists
and transp_on_list_emb by (auto simp: wqo_on_def)

lemmas higman = wqo_on_lists

lemma wqo_on_list_UNIV [intro]:
"wqo_on P UNIV ⟹ wqo_on (list_emb P) UNIV"
using wqo_on_lists [of P UNIV] by simp

text ‹
Every reflexive and transitive relation on a finite set is a wqo.
›
lemma finite_wqo_on:
assumes "finite A" and refl: "reflp_on P A" and "transp_on P A"
shows "wqo_on P A"
using assms and finite_almost_full_on by (auto simp: wqo_on_def)

lemma finite_eq_wqo_on:
assumes "finite A"
shows "wqo_on (=) A"
using finite_wqo_on [OF assms, of "(=)"]
by (auto simp: reflp_on_def transp_on_def)

lemma wqo_on_lists_over_finite_sets:
"wqo_on (list_emb (=)) (UNIV::('a::finite) list set)"
using wqo_on_lists [OF finite_eq_wqo_on [OF finite [of "UNIV::('a::finite) set"]]] by simp

lemma wqo_on_map:
fixes P and Q and h
defines "P' ≡ λx y. P x y ∧ Q (h x) (h y)"
assumes "wqo_on P A"
and "wqo_on Q B"
and subset: "h  A ⊆ B"
shows "wqo_on P' A"
proof
let ?Q = "λx y. Q (h x) (h y)"
from ‹wqo_on P A› have "transp_on P A"
by (rule wqo_on_imp_transp_on)
then show "transp_on P' A"
using ‹wqo_on Q B› and subset
unfolding wqo_on_def transp_on_def P'_def by blast

from ‹wqo_on P A› have "almost_full_on P A"
by (rule wqo_on_imp_almost_full_on)
from ‹wqo_on Q B› have "almost_full_on Q B"
by (rule wqo_on_imp_almost_full_on)

show "almost_full_on P' A"
proof
fix f
assume *: "∀i::nat. f i ∈ A"
from almost_full_on_imp_homogeneous_subseq [OF ‹almost_full_on P A› this]
obtain g :: "nat ⇒ nat"
where g: "⋀i j. i < j ⟹ g i < g j"
and **: "∀i. f (g i) ∈ A ∧ P (f (g i)) (f (g (Suc i)))"
using * by auto
from chain_transp_on_less [OF ** ‹transp_on P A›]
have **: "⋀i j. i < j ⟹ P (f (g i)) (f (g j))" .
let ?g = "λi. h (f (g i))"
from * and subset have B: "⋀i. ?g i ∈ B" by auto
with ‹almost_full_on Q B› [unfolded almost_full_on_def good_def, THEN bspec, of ?g]
obtain i j :: nat
where "i < j" and "Q (?g i) (?g j)" by blast
with ** [OF ‹i < j›] have "P' (f (g i)) (f (g j))"
by (auto simp: P'_def)
with g [OF ‹i < j›] show "good P' f" by (auto simp: good_def)
qed
qed

lemma wqo_on_UNIV_nat:
"wqo_on (≤) (UNIV :: nat set)"
unfolding wqo_on_def transp_on_def
using almost_full_on_UNIV_nat by simp

end


# Theory Kruskal

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Kruskal's Tree Theorem›

theory Kruskal
imports Well_Quasi_Orders
begin

locale kruskal_tree =
fixes F :: "('b × nat) set"
and mk :: "'b ⇒ 'a list ⇒ ('a::size)"
and root :: "'a ⇒ 'b × nat"
and args :: "'a ⇒ 'a list"
and trees :: "'a set"
assumes size_arg: "t ∈ trees ⟹ s ∈ set (args t) ⟹ size s < size t"
and root_mk: "(f, length ts) ∈ F ⟹ root (mk f ts) = (f, length ts)"
and args_mk: "(f, length ts) ∈ F ⟹ args (mk f ts) = ts"
and mk_root_args: "t ∈ trees ⟹ mk (fst (root t)) (args t) = t"
and trees_root: "t ∈ trees ⟹ root t ∈ F"
and trees_arity: "t ∈ trees ⟹ length (args t) = snd (root t)"
and trees_args: "⋀s. t ∈ trees ⟹ s ∈ set (args t) ⟹ s ∈ trees"
begin

lemma mk_inject [iff]:
assumes "(f, length ss) ∈ F" and "(g, length ts) ∈ F"
shows "mk f ss = mk g ts ⟷ f = g ∧ ss = ts"
proof -
{ assume "mk f ss = mk g ts"
then have "root (mk f ss) = root (mk g ts)"
and "args (mk f ss) = args (mk g ts)" by auto }
show ?thesis
using root_mk [OF assms(1)] and root_mk [OF assms(2)]
and args_mk [OF assms(1)] and args_mk [OF assms(2)] by auto
qed

inductive emb for P
where
arg: "⟦(f, m) ∈ F; length ts = m; ∀t∈set ts. t ∈ trees;
t ∈ set ts; emb P s t⟧ ⟹ emb P s (mk f ts)" |
list_emb: "⟦(f, m) ∈ F; (g, n) ∈ F; length ss = m; length ts = n;
∀s ∈ set ss. s ∈ trees; ∀t ∈ set ts. t ∈ trees;
P (f, m) (g, n); list_emb (emb P) ss ts⟧ ⟹ emb P (mk f ss) (mk g ts)"
monos list_emb_mono

lemma almost_full_on_trees:
assumes "almost_full_on P F"
shows "almost_full_on (emb P) trees" (is "almost_full_on ?P ?A")
proof (rule ccontr)
interpret mbs ?A .
assume "¬ ?thesis"
from mbs' [OF this] obtain m
and min: "∀g. (m, g) ∈ gseq ⟶ good ?P g" ..
then have trees: "⋀i. m i ∈ trees" by auto

define r where "r i = root (m i)" for i
define a where "a i = args (m i)" for i
define S where "S = ⋃{set (a i) | i. True}"

have m: "⋀i. m i = mk (fst (r i)) (a i)"
by (simp add: r_def a_def mk_root_args [OF trees])
have lists: "∀i. a i ∈ lists S" by (auto simp: a_def S_def)
have arity: "⋀i. length (a i) = snd (r i)"
using trees_arity [OF trees] by (auto simp: r_def a_def)
then have sig: "⋀i. (fst (r i), length (a i)) ∈ F"
using trees_root [OF trees] by (auto simp: a_def r_def)
have a_trees: "⋀i. ∀t ∈ set (a i). t ∈ trees" by (auto simp: a_def trees_args [OF trees])

have "almost_full_on ?P S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain s :: "nat ⇒ 'a"
where S: "⋀i. s i ∈ S" and bad_s: "bad ?P s" by (auto simp: almost_full_on_def)

define n where "n = (LEAST n. ∃k. s k ∈ set (a n))"
have "∃n. ∃k. s k ∈ set (a n)" using S by (force simp: S_def)
from LeastI_ex [OF this] obtain k
where sk: "s k ∈ set (a n)" by (auto simp: n_def)
have args: "⋀k. ∃m ≥ n. s k ∈ set (a m)"
using S by (auto simp: S_def) (metis Least_le n_def)

define m' where "m' i = (if i < n then m i else s (k + (i - n)))" for i

have m'_less: "⋀i. i < n ⟹ m' i = m i" by (simp add: m'_def)
have m'_geq: "⋀i. i ≥ n ⟹ m' i = s (k + (i - n))" by (simp add: m'_def)

proof
assume "good ?P m'"
then obtain i j where "i < j" and emb: "?P (m' i) (m' j)" by auto
{ assume "j < n"
with ‹i < j› and emb have "?P (m i) (m j)" by (auto simp: m'_less)
with ‹i < j› and bad have False by blast }
moreover
{ assume "n ≤ i"
with ‹i < j› and emb have "?P (s (k + (i - n))) (s (k + (j - n)))"
and "k + (i - n) < k + (j - n)" by (auto simp: m'_geq)
with bad_s have False by auto }
moreover
{ assume "i < n" and "n ≤ j"
with ‹i < j› and emb have *: "?P (m i) (s (k + (j - n)))" by (auto simp: m'_less m'_geq)
with args obtain l where "l ≥ n" and **: "s (k + (j - n)) ∈ set (a l)" by blast
from emb.arg [OF sig [of l] _ a_trees [of l] ** *]
have "?P (m i) (m l)" by (simp add: m)
moreover have "i < l" using ‹i < n› and ‹n ≤ l› by auto
ultimately have False using bad by blast }
ultimately show False using ‹i < j› by arith
qed
moreover have "(m, m') ∈ gseq"
proof -
have "m ∈ SEQ ?A" using trees by auto
moreover have "m' ∈ SEQ ?A"
using trees and S and trees_args [OF trees] by (auto simp: m'_def a_def S_def)
moreover have "∀i < n. m i = m' i" by (auto simp: m'_less)
moreover have "size (m' n) < size (m n)"
using sk and size_arg [OF trees, unfolded m]
by (auto simp: m m'_geq root_mk [OF sig] args_mk [OF sig])
ultimately show ?thesis by (auto simp: gseq_def)
qed
ultimately show False using min by blast
qed
from almost_full_on_lists [OF this, THEN almost_full_on_imp_homogeneous_subseq, OF lists]
obtain φ :: "nat ⇒ nat"
where less: "⋀i j. i < j ⟹ φ i < φ j"
and lemb: "⋀i j. i < j ⟹ list_emb ?P (a (φ i)) (a (φ j))" by blast
have roots: "⋀i. r (φ i) ∈ F" using trees [THEN trees_root] by (auto simp: r_def)
then have "r ∘ φ ∈ SEQ F" by auto
with assms have "good P (r ∘ φ)" by (auto simp: almost_full_on_def)
then obtain i j
where "i < j" and "P (r (φ i)) (r (φ j))" by auto
with lemb [OF ‹i < j›] have "?P (m (φ i)) (m (φ j))"
using sig and arity and a_trees by (auto simp: m intro!: emb.list_emb)
with less [OF ‹i < j›] and bad show False by blast
qed

inductive_cases
emb_mk2 [consumes 1, case_names arg list_emb]: "emb P s (mk g ts)"

inductive_cases
list_emb_Nil2_cases: "list_emb P xs []" and
list_emb_Cons_cases: "list_emb P xs (y#ys)"

lemma list_emb_trans_right:
assumes "list_emb P xs ys" and "list_emb (λy z. P y z ∧ (∀x. P x y ⟶ P x z)) ys zs"
shows "list_emb P xs zs"
using assms(2, 1) by (induct arbitrary: xs) (auto elim!: list_emb_Nil2_cases list_emb_Cons_cases)

lemma emb_trans:
assumes trans: "⋀f g h. f ∈ F ⟹ g ∈ F ⟹ h ∈ F ⟹ P f g ⟹ P g h ⟹ P f h"
assumes "emb P s t" and "emb P t u"
shows "emb P s u"
using assms(3, 2)
proof (induct arbitrary: s)
case (arg f m ts v)
then show ?case by (auto intro: emb.arg)
next
case (list_emb f m g n ss ts)
note IH = this
from ‹emb P s (mk f ss)›
show ?case
proof (cases rule: emb_mk2)
case arg
then show ?thesis using IH by (auto elim!: list_emb_set intro: emb.arg)
next
case list_emb
then show ?thesis using IH by (auto intro: emb.intros dest: trans list_emb_trans_right)
qed
qed

lemma transp_on_emb:
assumes "transp_on P F"
shows "transp_on (emb P) trees"
using assms and emb_trans [of P] unfolding transp_on_def by blast

lemma kruskal:
assumes "wqo_on P F"
shows "wqo_on (emb P) trees"
using almost_full_on_trees [of P] and assms by (metis transp_on_emb wqo_on_def)

end

end



# Theory Kruskal_Examples

theory Kruskal_Examples
imports Kruskal
begin

datatype 'a tree = Node 'a "'a tree list"

fun node
where
"node (Node f ts) = (f, length ts)"

fun succs
where
"succs (Node f ts) = ts"

inductive_set trees for A
where
"f ∈ A ⟹ ∀t ∈ set ts. t ∈ trees A ⟹ Node f ts ∈ trees A"

lemma [simp]:
"trees UNIV = UNIV"
proof -
{ fix t :: "'a tree"
have "t ∈ trees UNIV"
by (induct t) (auto intro: trees.intros) }
then show ?thesis by auto
qed

interpretation kruskal_tree_tree: kruskal_tree "A × UNIV" Node node succs "trees A" for A
apply (unfold_locales)
apply auto
apply (case_tac [!] t rule: trees.cases)
apply auto
by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_tree_tree.almost_full_on_trees
thm kruskal_tree_tree.kruskal

definition "tree_emb A P = kruskal_tree_tree.emb A (prod_le P (λ_ _. True))"

lemma wqo_on_trees:
assumes "wqo_on P A"
shows "wqo_on (tree_emb A P) (trees A)"
using wqo_on_Sigma [OF assms wqo_on_UNIV, THEN kruskal_tree_tree.kruskal]

text ‹
If the type @{typ "'a"} is well-quasi-ordered by ‹P›, then trees of type @{typ "'a tree"}
are well-quasi-ordered by the homeomorphic embedding relation.
›
instantiation tree :: (wqo) wqo
begin
definition "s ≤ t ⟷ tree_emb UNIV (≤) s t"
definition "(s :: 'a tree) < t ⟷ s ≤ t ∧ ¬ (t ≤ s)"

instance
by (rule class.wqo.of_class.intro)
(auto simp: less_eq_tree_def [abs_def] less_tree_def [abs_def]
intro: wqo_on_trees [of _ UNIV, simplified])
end

datatype ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"

fun root
where
"root (Fun f ts) = (f, length ts)"

fun args
where
"args (Fun f ts) = ts"

inductive_set gterms for F
where
"(f, n) ∈ F ⟹ length ts = n ⟹ ∀s ∈ set ts. s ∈ gterms F ⟹ Fun f ts ∈ gterms F"

interpretation kruskal_term: kruskal_tree F Fun root args "gterms F" for F
apply (unfold_locales)
apply auto
apply (case_tac [!] t rule: gterms.cases)
apply auto
by (metis less_not_refl not_less_eq size_list_estimation)

thm kruskal_term.almost_full_on_trees

inductive_set terms
where
"∀t ∈ set ts. t ∈ terms ⟹ Fun f ts ∈ terms"

interpretation kruskal_variadic: kruskal_tree UNIV Fun root args terms
apply (unfold_locales)
apply auto
apply (case_tac [!] t rule: terms.cases)
apply auto
by (metis less_not_refl not_less_eq size_list_estimation)

datatype 'a exp = V 'a | C nat | Plus "'a exp" "'a exp"

datatype 'a symb = v 'a | c nat | p

fun mk
where
"mk (v x) [] = V x" |
"mk (c n) [] = C n" |
"mk p [a, b] = Plus a b"

fun rt
where
"rt (V x) = (v x, 0::nat)" |
"rt (C n) = (c n, 0)" |
"rt (Plus a b) = (p, 2)"

fun ags
where
"ags (V x) = []" |
"ags (C n) = []" |
"ags (Plus a b) = [a, b]"

inductive_set exps
where
"V x ∈ exps" |
"C n ∈ exps" |
"a ∈ exps ⟹ b ∈ exps ⟹ Plus a b ∈ exps"

lemma [simp]:
assumes "length ts = 2"
shows "rt (mk p ts) = (p, 2)"
using assms by (induct ts) (auto, case_tac ts, auto)

lemma [simp]:
assumes "length ts = 2"
shows "ags (mk p ts) = ts"
using assms by (induct ts) (auto, case_tac ts, auto)

interpretation kruskal_exp: kruskal_tree
"{(v x, 0) | x. True} ∪ {(c n, 0) | n. True} ∪ {(p, 2)}"
mk rt ags exps
apply (unfold_locales)
apply auto
apply (case_tac [!] t rule: exps.cases)
by auto

thm kruskal_exp.almost_full_on_trees

hide_const (open) tree_emb V C Plus v c p

end


# Theory Wqo_Instances

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Instances of Well-Quasi-Orders›

theory Wqo_Instances
imports Kruskal
begin

subsection ‹The Option Type is Well-Quasi-Ordered›

instantiation option :: (wqo) wqo
begin
definition "x ≤ y ⟷ option_le (≤) x y"
definition "(x :: 'a option) < y ⟷ x ≤ y ∧ ¬ (y ≤ x)"

instance
by (rule class.wqo.of_class.intro)
(auto simp: less_eq_option_def [abs_def] less_option_def [abs_def])
end

subsection ‹The Sum Type is Well-Quasi-Ordered›

instantiation sum :: (wqo, wqo) wqo
begin
definition "x ≤ y ⟷ sum_le (≤) (≤) x y"
definition "(x :: 'a + 'b) < y ⟷ x ≤ y ∧ ¬ (y ≤ x)"

instance
by (rule class.wqo.of_class.intro)
(auto simp: less_eq_sum_def [abs_def] less_sum_def [abs_def])
end

subsection ‹Pairs are Well-Quasi-Ordered›

text ‹If types @{typ "'a"} and @{typ "'b"} are well-quasi-ordered by ‹P›
and ‹Q›, then pairs of type @{typ "'a × 'b"} are well-quasi-ordered by
the pointwise combination of ‹P› and ‹Q›.›

instantiation prod :: (wqo, wqo) wqo
begin
definition "p ≤ q ⟷ prod_le (≤) (≤) p q"
definition "(p :: 'a × 'b) < q ⟷ p ≤ q ∧ ¬ (q ≤ p)"

instance
by (rule class.wqo.of_class.intro)
(auto simp: less_eq_prod_def [abs_def] less_prod_def [abs_def])
end

subsection ‹Lists are Well-Quasi-Ordered›

text ‹If the type @{typ "'a"} is well-quasi-ordered by ‹P›, then
lists of type @{typ "'a list"} are well-quasi-ordered by the homeomorphic
embedding relation.›

instantiation list :: (wqo) wqo
begin
definition "xs ≤ ys ⟷ list_emb (≤) xs ys"
definition "(xs :: 'a list) < ys ⟷ xs ≤ ys ∧ ¬ (ys ≤ xs)"

instance
by (rule class.wqo.of_class.intro)
(auto simp: less_eq_list_def [abs_def] less_list_def [abs_def])
end

end



# Theory Multiset_Extension

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Multiset Extension of Orders (as Binary Predicates)›

(*TODO: move theory (and maybe rename)*)

theory Multiset_Extension
imports
Open_Induction.Restricted_Predicates
"HOL-Library.Multiset"
begin

definition multisets :: "'a set ⇒ 'a multiset set" where
"multisets A = {M. set_mset M ⊆ A}"

lemma in_multisets_iff:
"M ∈ multisets A ⟷ set_mset M ⊆ A"

lemma empty_multisets [simp]:
"{#} ∈ multisets F"

lemma multisets_union [simp]:
"M ∈ multisets A ⟹ N ∈ multisets A ⟹ M + N ∈ multisets A"

definition mulex1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"mulex1 P = (λM N. (M, N) ∈ mult1 {(x, y). P x y})"

lemma mulex1_empty [iff]:
"mulex1 P M {#} ⟷ False"
using not_less_empty [of M "{(x, y). P x y}"]
by (auto simp: mulex1_def)

lemma mulex1_add: "mulex1 P N (M0 + {#a#}) ⟹
(∃M. mulex1 P M M0 ∧ N = M + {#a#}) ∨
(∃K. (∀b. b ∈# K ⟶ P b a) ∧ N = M0 + K)"
using less_add [of N a M0 "{(x, y). P x y}"]
by (auto simp: mulex1_def)

"mulex1 P A (add_mset a A)"
proof -
let ?R = "{(x, y). P x y}"
thm mult1_def
have "A + {#a#} = A + {#a#}" by simp
moreover have "A = A + {#}" by simp
moreover have "∀b. b ∈# {#} ⟶ (b, a) ∈ ?R" by simp
ultimately have "(A, add_mset a A) ∈ mult1 ?R"
unfolding mult1_def by blast
then show ?thesis by (simp add: mulex1_def)
qed

lemma empty_mult1 [simp]:
"({#}, {#a#}) ∈ mult1 R"
proof -
have "{#a#} = {#} + {#a#}" by simp
moreover have "{#} = {#} + {#}" by simp
moreover have "∀b. b ∈# {#} ⟶ (b, a) ∈ R" by simp
ultimately show ?thesis unfolding mult1_def by force
qed

lemma empty_mulex1 [simp]:
"mulex1 P {#} {#a#}"
using empty_mult1 [of a "{(x, y). P x y}"] by (simp add: mulex1_def)

definition mulex_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"mulex_on P A = (restrict_to (mulex1 P) (multisets A))⇧+⇧+"

abbreviation mulex :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ 'a multiset ⇒ bool" where
"mulex P ≡ mulex_on P UNIV"

lemma mulex_on_induct [consumes 1, case_names base step, induct pred: mulex_on]:
assumes "mulex_on P A M N"
and "⋀M N. ⟦M ∈ multisets A; N ∈ multisets A; mulex1 P M N⟧ ⟹ Q M N"
and "⋀L M N. ⟦mulex_on P A L M; Q L M; N ∈ multisets A; mulex1 P M N⟧ ⟹ Q L N"
shows "Q M N"
using assms unfolding mulex_on_def by (induct) blast+

assumes "a ∈ A" and "M ∈ multisets A"
shows "mulex_on P A M (add_mset a M)"
proof -
have "mulex1 P M (M + {#a#})" by simp
with assms have "restrict_to (mulex1 P) (multisets A) M (add_mset a M)"
by (auto simp: multisets_def)
then show ?thesis unfolding mulex_on_def by blast
qed

lemma singleton_multisets [iff]:
"{#x#} ∈ multisets A ⟷ x ∈ A"
by (auto simp: multisets_def)

lemma union_multisetsD:
assumes "M + N ∈ multisets A"
shows "M ∈ multisets A ∧ N ∈ multisets A"
using assms by (auto simp: multisets_def)

lemma mulex_on_multisetsD [dest]:
assumes "mulex_on P F M N"
shows "M ∈ multisets F" and "N ∈ multisets F"
using assms by (induct) auto

lemma union_multisets_iff [iff]:
"M + N ∈ multisets A ⟷ M ∈ multisets A ∧ N ∈ multisets A"
by (auto dest: union_multisetsD)

"add_mset a M ∈ multisets A ⟷ a ∈ A ∧ M ∈ multisets A"

lemma mulex_on_trans:
"mulex_on P A L M ⟹ mulex_on P A M N ⟹ mulex_on P A L N"
by (auto simp: mulex_on_def)

lemma transp_on_mulex_on:
"transp_on (mulex_on P A) B"
using mulex_on_trans [of P A] by (auto simp: transp_on_def)

assumes "mulex_on P A M N" and "a ∈ A"
shows "mulex_on P A M (add_mset a N)"
proof -
from assms have "a ∈ A" and "N ∈ multisets A" by auto
then have "mulex_on P A N (add_mset a N)" by simp
with ‹mulex_on P A M N› show ?thesis by (rule mulex_on_trans)
qed

lemma empty_mulex_on [simp]:
assumes "M ≠ {#}" and "M ∈ multisets A"
shows "mulex_on P A {#} M"
using assms
proof (induct M)
show ?case
proof (cases "M = {#}")
assume "M = {#}"
with add show ?thesis by (auto simp: mulex_on_def)
next
assume "M ≠ {#}"
with add show ?thesis by (auto intro: mulex_on_trans)
qed
qed simp

assumes "M ∈ multisets A" and "K ∈ multisets A" and "K ≠ {#}"
shows "mulex_on P A M (M + K)"
using assms
proof (induct K)
case empty
then show ?case by (cases "K = {#}") auto
next
show ?case
proof (cases "M = {#}")
assume "M = {#}" with add show ?thesis by auto
next
assume "M ≠ {#}" with add show ?thesis
qed
qed

lemma mult1_singleton [iff]:
"({#x#}, {#y#}) ∈ mult1 R ⟷ (x, y) ∈ R"
proof
assume "(x, y) ∈ R"
then have "{#y#} = {#} + {#y#}"
and "{#x#} = {#} + {#x#}"
and "∀b. b ∈# {#x#} ⟶ (b, y) ∈ R" by auto
then show "({#x#}, {#y#}) ∈ mult1 R" unfolding mult1_def by blast
next
assume "({#x#}, {#y#}) ∈ mult1 R"
then obtain M0 K a
where "{#y#} = add_mset a M0"
and "{#x#} = M0 + K"
and "∀b. b ∈# K ⟶ (b, a) ∈ R"
unfolding mult1_def by blast
then show "(x, y) ∈ R" by (auto simp: add_eq_conv_diff)
qed

lemma mulex1_singleton [iff]:
"mulex1 P {#x#} {#y#} ⟷ P x y"
using mult1_singleton [of x y "{(x, y). P x y}"] by (simp add: mulex1_def)

lemma singleton_mulex_onI:
"P x y ⟹ x ∈ A ⟹ y ∈ A ⟹ mulex_on P A {#x#} {#y#}"
by (auto simp: mulex_on_def)

assumes "(mulex_on P A)⇧=⇧= M N" and "M ∈ multisets A" and "a ∈ A"
shows "mulex_on P A M (N + {#a#})"
using assms by (cases "M = N") simp_all

assumes "(mulex_on P A)⇧=⇧= M N" and "M ∈ multisets A" and "a ∈ A"
shows "mulex_on P A M ({#a#} + N)"

lemma mulex_on_union_right [simp]:
assumes "mulex_on P F A B" and "K ∈ multisets F"
shows "mulex_on P F A (K + B)"
using assms
proof (induct K)
then have "a ∈ F" and "mulex_on P F A (B + K)" by (auto simp: multisets_def ac_simps)
then have "mulex_on P F A ((B + K) + {#a#})" by simp
then show ?case by (simp add: ac_simps)
qed simp

lemma mulex_on_union_right' [simp]:
assumes "mulex_on P F A B" and "K ∈ multisets F"
shows "mulex_on P F A (B + K)"
using mulex_on_union_right [OF assms] by (simp add: ac_simps)

text ‹Adapted from @{thm all_accessible} in @{theory "HOL-Library.Multiset"}.›
lemma accessible_on_mulex1_multisets:
assumes wf: "wfp_on P A"
shows "∀M∈multisets A. accessible_on (mulex1 P) (multisets A) M"
proof
let ?P = "mulex1 P"
let ?A = "multisets A"
let ?acc = "accessible_on ?P ?A"
{
fix M M0 a
assume M0: "?acc M0"
and "a ∈ A"
and "M0 ∈ ?A"
and wf_hyp: "⋀b. ⟦b ∈ A; P b a⟧ ⟹ (∀M. ?acc (M) ⟶ ?acc (M + {#b#}))"
and acc_hyp: "∀M. M ∈ ?A ∧ ?P M M0 ⟶ ?acc (M + {#a#})"
then have "add_mset a M0 ∈ ?A" by (auto simp: multisets_def)
then have "?acc (add_mset a M0)"
proof (rule accessible_onI [of "add_mset a M0"])
fix N
assume "N ∈ ?A"
and "?P N (add_mset a M0)"
then have "((∃M. M ∈ ?A ∧ ?P M M0 ∧ N = M + {#a#}) ∨
(∃K. (∀b. b ∈# K ⟶ P b a) ∧ N = M0 + K))"
using mulex1_add [of P N M0 a] by (auto simp: multisets_def)
then show "?acc (N)"
proof (elim exE disjE conjE)
fix M assume "M ∈ ?A" and "?P M M0" and N: "N = M + {#a#}"
from acc_hyp have "M ∈ ?A ∧ ?P M M0 ⟶ ?acc (M + {#a#})" ..
with ‹M ∈ ?A› and ‹?P M M0› have "?acc (M + {#a#})" by blast
then show "?acc (N)" by (simp only: N)
next
fix K
assume N: "N = M0 + K"
assume "∀b. b ∈# K ⟶ P b a"
moreover from N and ‹N ∈ ?A› have "K ∈ ?A" by (auto simp: multisets_def)
ultimately have "?acc (M0 + K)"
proof (induct K)
case empty
from M0 show "?acc (M0 + {#})" by simp
next
from add.prems have "x ∈ A" and "P x a" by (auto simp: multisets_def)
with wf_hyp have "∀M. ?acc M ⟶ ?acc (M + {#x#})" by blast
moreover from add have "?acc (M0 + K)" by (auto simp: multisets_def)
ultimately show "?acc (M0 + (add_mset x K))" by simp
qed
then show "?acc N" by (simp only: N)
qed
qed
} note tedious_reasoning = this

fix M
assume "M ∈ ?A"
then show "?acc M"
proof (induct M)
show "?acc {#}"
proof (rule accessible_onI)
show "{#} ∈ ?A" by (auto simp: multisets_def)
next
fix b assume "?P b {#}" then show "?acc b" by simp
qed
next
then have "?acc M" by (auto simp: multisets_def)
from add have "a ∈ A" by (auto simp: multisets_def)
with wf have "∀M. ?acc M ⟶ ?acc (add_mset a M)"
proof (induct)
case (less a)
then have r: "⋀b. ⟦b ∈ A; P b a⟧ ⟹ (∀M. ?acc M ⟶ ?acc (M + {#b#}))" by auto
show "∀M. ?acc M ⟶ ?acc (add_mset a M)"
proof (intro allI impI)
fix M'
assume "?acc M'"
moreover then have "M' ∈ ?A" by (blast dest: accessible_on_imp_mem)
ultimately show "?acc (add_mset a M')"
by (induct) (rule tedious_reasoning [OF _ ‹a ∈ A› _ r], auto)
qed
qed
with ‹?acc (M)› show "?acc (add_mset a M)" by blast
qed
qed

lemmas wfp_on_mulex1_multisets =
accessible_on_mulex1_multisets [THEN accessible_on_imp_wfp_on]

lemmas irreflp_on_mulex1 =
wfp_on_mulex1_multisets [THEN wfp_on_imp_irreflp_on]

lemma wfp_on_mulex_on_multisets:
assumes "wfp_on P A"
shows "wfp_on (mulex_on P A) (multisets A)"
using wfp_on_mulex1_multisets [OF assms]
by (simp only: mulex_on_def wfp_on_restrict_to_tranclp_wfp_on_conv)

lemmas irreflp_on_mulex_on =
wfp_on_mulex_on_multisets [THEN wfp_on_imp_irreflp_on]

lemma mulex1_union:
"mulex1 P M N ⟹ mulex1 P (K + M) (K + N)"
by (auto simp: mulex1_def mult1_union)

lemma mulex_on_union:
assumes "mulex_on P A M N" and "K ∈ multisets A"
shows "mulex_on P A (K + M) (K + N)"
using assms
proof (induct)
case (base M N)
then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
moreover from base have "(K + M) ∈ multisets A"
and "(K + N) ∈ multisets A" by (auto simp: multisets_def)
ultimately have "restrict_to (mulex1 P) (multisets A) (K + M) (K + N)" by auto
then show ?case by (auto simp: mulex_on_def)
next
case (step L M N)
then have "mulex1 P (K + M) (K + N)" by (blast dest: mulex1_union)
moreover from step have "(K + M) ∈ multisets A" and "(K + N) ∈ multisets A" by blast+
ultimately have "(restrict_to (mulex1 P) (multisets A))⇧+⇧+ (K + M) (K + N)" by auto
moreover have "mulex_on P A (K + L) (K + M)" using step by blast
ultimately show ?case by (auto simp: mulex_on_def)
qed

lemma mulex_on_union':
assumes "mulex_on P A M N" and "K ∈ multisets A"
shows "mulex_on P A (M + K) (N + K)"
using mulex_on_union [OF assms] by (simp add: ac_simps)

assumes "mulex_on P A M N" and "m ∈ A"
apply (rule mulex_on_union')
using assms by auto

lemma union_mulex_on_mono:
"mulex_on P F A C ⟹ mulex_on P F B D ⟹ mulex_on P F (A + B) (C + D)"
by (metis mulex_on_multisetsD mulex_on_trans mulex_on_union mulex_on_union')

assumes "P m n" and "m ∈ A" and "n ∈ A" and "M ∈ multisets A"
apply (rule mulex_on_union)
using assms by (auto simp: mulex_on_def)

assumes "P m n" and "m ∈ A" and "n ∈ A" and "mulex_on P A M N"
apply (rule union_mulex_on_mono)
using assms by (auto simp: mulex_on_def)

lemma union_mulex_on_mono1:
"A ∈ multisets F ⟹ (mulex_on P F)⇧=⇧= A C ⟹ mulex_on P F B D ⟹
mulex_on P F (A + B) (C + D)"
by (auto intro: union_mulex_on_mono mulex_on_union)

lemma union_mulex_on_mono2:
"B ∈ multisets F ⟹ mulex_on P F A C ⟹ (mulex_on P F)⇧=⇧= B D ⟹
mulex_on P F (A + B) (C + D)"
by (auto intro: union_mulex_on_mono mulex_on_union')

lemma mult1_mono:
assumes "⋀x y. ⟦x ∈ A; y ∈ A; (x, y) ∈ R⟧ ⟹ (x, y) ∈ S"
and "M ∈ multisets A"
and "N ∈ multisets A"
and "(M, N) ∈ mult1 R"
shows "(M, N) ∈ mult1 S"
using assms unfolding mult1_def multisets_def
by auto (metis (full_types) subsetD)

lemma mulex1_mono:
assumes "⋀x y. ⟦x ∈ A; y ∈ A; P x y⟧ ⟹ Q x y"
and "M ∈ multisets A"
and "N ∈ multisets A"
and "mulex1 P M N"
shows "mulex1 Q M N"
using mult1_mono [of A "{(x, y). P x y}" "{(x, y). Q x y}" M N]
and assms unfolding mulex1_def by blast

lemma mulex_on_mono:
assumes *: "⋀x y. ⟦x ∈ A; y ∈ A; P x y⟧ ⟹ Q x y"
and "mulex_on P A M N"
shows "mulex_on Q A M N"
proof -
let ?rel = "λP. (restrict_to (mulex1 P) (multisets A))"
from ‹mulex_on P A M N› have "(?rel P)⇧+⇧+ M N" by (simp add: mulex_on_def)
then have "(?rel Q)⇧+⇧+ M N"
proof (induct rule: tranclp.induct)
case (r_into_trancl M N)
then have "M ∈ multisets A" and "N ∈ multisets A" by auto
from mulex1_mono [OF * this] and r_into_trancl
show ?case by auto
next
case (trancl_into_trancl L M N)
then have "M ∈ multisets A" and "N ∈ multisets A" by auto
from mulex1_mono [OF * this] and trancl_into_trancl
have "?rel Q M N" by auto
with ‹(?rel Q)⇧+⇧+ L M› show ?case by (rule tranclp.trancl_into_trancl)
qed
then show ?thesis by (simp add: mulex_on_def)
qed

lemma mult1_reflcl:
assumes "(M, N) ∈ mult1 R"
shows "(M, N) ∈ mult1 (R⇧=)"
using assms by (auto simp: mult1_def)

lemma mulex1_reflclp:
assumes "mulex1 P M N"
shows "mulex1 (P⇧=⇧=) M N"
using mulex1_mono [of UNIV P "P⇧=⇧=" M N, OF _ _ _ assms]
by (auto simp: multisets_def)

lemma mulex_on_reflclp:
assumes "mulex_on P A M N"
shows "mulex_on (P⇧=⇧=) A M N"
using mulex_on_mono [OF _ assms, of "P⇧=⇧="] by auto

lemma surj_on_multisets_mset:
"∀M∈multisets A. ∃xs∈lists A. M = mset xs"
proof
fix M
assume "M ∈ multisets A"
then show "∃xs∈lists A. M = mset xs"
proof (induct M)
case empty show ?case by simp
next
then obtain xs where "xs ∈ lists A" and "M = mset xs" by auto
then have "add_mset a M = mset (a # xs)" by simp
moreover have "a # xs ∈ lists A" using ‹xs ∈ lists A› and add by auto
ultimately show ?case by blast
qed
qed

lemma image_mset_lists [simp]:
"mset  lists A = multisets A"
using surj_on_multisets_mset [of A]
by auto (metis mem_Collect_eq multisets_def set_mset_mset subsetI)

lemma multisets_UNIV [simp]: "multisets UNIV = UNIV"
by (metis image_mset_lists lists_UNIV surj_mset)

lemma non_empty_multiset_induct [consumes 1, case_names singleton add]:
assumes "M ≠ {#}"
and "⋀x. P {#x#}"
and "⋀x M. P M ⟹ P (add_mset x M)"
shows "P M"
using assms by (induct M) auto

lemma mulex_on_all_strict:
assumes "X ≠ {#}"
assumes "X ∈ multisets A" and "Y ∈ multisets A"
and *: "∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)"
shows "mulex_on P A Y X"
using assms
proof (induction X arbitrary: Y rule: non_empty_multiset_induct)
case (singleton x)
then have "mulex1 P Y {#x#}"
unfolding mulex1_def mult1_def
by auto
with singleton show ?case by (auto simp: mulex_on_def)
next
let ?Y = "{# y ∈# Y. ∃x. x ∈# M ∧ P y x #}"
let ?Z = "Y - ?Y"
have Y: "Y = ?Z + ?Y" by (subst multiset_eq_iff) auto
from ‹Y ∈ multisets A› have "?Y ∈ multisets A" by (metis multiset_partition union_multisets_iff)
moreover have "∀y. y ∈# ?Y ⟶ (∃x. x ∈# M ∧ P y x)" by auto
moreover have "M ∈ multisets A" using add by auto
ultimately have "mulex_on P A ?Y M" using add by blast
moreover have "mulex_on P A ?Z {#x#}"
proof -
have "{#x#} = {#} + {#x#}" by simp
moreover have "?Z = {#} + ?Z" by simp
moreover have "∀y. y ∈# ?Z ⟶ P y x"
ultimately have "mulex1 P ?Z {#x#}" unfolding mulex1_def mult1_def by blast
moreover have "{#x#} ∈ multisets A" using add.prems by auto
moreover have "?Z ∈ multisets A"
using ‹Y ∈ multisets A› by (metis diff_union_cancelL multiset_partition union_multisetsD)
ultimately show ?thesis by (auto simp: mulex_on_def)
qed
ultimately have "mulex_on P A (?Y + ?Z) (M + {#x#})" by (rule union_mulex_on_mono)
then show ?case using Y by (simp add: ac_simps)
qed

text ‹The following lemma shows that the textbook definition (e.g.,
Term Rewriting and All That'') is the same as the one used below.›
lemma diff_set_Ex_iff:
"X ≠ {#} ∧ X ⊆# M ∧ N = (M - X) + Y ⟷ X ≠ {#} ∧ (∃Z. M = Z + X ∧ N = Z + Y)"
by (auto) (metis add_diff_cancel_left' multiset_diff_union_assoc union_commute)

text ‹Show that @{const mulex_on} is equivalent to the textbook definition
of multiset-extension for transitive base orders.›
lemma mulex_on_alt_def:
assumes trans: "transp_on P A"
shows "mulex_on P A M N ⟷ M ∈ multisets A ∧ N ∈ multisets A ∧ (∃X Y Z.
X ≠ {#} ∧ N = Z + X ∧ M = Z + Y ∧ (∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)))"
(is "?P M N ⟷ ?Q M N")
proof
assume "?P M N" then show "?Q M N"
proof (induct M N)
case (base M N)
then obtain a M0 K where N: "N = M0 + {#a#}"
and M: "M = M0 + K"
and *: "∀b. b ∈# K ⟶ P b a"
and "M ∈ multisets A" and "N ∈ multisets A" by (auto simp: mulex1_def mult1_def)
moreover then have "{#a#} ∈ multisets A" and "K ∈ multisets A" by auto
moreover have "{#a#} ≠ {#}" by auto
moreover have "N = M0 + {#a#}" by fact
moreover have "M = M0 + K" by fact
moreover have "∀y. y ∈# K ⟶ (∃x. x ∈# {#a#} ∧ P y x)" using * by auto
ultimately show ?case by blast
next
case (step L M N)
then obtain X Y Z
where "L ∈ multisets A" and "M ∈ multisets A" and "N ∈ multisets A"
and "X ∈ multisets A" and "Y ∈ multisets A"
and M: "M = Z + X"
and L: "L = Z + Y" and "X ≠ {#}"
and Y: "∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)"
and "mulex1 P M N"
by blast
from ‹mulex1 P M N› obtain a M0 K
where N: "N = add_mset a M0" and M': "M = M0 + K"
and *: "∀b. b ∈# K ⟶ P b a" unfolding mulex1_def mult1_def by blast
have L': "L = (M - X) + Y" by (simp add: L M)
have K: "∀y. y ∈# K ⟶ (∃x. x ∈# {#a#} ∧ P y x)" using * by auto

txt ‹The remainder of the proof is adapted from the proof of Lemma 2.5.4. of
the book Term Rewriting and All That.''›
let ?X = "add_mset a (X - K)"
let ?Y = "(K - X) + Y"

have "L ∈ multisets A" and "N ∈ multisets A" by fact+
moreover have "?X ≠ {#} ∧ (∃Z. N = Z + ?X ∧ L = Z + ?Y)"
proof -
have "?X ≠ {#}" by auto
moreover have "?X ⊆# N"
moreover have "L = (N - ?X) + ?Y"
proof (rule multiset_eqI)
fix x :: 'a
let ?c = "λM. count M x"
let ?ic = "λx. int (?c x)"
from ‹?X ⊆# N› have *: "?c {#a#} + ?c (X - K) ≤ ?c N"
by (auto simp add: subseteq_mset_def split: if_splits)
from * have **: "?c (X - K) ≤ ?c M0" unfolding N by (auto split: if_splits)
have "?ic (N - ?X + ?Y) = int (?c N - ?c ?X) + ?ic ?Y" by simp
also have "… = int (?c N - (?c {#a#} + ?c (X - K))) + ?ic (K - X) + ?ic Y" by simp
also have "… = ?ic N - (?ic {#a#} + ?ic (X - K)) + ?ic (K - X) + ?ic Y"
using of_nat_diff [OF *] by simp
also have "… = (?ic N - ?ic {#a#}) - ?ic (X - K) + ?ic (K - X) + ?ic Y" by simp
also have "… = (?ic N - ?ic {#a#}) + (?ic (K - X) - ?ic (X - K)) + ?ic Y" by simp
also have "… = (?ic N - ?ic {#a#}) + (?ic K - ?ic X) + ?ic Y" by simp
also have "… = (?ic N - ?ic ?X) + ?ic ?Y" by (simp add: N)
also have "… = ?ic L"
unfolding L' M' N
using ** by (simp add: algebra_simps)
finally show "?c L = ?c (N - ?X + ?Y)" by simp
qed
ultimately show ?thesis by (metis diff_set_Ex_iff)
qed
moreover have "∀y. y ∈# ?Y ⟶ (∃x. x ∈# ?X ∧ P y x)"
proof (intro allI impI)
fix y assume "y ∈# ?Y"
then have "y ∈# K - X ∨ y ∈# Y" by auto
then show "∃x. x ∈# ?X ∧ P y x"
proof
assume "y ∈# K - X"
then have "y ∈# K" by (rule in_diffD)
with K show ?thesis by auto
next
assume "y ∈# Y"
with Y obtain x where "x ∈# X" and "P y x" by blast
{ assume "x ∈# X - K" with ‹P y x› have ?thesis by auto }
moreover
{ assume "x ∈# K" with * have "P x a" by auto
moreover have "y ∈ A" using ‹Y ∈ multisets A› and ‹y ∈# Y› by (auto simp: multisets_def)
moreover have "a ∈ A" using ‹N ∈ multisets A› by (auto simp: N)
moreover have "x ∈ A" using ‹M ∈ multisets A› and ‹x ∈# K› by (auto simp: M' multisets_def)
ultimately have "P y a" using ‹P y x› and trans unfolding transp_on_def by blast
then have ?thesis by force }
moreover from ‹x ∈# X› have "x ∈# X - K ∨ x ∈# K"
by (auto simp add: in_diff_count not_in_iff)
ultimately show ?thesis by auto
qed
qed
ultimately show ?case by blast
qed
next
assume "?Q M N"
then obtain X Y Z where "M ∈ multisets A" and "N ∈ multisets A"
and "X ≠ {#}" and N: "N = Z + X" and M: "M = Z + Y"
and *: "∀y. y ∈# Y ⟶ (∃x. x ∈# X ∧ P y x)" by blast
with mulex_on_all_strict [of X A Y] have "mulex_on P A Y X" by auto
moreover from ‹N ∈ multisets A› have "Z ∈ multisets A" by (auto simp: N)
ultimately show "?P M N" unfolding M N by (metis mulex_on_union)
qed

end



# Theory Wqo_Multiset

(*  Title:      Well-Quasi-Orders
Author:     Christian Sternagel <c.sternagel@gmail.com>
Maintainer: Christian Sternagel
*)

section ‹Multiset Extension Preserves Well-Quasi-Orders›

theory Wqo_Multiset
imports
Multiset_Extension
Well_Quasi_Orders
begin

lemma list_emb_imp_reflclp_mulex_on:
assumes "xs ∈ lists A" and "ys ∈ lists A"
and "list_emb P xs ys"
shows "(mulex_on P A)⇧=⇧= (mset xs) (mset ys)"
using assms(3, 1, 2)
proof (induct)
case (list_emb_Nil ys)
then show ?case
by (cases ys) (auto intro!: empty_mulex_on simp: multisets_def)
next
case (list_emb_Cons xs ys y)
then show ?case by (auto intro!: mulex_on_self_add_singleton_right simp: multisets_def)
next
case (list_emb_Cons2 x y xs ys)
then show ?case
simp: multisets_def)
qed

text ‹The (reflexive closure of the) multiset extension of an almost-full relation
is almost-full.›
lemma almost_full_on_multisets:
assumes "almost_full_on P A"
shows "almost_full_on (mulex_on P A)⇧=⇧= (multisets A)"
proof -
let ?P = "(mulex_on P A)⇧=⇧="
from almost_full_on_hom [OF _ almost_full_on_lists, of A P ?P mset,
OF list_emb_imp_reflclp_mulex_on, simplified]
show ?thesis using assms by blast
qed

lemma wqo_on_multisets:
assumes "wqo_on P A"
shows "wqo_on (mulex_on P A)⇧=⇧= (multisets A)"
proof
from transp_on_mulex_on [of P A "multisets A"]
show "transp_on (mulex_on P A)⇧=⇧= (multisets A)"
unfolding transp_on_def by blast
next
from almost_full_on_multisets [OF assms [THEN wqo_on_imp_almost_full_on]]
show "almost_full_on (mulex_on P A)⇧=⇧= (multisets A)" .
qed

end

`