Theory Minimal_Elements

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

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