# Theory OrdinalDef

```(*  Title:       Countable Ordinals

Author:      Brian Huffman, 2005
Maintainer:  Brian Huffman <brianh at cse.ogi.edu>
*)

section ‹Definition of Ordinals›

theory OrdinalDef
imports Main
begin

subsection ‹Preliminary datatype for ordinals›

datatype ord0 = ord0_Zero | ord0_Lim "nat ⇒ ord0"

text ‹subterm ordering on ord0›

definition
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)
qed

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)
qed

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"
qed

text ‹ordering on ord0›

instantiation ord0 :: ord
begin

definition
ord0_less_def: "x < y ⟷ (x,y) ∈ ord0_leq O ord0_prec⇧+"

definition
ord0_le_def:   "x ≤ y ⟷ (x,y) ∈ ord0_leq"

instance ..

end

lemma ord0_order_refl[simp]: "(x::ord0) ≤ x"

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 old.prod.case ord0_leI ord0_le_less_trans ord0_less_imp_le)
qed
then show ?case
using "1" by blast
qed
then show ?thesis
by simp
qed

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")
proof
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
qed

subsection ‹Ordinal type›

definition
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
begin

definition
ordinal_less_def: "x < y ⟷ (∀a∈Rep_ordinal x. ∀b∈Rep_ordinal y. a < b)"

definition
ordinal_le_def: "x ≤ y ⟷ (∀a∈Rep_ordinal x. ∀b∈Rep_ordinal y. a ≤ b)"

instance ..

end

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

lemma mem_ord0rel_Image [simp, intro!]: "x ∈ ord0rel `` {x}"

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])
done

lemma Abs_ordinal_le[simp]:
"Abs_ordinal (ord0rel `` {x}) ≤ Abs_ordinal (ord0rel `` {y}) ⟷ (x ≤ y)" (is "?L=?R")
proof
show "?L ⟹ ?R"
using Rep_Abs_ord0rel ordinal_le_def by blast
next
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
qed

lemma Abs_ordinal_less[simp]:
"Abs_ordinal (ord0rel `` {x}) < Abs_ordinal (ord0rel `` {y}) ⟷ (x < y)" (is "?L=?R")
proof
show "?L ⟹ ?R"
using Rep_Abs_ord0rel ordinal_less_def by blast
next
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
qed

instance ordinal :: linorder
proof
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)
qed

instance ordinal :: wellorder
proof
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
qed
qed

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

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

subsection ‹Induction over ordinals›

text "zero and strict limits"

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

definition
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"

lemma ord0_precD: "(x,y) ∈ ord0_prec ⟹ ∃f n. x = f n ∧ y = ord0_Lim f"

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 "x≤y" "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)
qed

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"

lemma Abs_ordinal_oStrictLimit:
"Abs_ordinal (ord0rel `` {ord0_Lim f})
= oStrictLimit (λn. Abs_ordinal (ord0rel `` {f n}))"
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
next
case (ord0_Lim x)
then show ?case
qed
then show ?thesis
qed

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)
qed

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
qed
then show ?thesis
using assms linorder_not_le by blast
qed

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

end
```