(* 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