# Theory Ordinal

```chapter ‹Ordinals, Sequences and Ordinal Recursion›

theory Ordinal imports HF
begin

section ‹Ordinals›

subsection ‹Basic Definitions›

text ‹Definition 2.1. We say that x is transitive if every element of x is a subset of x.›
definition
Transset  :: "hf ⇒ bool"  where
"Transset(x) ≡ ∀y. y ❙∈ x ⟶ y ≤ x"

lemma Transset_sup: "Transset x ⟹ Transset y ⟹ Transset (x ⊔ y)"
by (auto simp: Transset_def)

lemma Transset_inf: "Transset x ⟹ Transset y ⟹ Transset (x ⊓ y)"
by (auto simp: Transset_def)

lemma Transset_hinsert: "Transset x ⟹ y ≤ x ⟹ Transset (x ◃ y)"
by (auto simp: Transset_def)

text ‹In HF, the ordinals are simply the natural numbers. But the definitions are the same
as for transfinite ordinals.›
definition
Ord  :: "hf ⇒ bool"  where
"Ord(k)      ≡ Transset(k) ∧ (∀x ❙∈ k. Transset(x))"

subsection ‹Definition 2.2 (Successor).›
definition
succ  :: "hf ⇒ hf"  where
"succ(x)      ≡ hinsert x x"

lemma succ_iff [simp]: "x ❙∈ succ y ⟷ x=y ∨ x ❙∈ y"

lemma succ_ne_self [simp]: "i ≠ succ i"
by (metis hmem_ne succ_iff)

lemma succ_notin_self: "succ i ❙∉ i"
by (metis hmem_ne succ_iff)

lemma succE [elim?]: assumes "x ❙∈ succ y" obtains "x=y" | "x ❙∈ y"
by (metis assms succ_iff)

lemma hmem_succ_ne: "succ x ❙∈ y ⟹ x ≠ y"
by (metis hmem_not_refl succ_iff)

lemma hball_succ [simp]: "(∀x ❙∈ succ k. P x) ⟷ P k ∧ (∀x ❙∈ k. P x)"
by (auto simp: HBall_def)

lemma hbex_succ [simp]: "(∃x ❙∈ succ k. P x) ⟷ P k ∨ (∃x ❙∈ k. P x)"
by (auto simp: HBex_def)

lemma One_hf_eq_succ: "1 = succ 0"
by (metis One_hf_def succ_def)

lemma zero_hmem_one [iff]: "x ❙∈ 1 ⟷ x = 0"
by (metis One_hf_eq_succ hmem_hempty succ_iff)

lemma hball_One [simp]: "(∀x❙∈1. P x) = P 0"

lemma hbex_One [simp]: "(∃x❙∈1. P x) = P 0"

lemma hpair_neq_succ [simp]: "⟨x,y⟩ ≠ succ k"
by (auto simp: succ_def hpair_def) (metis hemptyE hmem_hinsert hmem_ne)

lemma succ_neq_hpair [simp]: "succ k ≠ ⟨x,y⟩ "
by (metis hpair_neq_succ)

lemma hpair_neq_one [simp]: "⟨x,y⟩ ≠ 1"
by (metis One_hf_eq_succ hpair_neq_succ)

lemma one_neq_hpair [simp]: "1 ≠ ⟨x,y⟩"
by (metis hpair_neq_one)

lemma hmem_succ_self [simp]: "k ❙∈ succ k"
by (metis succ_iff)

lemma hmem_succ: "l ❙∈ k ⟹ l ❙∈ succ k"
by (metis succ_iff)

text ‹Theorem 2.3.›
lemma Ord_0 [iff]: "Ord 0"

lemma Ord_succ: "Ord(k) ⟹ Ord(succ(k))"
by (simp add: Ord_def Transset_def succ_def less_eq_insert2_iff HBall_def)

lemma Ord_1 [iff]: "Ord 1"
by (metis One_hf_def Ord_0 Ord_succ succ_def)

lemma OrdmemD: "Ord(k) ⟹ j ❙∈ k ⟹ j ≤ k"
by (simp add: Ord_def Transset_def HBall_def)

lemma Ord_trans: "⟦ i❙∈j;  j❙∈k;  Ord(k) ⟧  ⟹ i❙∈k"
by (blast dest: OrdmemD)

lemma hmem_0_Ord:
assumes k: "Ord(k)" and knz: "k ≠ 0" shows "0 ❙∈ k"
by (metis foundation [OF knz] Ord_trans hempty_iff hinter_iff k)

lemma Ord_in_Ord: "⟦ Ord(k);  m ❙∈ k ⟧  ⟹ Ord(m)"
by (auto simp: Ord_def Transset_def)

subsection ‹Induction, Linearity, etc.›

lemma Ord_induct [consumes 1, case_names step]:
assumes k: "Ord(k)"
and step: "⋀x.⟦ Ord(x);  ⋀y. y ❙∈ x ⟹ P(y) ⟧  ⟹ P(x)"
shows "P(k)"
proof -
have "∀m ❙∈ k. Ord(m) ⟶ P(m)"
proof (induct k rule: hf_induct)
case 0 thus ?case  by simp
next
case (hinsert a b)
thus ?case
by (auto intro: Ord_in_Ord step)
qed
thus ?thesis using k
by (auto intro: Ord_in_Ord step)
qed

text ‹Theorem 2.4 (Comparability of ordinals).›
lemma Ord_linear: "Ord(k) ⟹ Ord(l) ⟹ k❙∈l ∨ k=l ∨ l❙∈k"
proof (induct k arbitrary: l rule: Ord_induct)
case (step k)
note step_k = step
show ?case using ‹Ord(l)›
proof (induct l rule: Ord_induct)
case (step l)
thus ?case using step_k
by (metis Ord_trans hf_equalityI)
qed
qed

text ‹The trichotomy law for ordinals›
lemma Ord_linear_lt:
assumes o: "Ord(k)" "Ord(l)"
obtains (lt) "k❙∈l" | (eq) "k=l" | (gt) "l❙∈k"
by (metis Ord_linear o)

lemma Ord_linear2:
assumes o: "Ord(k)" "Ord(l)"
obtains (lt) "k❙∈l" | (ge) "l ≤ k"
by (metis Ord_linear OrdmemD order_eq_refl o)

lemma Ord_linear_le:
assumes o: "Ord(k)" "Ord(l)"
obtains (le) "k ≤ l" | (ge) "l ≤ k"
by (metis Ord_linear2 OrdmemD o)

lemma hunion_less_iff [simp]: "⟦Ord i; Ord j⟧ ⟹ i ⊔ j < k ⟷ i<k ∧ j<k"
by (metis Ord_linear_le le_iff_sup sup.order_iff sup.strict_boundedE)

text ‹Theorem 2.5›
lemma Ord_mem_iff_lt: "Ord(k) ⟹ Ord(l) ⟹ k❙∈l ⟷ k < l"
by (metis Ord_linear OrdmemD hmem_not_refl less_hf_def less_le_not_le)

lemma le_succE: "succ i ≤ succ j ⟹ i ≤ j"
by (simp add: less_eq_hf_def) (metis hmem_not_sym)

lemma le_succ_iff: "Ord i ⟹ Ord j ⟹ succ i ≤ succ j ⟷ i ≤ j"
by (metis Ord_linear_le Ord_succ le_succE order_antisym)

lemma succ_inject_iff [iff]: "succ i = succ j ⟷ i = j"
by (metis succ_def hmem_hinsert hmem_not_sym)

lemma mem_succ_iff [simp]: "Ord j ⟹ succ i ❙∈ succ j ⟷ i ❙∈ j"
by (metis Ord_in_Ord Ord_mem_iff_lt Ord_succ succ_def less_eq_insert1_iff less_hf_def succ_iff)

lemma Ord_mem_succ_cases:
assumes "Ord(k)" "l ❙∈ k"
shows "succ l = k ∨ succ l ❙∈ k"
by (metis assms mem_succ_iff succ_iff)

subsection ‹Supremum and Infimum›

lemma Ord_Union [intro,simp]: "⟦ ⋀i. i❙∈A ⟹ Ord(i) ⟧  ⟹ Ord(⨆ A)"
by (auto simp: Ord_def Transset_def) blast

lemma Ord_Inter [intro,simp]:
assumes "⋀i. i❙∈A ⟹ Ord(i)" shows "Ord(⨅ A)"
proof (cases "A=0")
case False
with assms show ?thesis
by (fastforce simp add: Ord_def Transset_def)
qed auto

text ‹Theorem 2.7. Every set x of ordinals is ordered by the binary relation <.
Moreover if x = 0 then x has a smallest and a largest element.›

lemma hmem_Sup_Ords: "⟦A≠0; ⋀i. i❙∈A ⟹ Ord(i)⟧ ⟹ ⨆A ❙∈ A"
proof (induction A rule: hf_induct)
case 0 thus ?case  by simp
next
case (hinsert x A)
show ?case
proof (cases A rule: hf_cases)
case 0 thus ?thesis by simp
next
case (hinsert y A')
hence UA: "⨆A ❙∈ A"
by (metis hinsert.IH(2) hinsert.prems(2) hinsert_nonempty hmem_hinsert)
hence "⨆A ≤ x ∨ x ≤ ⨆A"
by (metis Ord_linear2 OrdmemD hinsert.prems(2) hmem_hinsert)
thus ?thesis
by (metis HUnion_hinsert UA le_iff_sup less_eq_insert1_iff order_refl sup.commute)
qed
qed

lemma hmem_Inf_Ords: "⟦A≠0; ⋀i. i❙∈A ⟹ Ord(i)⟧ ⟹ ⨅A ❙∈ A"
proof (induction A rule: hf_induct)
case 0 thus ?case  by simp
next
case (hinsert x A)
show ?case
proof (cases A rule: hf_cases)
case 0 thus ?thesis by auto
next
case (hinsert y A')
hence IA: "⨅A ❙∈ A"
by (metis hinsert.IH(2) hinsert.prems(2) hinsert_nonempty hmem_hinsert)
hence "⨅A ≤ x ∨ x ≤ ⨅A"
by (metis Ord_linear2 OrdmemD hinsert.prems(2) hmem_hinsert)
thus ?thesis
by (metis HInter_hinsert IA hmem_hempty hmem_hinsert inf_absorb2 le_iff_inf)
qed
qed

lemma Ord_pred: "⟦Ord(k); k ≠ 0⟧ ⟹ succ(⨆k) = k"
by (metis (full_types) HUnion_iff Ord_in_Ord Ord_mem_succ_cases hmem_Sup_Ords hmem_ne succ_iff)

lemma Ord_cases [cases type: hf, case_names 0 succ]:
assumes Ok: "Ord(k)"
obtains "k = 0" | l where "Ord l" "succ l = k"
by (metis Ok Ord_in_Ord Ord_pred succ_iff)

lemma Ord_induct2 [consumes 1, case_names 0 succ, induct type: hf]:
assumes k: "Ord(k)"
and P: "P 0" "⋀k. Ord k ⟹ P k ⟹ P (succ k)"
shows "P k"
using k
proof (induction k rule: Ord_induct)
case (step k) thus ?case
by (metis Ord_cases P hmem_succ_self)
qed

lemma Ord_succ_iff [iff]: "Ord (succ k) = Ord k"
by (metis Ord_in_Ord Ord_succ less_eq_insert1_iff order_refl succ_def)

lemma [simp]: "succ k ≠ 0"
by (metis hinsert_nonempty succ_def)

lemma Ord_Sup_succ_eq [simp]: "Ord k ⟹ ⨆(succ k) = k"
by (metis Ord_pred Ord_succ_iff succ_inject_iff hinsert_nonempty succ_def)

lemma Ord_lt_succ_iff_le: "Ord k ⟹ Ord l ⟹ k < succ l ⟷ k ≤ l"
by (metis Ord_mem_iff_lt Ord_succ_iff less_le_not_le order_eq_iff succ_iff)

lemma zero_in_Ord: "Ord k ⟹ k=0 ∨ 0 ❙∈ k"
by (induct k) auto

lemma hpair_neq_Ord: "Ord k ⟹ ⟨x,y⟩ ≠ k"
by (cases k) auto

lemma hpair_neq_Ord': assumes k: "Ord k" shows "k ≠ ⟨x,y⟩"
by (metis k hpair_neq_Ord)

lemma Not_Ord_hpair [iff]: "¬ Ord ⟨x,y⟩"
by (metis hpair_neq_Ord)

lemma is_hpair [simp]: "is_hpair ⟨x,y⟩"

lemma Ord_not_hpair: "Ord x ⟹ ¬ is_hpair x"
by (metis Not_Ord_hpair is_hpair_def)

lemma zero_in_succ [simp,intro]: "Ord i ⟹ 0 ❙∈ succ i"
by (metis succ_iff zero_in_Ord)

subsection ‹Converting Between Ordinals and Natural Numbers›

fun ord_of :: "nat ⇒ hf"
where
"ord_of 0 = 0"
| "ord_of (Suc k) = succ (ord_of k)"

lemma Ord_ord_of [simp]: "Ord (ord_of k)"
by (induct k, auto)

lemma ord_of_inject [iff]: "ord_of i = ord_of j ⟷ i=j"
proof (induct i arbitrary: j)
case 0 show ?case
by (metis Zero_neq_Suc hempty_iff hmem_succ_self ord_of.elims)
next
case (Suc i) show ?case
by (cases j) (auto simp: Suc)
qed

lemma ord_of_minus_1: "n > 0 ⟹ ord_of n = succ (ord_of (n - 1))"
by (metis Suc_diff_1 ord_of.simps(2))

definition nat_of_ord :: "hf ⇒ nat"
where "nat_of_ord x = (THE n. x = ord_of n)"

lemma nat_of_ord_ord_of [simp]: "nat_of_ord (ord_of n) = n"
by (auto simp: nat_of_ord_def)

lemma nat_of_ord_0 [simp]: "nat_of_ord 0 = 0"
by (metis (mono_tags) nat_of_ord_ord_of ord_of.simps(1))

lemma ord_of_nat_of_ord [simp]: "Ord x ⟹ ord_of (nat_of_ord x) = x"
proof (induction x rule: Ord_induct2)
case (succ k)
then show ?case
by (metis nat_of_ord_ord_of ord_of.simps(2))
qed auto

lemma nat_of_ord_inject: "Ord x ⟹ Ord y ⟹ nat_of_ord x = nat_of_ord y ⟷ x = y"
by (metis ord_of_nat_of_ord)

lemma nat_of_ord_succ [simp]: "Ord x ⟹ nat_of_ord (succ x) = Suc (nat_of_ord x)"
by (metis nat_of_ord_ord_of ord_of.simps(2) ord_of_nat_of_ord)

lemma inj_ord_of: "inj_on ord_of A"

lemma hfset_ord_of: "hfset (ord_of n) = ord_of ` {0..<n}"
by (induct n) (auto simp: hfset_hinsert succ_def)

lemma bij_betw_ord_of: "bij_betw ord_of {0..<n} (hfset (ord_of n))"
by (simp add: bij_betw_def inj_ord_of hfset_ord_of)

lemma bij_betw_ord_ofI:
"bij_betw h A {0..<n} ⟹ bij_betw (ord_of ∘ h) A (hfset (ord_of n))"
by (blast intro: bij_betw_ord_of bij_betw_trans)

section ‹Sequences and Ordinal Recursion›

text ‹Definition 3.2 (Sequence).›

definition Seq :: "hf ⇒ hf ⇒ bool"
where "Seq s k ⟷ hrelation s ∧ hfunction s ∧ k ≤ hdomain s"

lemma Seq_0 [iff]: "Seq 0 0"
by (auto simp: Seq_def hrelation_def hfunction_def)

lemma Seq_succ_D: "Seq s (succ k) ⟹ Seq s k"

lemma Seq_Ord_D: "Seq s k ⟹ l ❙∈ k ⟹ Ord k ⟹ Seq s l"
by (auto simp: Seq_def intro: Ord_trans)

lemma Seq_restr: "Seq s (succ k) ⟹ Seq (hrestrict s k) k"
by (simp add: Seq_def hfunction_restr succ_def)

lemma Seq_Ord_restr: "⟦Seq s k; l ❙∈ k; Ord k⟧ ⟹ Seq (hrestrict s l) l"
by (auto simp: Seq_def hfunction_restr intro: Ord_trans)

lemma Seq_ins: "⟦Seq s k; k ❙∉ hdomain s⟧ ⟹ Seq (s ◃ ⟨k, y⟩) (succ k)"
by (auto simp: Seq_def hrelation_def succ_def hfunction_def hdomainI)

definition insf :: "hf ⇒ hf ⇒ hf ⇒ hf"
where "insf s k y ≡ nonrestrict s ⦃k⦄ ◃ ⟨k, y⟩"

lemma hrelation_insf: "hrelation s ⟹ hrelation (insf s k y)"
by (simp add: hrelation_def insf_def nonrestrict_def)

lemma hfunction_insf: "hfunction s ⟹ hfunction (insf s k y)"
by (auto simp: insf_def hfunction_def nonrestrict_def hmem_not_refl)

lemma hdomain_insf: "k ≤ hdomain s ⟹ succ k ≤ hdomain (insf s k y)"
unfolding insf_def
using hdomain_def hdomain_ins less_eq_hf_def nonrestrict_def by fastforce

lemma Seq_insf: "Seq s k ⟹ Seq (insf s k y) (succ k)"
by (simp add: Ordinal.Seq_def hdomain_insf hfunction_insf hrelation_insf)

lemma Seq_succ_iff: "Seq s (succ k) ⟷ Seq s k ∧ (∃y. ⟨k, y⟩ ❙∈ s)"
using Ordinal.Seq_def hdomain_def succ_def by auto

lemma nonrestrictD: "a ❙∈ nonrestrict s X ⟹ a ❙∈ s"
by (auto simp: nonrestrict_def)

lemma hpair_in_nonrestrict_iff [simp]:
"⟨a,b⟩ ❙∈ nonrestrict s X ⟷ ⟨a,b⟩ ❙∈ s ∧ ¬ a ❙∈ X"
by (auto simp: nonrestrict_def)

lemma app_nonrestrict_Seq: "Seq s k ⟹ z ❙∉ X ⟹ app (nonrestrict s X) z = app s z"
by (auto simp: Seq_def nonrestrict_def app_def HBall_def) (metis)

lemma app_insf_Seq: "Seq s k ⟹ app (insf s k y) k = y"
by (metis Seq_def hfunction_insf app_equality hmem_hinsert insf_def)

lemma app_insf2_Seq: "Seq s k ⟹ k' ≠ k ⟹ app (insf s k y) k' = app s k'"
by (simp add: app_nonrestrict_Seq insf_def app_ins2)

lemma app_insf_Seq_if: "Seq s k ⟹ app (insf s k y) k' = (if k' = k then y else app s k')"
by (metis app_insf2_Seq app_insf_Seq)

lemma Seq_imp_eq_app: "⟦Seq s d; ⟨x,y⟩ ❙∈ s⟧ ⟹ app s x = y"
by (metis Seq_def app_equality)

lemma Seq_iff_app: "⟦Seq s d; x ❙∈ d⟧ ⟹ ⟨x,y⟩ ❙∈ s ⟷ app s x = y"
by (auto simp: Seq_def hdomain_def app_equality)

lemma Exists_iff_app: "Seq s d ⟹ x ❙∈ d ⟹ (∃y. ⟨x, y⟩ ❙∈ s ∧ P y) = P (app s x)"
by (metis Seq_iff_app)

lemma Ord_trans2: "⟦i2 ❙∈ i; i ❙∈ j;  j ❙∈ k;  Ord k⟧ ⟹ i2❙∈k"
by (metis Ord_trans)

definition ord_rec_Seq :: "hf ⇒ (hf ⇒ hf) ⇒ hf ⇒ hf ⇒ hf ⇒ bool"
where
"ord_rec_Seq T G s k y ⟷
(Seq s k ∧ y = G (app s (⨆k)) ∧ app s 0 = T ∧
(∀n. succ n ❙∈ k ⟶ app s (succ n) = G (app s n)))"

lemma Seq_succ_insf:
assumes s: "Seq s (succ k)"  shows "∃ y. s = insf s k y"
proof -
obtain y where y: "⟨k, y⟩ ❙∈ s" by (metis Seq_succ_iff s)
hence yuniq: "∀ y'. ⟨k, y'⟩ ❙∈ s ⟶ y' = y" using s
{ fix z
assume z: "z ❙∈ s"
then obtain u v where uv: "z = ⟨u, v⟩" using s
by (metis Seq_def hrelation_def is_hpair_def)
hence "z ❙∈ insf s k y"
by (metis hemptyE hmem_hinsert hpair_in_nonrestrict_iff insf_def yuniq z)
} then show ?thesis
by (metis hf_equalityI hmem_hinsert insf_def nonrestrictD y)
qed

lemma ord_rec_Seq_succ_iff:
assumes k: "Ord k" and knz: "k ≠ 0"
shows "ord_rec_Seq T G s (succ k) z ⟷ (∃ s' y. ord_rec_Seq T G s' k y ∧ z = G y ∧ s = insf s' k y)"
proof
assume os: "ord_rec_Seq T G s (succ k) z"
have "s = insf s k (G (app s (⨆k)))"
by (smt (verit, best) Ord_pred Seq_succ_D Seq_succ_insf app_insf_Seq k knz ord_rec_Seq_def os succ_iff)
then show "∃s' y. ord_rec_Seq T G s' k y ∧ z = G y ∧ s = insf s' k y"
by (metis Ord_Sup_succ_eq Seq_succ_D app_insf_Seq k ord_rec_Seq_def os succ_iff)
next
assume ok: "∃s' y. ord_rec_Seq T G s' k y ∧ z = G y ∧ s = insf s' k y"
thus "ord_rec_Seq T G s (succ k) z" using ok k knz
by (auto simp: ord_rec_Seq_def app_insf_Seq_if hmem_ne hmem_succ_ne Seq_insf)
qed

lemma ord_rec_Seq_functional:
"Ord k ⟹ k ≠ 0 ⟹ ord_rec_Seq T G s k y ⟹ ord_rec_Seq T G s' k y' ⟹ y' = y"
proof (induct k arbitrary: y y' s s' rule: Ord_induct2)
case 0 thus ?case
next
case (succ k) show ?case
proof (cases "k=0")
case True thus ?thesis using succ
by (auto simp: ord_rec_Seq_def)
next
case False
thus ?thesis using succ
by (auto simp: ord_rec_Seq_succ_iff)
qed
qed

definition ord_recp :: "hf ⇒ (hf ⇒ hf) ⇒ (hf ⇒ hf) ⇒ hf ⇒ hf ⇒ bool"
where
"ord_recp T G H x y =
(if x=0 then y = T
else
if Ord(x) then ∃ s. ord_rec_Seq T G s x y
else y = H x)"

lemma ord_recp_functional: "ord_recp T G H x y ⟹ ord_recp T G H x y' ⟹ y' = y"
by (auto simp: ord_recp_def ord_rec_Seq_functional split: if_split_asm)

lemma ord_recp_succ_iff:
assumes k: "Ord k" shows "ord_recp T G H (succ k) z ⟷ (∃y. z = G y ∧ ord_recp T G H k y)"
proof (cases "k=0")
case True thus ?thesis
by (simp add: ord_recp_def ord_rec_Seq_def) (metis Seq_0 Seq_insf app_insf_Seq)
next
case False
thus ?thesis using k
by (auto simp: ord_recp_def ord_rec_Seq_succ_iff)
qed

definition ord_rec :: "hf ⇒ (hf ⇒ hf) ⇒ (hf ⇒ hf) ⇒ hf ⇒ hf"
where
"ord_rec T G H x = (THE y. ord_recp T G H x y)"

lemma ord_rec_0 [simp]: "ord_rec T G H 0 = T"

lemma ord_recp_total: "∃y. ord_recp T G H x y"
proof (cases "Ord x")
case True thus ?thesis
proof (induct x rule: Ord_induct2)
case 0 thus ?case
next
case (succ x) thus ?case
by (metis ord_recp_succ_iff)
qed
next
case False thus ?thesis
by (auto simp: ord_recp_def)
qed

lemma ord_rec_succ [simp]:
assumes k: "Ord k" shows "ord_rec T G H (succ k) = G (ord_rec T G H k)"
proof -
from ord_recp_total [of T G H k]
obtain y where "ord_recp T G H k y" by auto
thus ?thesis using k
by (metis (no_types, lifting) ord_rec_def ord_recp_functional ord_recp_succ_iff the_equality)
qed

lemma ord_rec_non [simp]: "¬ Ord x ⟹ ord_rec T G H x = H x"
by (metis Ord_0 ord_rec_def ord_recp_def the_equality)

end
```