Theory Well_Quasi_Orders.Minimal_Elements
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