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