Theory Well_Quasi_Orders.Minimal_Bad_Sequences

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

section ‹Constructing Minimal Bad Sequences›

theory Minimal_Bad_Sequences
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}.
›
definition "BAD P = {f ∈ SEQ A. bad P f}"

lemma BAD_iff [iff]:
  "f ∈ BAD P ⟷ (∀i. f i ∈ A) ∧ bad P f"
  by (auto simp: BAD_def)

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)"

lemma eq_upto_BAD_mem:
  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"
  assumes BAD_ex: "h ∈ BAD P"
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.
›
lemma eq_upto_BAD_non_empty:
  "eq_upto (BAD P) lb i ≠ {}"
using eq_upto_lexmin_non_empty [of "BAD P"] and BAD_ex by auto

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.
›
lemma lb_BAD:
  "lb ∈ BAD P"
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