Theory OrdinalDef

(*  Title:       Countable Ordinals

    Author:      Brian Huffman, 2005
    Maintainer:  Brian Huffman <brianh at>

section ‹Definition of Ordinals›

theory OrdinalDef
  imports Main

subsection ‹Preliminary datatype for ordinals›

datatype ord0 = ord0_Zero | ord0_Lim "nat  ord0"

text ‹subterm ordering on ord0›

  ord0_prec :: "(ord0 × ord0) set" where
  "ord0_prec = (f i. {(f i, ord0_Lim f)})"

lemma wf_ord0_prec: "wf ord0_prec"
proof -
  have "x. (y. (y, x)  ord0_prec  P y)  P x  P a" for P a
    unfolding ord0_prec_def by (induction a) blast+
  then show ?thesis
    by (metis wfUNIVI)

lemmas ord0_prec_induct = wf_induct[OF wf_trancl[OF wf_ord0_prec]]

text ‹less-than-or-equal ordering on ord0›

inductive_set ord0_leq :: "(ord0 × ord0) set" where
  "a. (a,x)  ord0_prec+  (b. (b,y)  ord0_prec+  (a,b)  ord0_leq)
   (x,y)  ord0_leq"

lemma ord0_leqI:
  "a. (a,x)  ord0_prec+  (a,y)  ord0_leq O ord0_prec+
  (x,y)  ord0_leq"
  by (meson ord0_leq.intros relcomp.cases)

lemma ord0_leqD:
  "(x,y)  ord0_leq; (a,x)  ord0_prec+  (a,y)  ord0_leq O ord0_prec+"
  by (ind_cases "(x,y)  ord0_leq", auto)

lemma ord0_leq_refl: "(x, x)  ord0_leq"
  by (rule ord0_prec_induct, rule ord0_leqI, auto)

lemma ord0_leq_trans:
  "(x,y)  ord0_leq  (y,z)  ord0_leq  (x,z)  ord0_leq"
proof (induction x arbitrary: y z rule: ord0_prec_induct)
  case (1 x)
  then show ?case
    by (meson ord0_leq.cases ord0_leq.intros)

lemma wf_ord0_leq: "wf (ord0_leq O ord0_prec+)"
  unfolding wf_def
proof clarify
  fix P x
  assume *: "x. (y. (y, x)  ord0_leq O ord0_prec+  P y)  P x"
  have "z. (z, x)  ord0_leq  P z" 
    by (rule ord0_prec_induct) (meson * ord0_leq.cases ord0_leq_trans relcomp.cases)
  then show "P x"
    by (simp add: ord0_leq_refl)

text ‹ordering on ord0›

instantiation ord0 :: ord

  ord0_less_def: "x < y  (x,y)  ord0_leq O ord0_prec+"

  ord0_le_def:   "x  y  (x,y)  ord0_leq"

instance ..


lemma ord0_order_refl[simp]: "(x::ord0)  x"
  by (simp add: ord0_le_def ord0_leq_refl)

lemma ord0_order_trans: "(x::ord0)  y; y  z  x  z"
  using ord0_le_def ord0_leq_trans by blast

lemma ord0_wf: "wf {(x,y::ord0). x < y}"
  using ord0_less_def wf_ord0_leq by auto

lemmas ord0_less_induct = wf_induct[OF ord0_wf]

lemma ord0_leI: "a::ord0. a < x  a < y  x  y"
  by (meson ord0_le_def ord0_leqD ord0_leqI ord0_leq_refl ord0_less_def)

lemma ord0_less_le_trans: "(x::ord0) < y; y  z  x < z"
  by (meson ord0_le_def ord0_leq.cases ord0_leq_trans ord0_less_def relcomp.intros relcompEpair)

lemma ord0_le_less_trans:
  "(x::ord0)  y; y < z  x < z"
  by (meson ord0_le_def ord0_leq_trans ord0_less_def relcomp.cases relcomp.intros)

lemma rev_ord0_le_less_trans:
  "(y::ord0) < z; x  y  x < z"
  by (rule ord0_le_less_trans)

lemma ord0_less_trans: "(x::ord0) < y; y < z  x < z"
  unfolding ord0_less_def 
  by (meson ord0_leq.cases relcomp.cases relcompI[OF ord0_leq_trans trancl_trans])

lemma ord0_less_imp_le: "(x::ord0) < y  x  y"
  using ord0_leI ord0_less_trans by blast

lemma ord0_linear_lemma:
  fixes m :: ord0 and n :: ord0
  shows "m < n  n < m  (m  n  n  m)"
proof -
  have "m < n  n < m  m  n  n  m" for m
  proof (induction n arbitrary: m rule: ord0_less_induct)
    case (1 n)
    have "y. (y, n)  {(x, y). x < y}  (x. x < y  y < x  x  y  y  x)  
           m < n  n < m  m  n  n  m"
    proof (induction m rule: ord0_less_induct)
      case (1 x)
      then show ?case
        by (smt (verit, best) mem_Collect_eq ord0_leI ord0_le_less_trans ord0_less_imp_le)
    then show ?case
      using "1" by blast
  then show ?thesis
    by simp

lemma ord0_linear: "(x::ord0)  y  y  x"
  using ord0_less_imp_le ord0_linear_lemma by blast

lemma ord0_order_less_le: "(x::ord0) < y  (x  y  ¬ y  x)" (is "?L=?R")
  show "?L  ?R"
    by (metis ord0_less_def ord0_less_imp_le ord0_less_le_trans wf_not_refl wf_ord0_leq)
  show "?R  ?L"
  using ord0_less_imp_le ord0_linear_lemma by blast

subsection ‹Ordinal type›

  ord0rel :: "(ord0 × ord0) set" where
  "ord0rel = {(x,y). x  y  y  x}"

typedef ordinal = "(UNIV::ord0 set) // ord0rel"
  by (unfold quotient_def, auto)

theorem Abs_ordinal_cases2 [case_names Abs_ordinal, cases type: ordinal]:
  "(z. x = Abs_ordinal (ord0rel `` {z})  P)  P"
  by (cases x, auto simp add: quotient_def)

instantiation ordinal :: ord

  ordinal_less_def: "x < y  (aRep_ordinal x. bRep_ordinal y. a < b)"

  ordinal_le_def: "x  y  (aRep_ordinal x. bRep_ordinal y. a  b)"

instance ..


lemma Rep_Abs_ord0rel [simp]:
  "Rep_ordinal (Abs_ordinal (ord0rel `` {x})) = (ord0rel `` {x})"
  by (simp add: Abs_ordinal_inverse quotientI)

lemma mem_ord0rel_Image [simp, intro!]: "x  ord0rel `` {x}"
  by (simp add: ord0rel_def)

lemma equiv_ord0rel: "equiv UNIV ord0rel"
  unfolding equiv_def refl_on_def sym_def trans_def ord0rel_def
  by (auto elim: ord0_order_trans)

lemma Abs_ordinal_eq[simp]:
  "(Abs_ordinal (ord0rel `` {x}) = Abs_ordinal (ord0rel `` {y})) = (x  y  y  x)"
  apply (simp add: Abs_ordinal_inject quotientI eq_equiv_class_iff[OF equiv_ord0rel])
  apply (simp add: ord0rel_def)

lemma Abs_ordinal_le[simp]:
  "Abs_ordinal (ord0rel `` {x})  Abs_ordinal (ord0rel `` {y})  (x  y)" (is "?L=?R")
  show "?L  ?R"
    using Rep_Abs_ord0rel ordinal_le_def by blast
  assume ?R
  then have "a b. (x, a)  ord0rel; (y, b)  ord0rel  a  b"
    unfolding ord0rel_def by (blast intro: ord0_order_trans)
  then show ?L
    by (auto simp add: ordinal_le_def)

lemma Abs_ordinal_less[simp]:
  "Abs_ordinal (ord0rel `` {x}) < Abs_ordinal (ord0rel `` {y})  (x < y)" (is "?L=?R")
  show "?L  ?R"
    using Rep_Abs_ord0rel ordinal_less_def by blast
  assume ?R
  then have "a b. (x, a)  ord0rel; (y, b)  ord0rel  a < b"
    unfolding ord0rel_def
    by (blast intro: ord0_le_less_trans ord0_less_le_trans)
  then show ?L
    by (auto simp add: ordinal_less_def)

instance ordinal :: linorder
  show "(x::ordinal)  x" for x
    by (cases x, simp)
  show "((x::ordinal) < y) = (x  y  ¬ y  x)" for x y
    by (cases x, cases y, auto simp add: ord0_order_less_le)
  show "(x::ordinal)  y  y  z  x  z" for x y z
    by (cases x, cases y, cases z, auto elim: ord0_order_trans)
  show "(x::ordinal)  y  y  x  x = y" for x y
    by (cases x, cases y, simp)
  show "(x::ordinal)  y  y  x" for x y
    by (cases x, cases y, simp add: ord0_linear)

instance ordinal :: wellorder
  show "P a" if "(x::ordinal. (y. y < x  P y)  P x)" for P a
  proof (rule Abs_ordinal_cases2)
    fix z
    assume a: "a = Abs_ordinal (ord0rel `` {z})"
    have "P (Abs_ordinal (ord0rel `` {z}))"
      using that
      apply (rule ord0_less_induct)
      by (metis Abs_ordinal_cases2 Abs_ordinal_less CollectI case_prodI)
    with a show "P a" by simp

lemma ordinal_linear: "(x::ordinal)  y  y  x"
  by auto

lemma ordinal_wf: "wf {(x,y::ordinal). x < y}"
  by (simp add: wf)

subsection ‹Induction over ordinals›

text "zero and strict limits"

  oZero :: "ordinal" where
  "oZero = Abs_ordinal (ord0rel `` {ord0_Zero})"

  oStrictLimit :: "(nat  ordinal)  ordinal" where
  "oStrictLimit f = Abs_ordinal
      (ord0rel `` {ord0_Lim (λn. SOME x. x  Rep_ordinal (f n))})"

text "induction over ordinals"

lemma ord0relD: "(x,y)  ord0rel  x  y  y  x"
  by (simp add: ord0rel_def)

lemma ord0_precD: "(x,y)  ord0_prec  f n. x = f n  y = ord0_Lim f"
  by (simp add: ord0_prec_def)

lemma less_ord0_LimI: "f n < ord0_Lim f"
  using ord0_leq_refl ord0_less_def ord0_prec_def by fastforce

lemma less_ord0_LimD: 
  assumes "x < ord0_Lim f" shows "n. x  f n"
proof -
  obtain y where "xy" "y < ord0_Lim f"
    using assms ord0_linear by auto
  then consider "(y, ord0_Lim f)  ord0_prec" | z where "y  z" "(z, ord0_Lim f)  ord0_prec"
    apply (clarsimp simp add: ord0_less_def ord0_le_def)
    by (metis ord0_less_def ord0_less_imp_le relcomp.relcompI that(2) tranclE)
  then show ?thesis
    by (metis x  y ord0.inject ord0_order_trans ord0_precD)
lemma some_ord0rel: "(x, SOME y. (x,y)  ord0rel)  ord0rel"
  by (rule_tac x=x in someI, simp add: ord0rel_def)

lemma ord0_Lim_le: "n. f n  g n  ord0_Lim f  ord0_Lim g"
  by (metis less_ord0_LimD less_ord0_LimI ord0_le_less_trans ord0_linear ord0_order_less_le)

lemma ord0_Lim_ord0rel:
  "n. (f n, g n)  ord0rel  (ord0_Lim f, ord0_Lim g)  ord0rel"
  by (simp add: ord0rel_def ord0_Lim_le)

lemma Abs_ordinal_oStrictLimit:
  "Abs_ordinal (ord0rel `` {ord0_Lim f})
  = oStrictLimit (λn. Abs_ordinal (ord0rel `` {f n}))"
  apply (simp add: oStrictLimit_def)
  using ord0_Lim_le ord0relD some_ord0rel by presburger

lemma oStrictLimit_induct:
  assumes base: "P oZero"
  assumes step: "f. n. P (f n)  P (oStrictLimit f)"
  shows "P a"
proof -
  obtain z where z: "a = Abs_ordinal (ord0rel `` {z})"
    using Abs_ordinal_cases2 by auto
  have "P (Abs_ordinal (ord0rel `` {z}))"
  proof (induction z)
    case ord0_Zero
    with base oZero_def show ?case by auto
    case (ord0_Lim x)
    then show ?case
      by (simp add: Abs_ordinal_oStrictLimit local.step)
  then show ?thesis
    by (simp add: z)

text "order properties of 0 and strict limits"

lemma oZero_least: "oZero  x"
proof -
  have "x = Abs_ordinal (ord0rel `` {z})  ord0_Zero  z" for z
  proof (induction z arbitrary: x)
    case (ord0_Lim u)
    then show ?case
      by (meson less_ord0_LimI ord0_le_less_trans ord0_less_imp_le rangeI) 
  qed auto
  then show ?thesis
    by (metis Abs_ordinal_cases2 Abs_ordinal_le oZero_def)

lemma oStrictLimit_ub: "f n < oStrictLimit f"
  apply (cases "f n", simp add: oStrictLimit_def)
  apply (rule_tac y="SOME x. x  Rep_ordinal (f n)" in ord0_le_less_trans)
  apply (metis (no_types) Image_singleton_iff Rep_Abs_ord0rel empty_iff mem_ord0rel_Image ord0relD some_in_eq)
  by (meson less_ord0_LimI)

lemma oStrictLimit_lub: 
  assumes "n. f n < x" shows "oStrictLimit f  x"
proof -
  have "n. x  f n" if x: "x < oStrictLimit f"
  proof -
    obtain z where z: "x = Abs_ordinal (ord0rel `` {z})" 
                      "z < ord0_Lim (λn. SOME x. x  Rep_ordinal (f n))"
      using less_ord0_LimI x unfolding oStrictLimit_def
      by (metis Abs_ordinal_cases2 Abs_ordinal_less)
    then obtain n where "z  (SOME x. x  Rep_ordinal (f n))"
      using less_ord0_LimD by blast
    then have "Abs_ordinal (ord0rel `` {z})  f n"
      apply (rule_tac x="f n" in Abs_ordinal_cases2)
      using ord0_order_trans ord0relD some_ord0rel by auto
    then show ?thesis
      using x = Abs_ordinal (ord0rel `` {z}) by auto
  then show ?thesis
    using assms linorder_not_le by blast

lemma less_oStrictLimitD: "x < oStrictLimit f  n. x  f n"
  by (metis leD leI oStrictLimit_lub)