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: "iN. 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