Theory Least_Enum

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

section ‹Enumerations of Well-Ordered Sets in Increasing Order›

theory Least_Enum
imports Main
begin
  
locale infinitely_many1 =
  fixes P :: "'a :: wellorder ⇒ bool"
  assumes infm: "∀i. ∃j>i. P j"
begin

text ‹
  Enumerate the elements of a well-ordered infinite set in increasing order.
›
fun enum :: "nat ⇒ 'a" where
  "enum 0 = (LEAST n. P n)" |
  "enum (Suc i) = (LEAST n. n > enum i ∧ P n)"

lemma enum_mono:
  shows "enum i < enum (Suc i)"
  using infm by (cases i, auto) (metis (lifting) LeastI)+

lemma enum_less:
  "i < j ⟹ enum i < enum j"
  using enum_mono by (metis lift_Suc_mono_less)

lemma enum_P:
  shows "P (enum i)"
  using infm by (cases i, auto) (metis (lifting) LeastI)+

end

locale infinitely_many2 =
  fixes P :: "'a :: wellorder ⇒ 'a ⇒ bool"
    and N :: "'a"
  assumes infm: "∀i≥N. ∃j>i. P i j"
begin

text ‹
  Enumerate the elements of a well-ordered infinite set that form a chain w.r.t.\ a given predicate
  @{term P} starting from a given index @{term N} in increasing order.
›
fun enumchain :: "nat ⇒ 'a" where
  "enumchain 0 = N" |
  "enumchain (Suc n) = (LEAST m. m > enumchain n ∧ P (enumchain n) m)"

lemma enumchain_mono:
  shows "N ≤ enumchain i ∧ enumchain i < enumchain (Suc i)"
proof (induct i)
  case 0
  have "enumchain 0 ≥ N" by simp
  moreover then have "∃m>enumchain 0. P (enumchain 0) m" using infm by blast
  ultimately show ?case by auto (metis (lifting) LeastI)
next
  case (Suc i)
  then have "N ≤ enumchain (Suc i)" by auto
  moreover then have "∃m>enumchain (Suc i). P (enumchain (Suc i)) m" using infm by blast
  ultimately show ?case by (auto) (metis (lifting) LeastI)
qed

lemma enumchain_chain:
  shows "P (enumchain i) (enumchain (Suc i))"
proof (cases i)
  case 0
  moreover have "∃m>enumchain 0. P (enumchain 0) m" using infm by auto
  ultimately show ?thesis by auto (metis (lifting) LeastI)
next
  case (Suc i)
  moreover have "enumchain (Suc i) > N" using enumchain_mono by (metis le_less_trans)
  moreover then have "∃m>enumchain (Suc i). P (enumchain (Suc i)) m" using infm by auto
  ultimately show ?thesis by (auto) (metis (lifting) LeastI)
qed

end

end