# Theory HOL-Cardinals.Wellorder_Constructions

```(*  Title:      HOL/Cardinals/Wellorder_Constructions.thy
Author:     Andrei Popescu, TU Muenchen

Constructions on wellorders.
*)

section ‹Constructions on Wellorders›

theory Wellorder_Constructions
imports
Wellorder_Embedding Order_Union
begin

unbundle cardinal_syntax

declare
ordLeq_Well_order_simp[simp]
not_ordLeq_iff_ordLess[simp]
not_ordLess_iff_ordLeq[simp]
Func_empty[simp]
Func_is_emp[simp]

subsection ‹Order filters versus restrictions and embeddings›

lemma ofilter_subset_iso:
assumes WELL: "Well_order r" and
OFA: "ofilter r A" and OFB: "ofilter r B"
shows "(A = B) = iso (Restr r A) (Restr r B) id"
using assms by (auto simp add: ofilter_subset_embedS_iso)

subsection ‹Ordering the well-orders by existence of embeddings›

corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq"
using ordLeq_reflexive unfolding ordLeq_def refl_on_def
by blast

corollary ordLeq_trans: "trans ordLeq"
using trans_def[of ordLeq] ordLeq_transitive by blast

corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq"
by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans)

corollary ordIso_subset: "ordIso ⊆ {r. Well_order r} × {r. Well_order r}"
using ordIso_reflexive unfolding refl_on_def ordIso_def by blast

corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso"
using ordIso_reflexive unfolding refl_on_def ordIso_def
by blast

corollary ordIso_trans: "trans ordIso"
using trans_def[of ordIso] ordIso_transitive by blast

corollary ordIso_sym: "sym ordIso"
by (auto simp add: sym_def ordIso_symmetric)

corollary ordIso_equiv: "equiv {r. Well_order r} ordIso"
using ordIso_subset ordIso_refl_on ordIso_sym ordIso_trans by (intro equivI)

lemma ordLess_Well_order_simp[simp]:
assumes "r <o r'"
shows "Well_order r ∧ Well_order r'"
using assms unfolding ordLess_def by simp

lemma ordIso_Well_order_simp[simp]:
assumes "r =o r'"
shows "Well_order r ∧ Well_order r'"
using assms unfolding ordIso_def by simp

lemma ordLess_irrefl: "irrefl ordLess"
by(unfold irrefl_def, auto simp add: ordLess_irreflexive)

lemma ordLess_or_ordIso:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "r <o r' ∨ r' <o r ∨ r =o r'"
unfolding ordLess_def ordIso_def
using assms embedS_or_iso[of r r'] by auto

corollary ordLeq_ordLess_Un_ordIso:
"ordLeq = ordLess ∪ ordIso"

lemma ordIso_or_ordLess:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "r =o r' ∨ r <o r' ∨ r' <o r"
using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blast

lemmas ord_trans = ordIso_transitive ordLeq_transitive ordLess_transitive
ordIso_ordLeq_trans ordLeq_ordIso_trans
ordIso_ordLess_trans ordLess_ordIso_trans
ordLess_ordLeq_trans ordLeq_ordLess_trans

lemma ofilter_ordLeq:
assumes "Well_order r" and "ofilter r A"
shows "Restr r A ≤o r"
by (metis assms inf.orderE ofilter_embed ofilter_subset_ordLeq refl_on_def wo_rel.Field_ofilter wo_rel.REFL wo_rel.intro)

corollary under_Restr_ordLeq:
"Well_order r ⟹ Restr r (under r a) ≤o r"
by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def)

subsection ‹Copy via direct images›

lemma Id_dir_image: "dir_image Id f ≤ Id"
unfolding dir_image_def by auto

lemma Un_dir_image:
"dir_image (r1 ∪ r2) f = (dir_image r1 f) ∪ (dir_image r2 f)"
unfolding dir_image_def by auto

lemma Int_dir_image:
assumes "inj_on f (Field r1 ∪ Field r2)"
shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)"
proof
show "dir_image (r1 Int r2) f ≤ (dir_image r1 f) Int (dir_image r2 f)"
using assms unfolding dir_image_def inj_on_def by auto
next
show "(dir_image r1 f) Int (dir_image r2 f) ≤ dir_image (r1 Int r2) f"
by (clarsimp simp: dir_image_def) (metis FieldI1 FieldI2 UnCI assms inj_on_def)
qed

(* More facts on ordinal sum: *)

lemma Osum_embed:
assumes FLD: "Field r Int Field r' = {}" and
WELL: "Well_order r" and WELL': "Well_order r'"
shows "embed r (r Osum r') id"
proof-
have 1: "Well_order (r Osum r')"
using assms by (auto simp add: Osum_Well_order)
moreover
have "compat r (r Osum r') id"
unfolding compat_def Osum_def by auto
moreover
have "inj_on id (Field r)" by simp
moreover
have "ofilter (r Osum r') (Field r)"
using 1 FLD
by (auto simp add: wo_rel_def wo_rel.ofilter_def Osum_def under_def Field_iff disjoint_iff)
ultimately show ?thesis
using assms by (auto simp add: embed_iff_compat_inj_on_ofilter)
qed

corollary Osum_ordLeq:
assumes FLD: "Field r Int Field r' = {}" and
WELL: "Well_order r" and WELL': "Well_order r'"
shows "r ≤o r Osum r'"
using assms Osum_embed Osum_Well_order
unfolding ordLeq_def by blast

lemma Well_order_embed_copy:
assumes WELL: "well_order_on A r" and
INJ: "inj_on f A" and SUB: "f ` A ≤ B"
shows "∃r'. well_order_on B r' ∧ r ≤o r'"
proof-
have "bij_betw f A (f ` A)"
using INJ inj_on_imp_bij_betw by blast
then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''"
using WELL  Well_order_iso_copy by blast
hence 2: "Well_order r'' ∧ Field r'' = (f ` A)"
using well_order_on_Well_order by blast
(*  *)
let ?C = "B - (f ` A)"
obtain r''' where "well_order_on ?C r'''"
using well_order_on by blast
hence 3: "Well_order r''' ∧ Field r''' = ?C"
using well_order_on_Well_order by blast
(*  *)
let ?r' = "r'' Osum r'''"
have "Field r'' Int Field r''' = {}"
using 2 3 by auto
hence "r'' ≤o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast
hence 4: "r ≤o ?r'" using 1 ordIso_ordLeq_trans by blast
(*  *)
hence "Well_order ?r'" unfolding ordLeq_def by auto
moreover
have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum)
ultimately show ?thesis using 4 by blast
qed

subsection ‹The maxim among a finite set of ordinals›

text ‹The correct phrasing would be ``a maxim of ...", as ‹≤o› is only a preorder.›

definition isOmax :: "'a rel set ⇒ 'a rel ⇒ bool"
where
"isOmax  R r ≡ r ∈ R ∧ (∀r' ∈ R. r' ≤o r)"

definition omax :: "'a rel set ⇒ 'a rel"
where
"omax R == SOME r. isOmax R r"

lemma exists_isOmax:
assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. Well_order r"
shows "∃ r. isOmax R r"
proof-
have "finite R ⟹ R ≠ {} ⟶ (∀ r ∈ R. Well_order r) ⟶ (∃ r. isOmax R r)"
proof(clarsimp)
fix r :: "('a × 'a) set" and R assume *: "finite R" and **: "r ∉ R"
and ***: "Well_order r" and ****: "∀r∈R. Well_order r"
and IH: "R ≠ {} ⟶ (∃p. isOmax R p)"
let ?R' = "insert r R"
show "∃p'. (isOmax ?R' p')"
proof(cases "R = {}")
case True
thus ?thesis
by (simp add: "***" isOmax_def ordLeq_reflexive)
next
case False
then obtain p where p: "isOmax R p" using IH by auto
hence  "Well_order p" using **** unfolding isOmax_def by simp
then consider  "r ≤o p" | "p ≤o r"
using *** ordLeq_total by auto
then show ?thesis
proof cases
case 1
then show ?thesis
using p unfolding isOmax_def by auto
next
case 2
then show ?thesis
by (metis "***" insert_iff isOmax_def ordLeq_reflexive ordLeq_transitive p)
qed
qed
qed
thus ?thesis using assms by auto
qed

lemma omax_isOmax:
assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. Well_order r"
shows "isOmax R (omax R)"
unfolding omax_def using assms

lemma omax_in:
assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. Well_order r"
shows "omax R ∈ R"
using assms omax_isOmax unfolding isOmax_def by blast

lemma Well_order_omax:
assumes "finite R" and "R ≠ {}" and "∀r∈R. Well_order r"
shows "Well_order (omax R)"
using assms omax_in by blast

lemma omax_maxim:
assumes "finite R" and "∀ r ∈ R. Well_order r" and "r ∈ R"
shows "r ≤o omax R"
using assms omax_isOmax unfolding isOmax_def by blast

lemma omax_ordLeq:
assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. r ≤o p"
shows "omax R ≤o p"
by (meson assms omax_in ordLeq_Well_order_simp)

lemma omax_ordLess:
assumes "finite R" and "R ≠ {}" and "∀ r ∈ R. r <o p"
shows "omax R <o p"
by (meson assms omax_in ordLess_Well_order_simp)

lemma omax_ordLeq_elim:
assumes "finite R" and "∀ r ∈ R. Well_order r"
and "omax R ≤o p" and "r ∈ R"
shows "r ≤o p"
by (meson assms omax_maxim ordLeq_transitive)

lemma omax_ordLess_elim:
assumes "finite R" and "∀ r ∈ R. Well_order r"
and "omax R <o p" and "r ∈ R"
shows "r <o p"
by (meson assms omax_maxim ordLeq_ordLess_trans)

lemma ordLeq_omax:
assumes "finite R" and "∀ r ∈ R. Well_order r"
and "r ∈ R" and "p ≤o r"
shows "p ≤o omax R"
by (meson assms omax_maxim ordLeq_transitive)

lemma ordLess_omax:
assumes "finite R" and "∀ r ∈ R. Well_order r"
and "r ∈ R" and "p <o r"
shows "p <o omax R"
by (meson assms omax_maxim ordLess_ordLeq_trans)

lemma omax_ordLeq_mono:
assumes P: "finite P" and R: "finite R"
and NE_P: "P ≠ {}" and Well_R: "∀ r ∈ R. Well_order r"
and LEQ: "∀ p ∈ P. ∃ r ∈ R. p ≤o r"
shows "omax P ≤o omax R"
by (meson LEQ NE_P P R Well_R omax_ordLeq ordLeq_omax)

lemma omax_ordLess_mono:
assumes P: "finite P" and R: "finite R"
and NE_P: "P ≠ {}" and Well_R: "∀ r ∈ R. Well_order r"
and LEQ: "∀ p ∈ P. ∃ r ∈ R. p <o r"
shows "omax P <o omax R"
by (meson LEQ NE_P P R Well_R omax_ordLess ordLess_omax)

subsection ‹Limit and succesor ordinals›

lemma embed_underS2:
assumes r: "Well_order r" and g: "embed r s g" and a: "a ∈ Field r"
shows "g ` underS r a = underS s (g a)"
by (meson a bij_betw_def embed_underS g r)

lemma bij_betw_insert:
assumes "b ∉ A" and "f b ∉ A'" and "bij_betw f A A'"
shows "bij_betw f (insert b A) (insert (f b) A')"
using notIn_Un_bij_betw[OF assms] by auto

context wo_rel
begin

lemma underS_induct:
assumes "⋀a. (⋀ a1. a1 ∈ underS a ⟹ P a1) ⟹ P a"
shows "P a"
by (induct rule: well_order_induct) (rule assms, simp add: underS_def)

lemma suc_underS:
assumes B: "B ⊆ Field r" and A: "AboveS B ≠ {}" and b: "b ∈ B"
shows "b ∈ underS (suc B)"
using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto

lemma underS_supr:
assumes bA: "b ∈ underS (supr A)" and A: "A ⊆ Field r"
shows "∃ a ∈ A. b ∈ underS a"
proof(rule ccontr, simp)
have bb: "b ∈ Field r" using bA unfolding underS_def Field_def by auto
assume "∀a∈A.  b ∉ underS a"
hence 0: "∀a ∈ A. (a,b) ∈ r" using A bA unfolding underS_def
by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
have "(supr A, b) ∈ r"
by (simp add: "0" A bb supr_least)
thus False
by (metis antisymD bA underS_E wo_rel.ANTISYM wo_rel_axioms)
qed

lemma underS_suc:
assumes bA: "b ∈ underS (suc A)" and A: "A ⊆ Field r"
shows "∃ a ∈ A. b ∈ under a"
proof(rule ccontr, simp)
have bb: "b ∈ Field r" using bA unfolding underS_def Field_def by auto
assume "∀a∈A.  b ∉ under a"
hence 0: "∀a ∈ A. a ∈ underS b" using A bA
by (metis bb in_mono max2_def max2_greater mem_Collect_eq underS_I under_def)
have "(suc A, b) ∈ r"
by (metis "0" A bb suc_least underS_E)
thus False
by (metis antisymD bA underS_E wo_rel.ANTISYM wo_rel_axioms)
qed

lemma (in wo_rel) in_underS_supr:
assumes "j ∈ underS i" and "i ∈ A" and "A ⊆ Field r" and "Above A ≠ {}"
shows "j ∈ underS (supr A)"
by (meson assms LIN in_mono supr_greater supr_inField underS_incl_iff)

lemma inj_on_Field:
assumes A: "A ⊆ Field r" and f: "⋀ a b. ⟦a ∈ A; b ∈ A; a ∈ underS b⟧ ⟹ f a ≠ f b"
shows "inj_on f A"
by (smt (verit) A f in_notinI inj_on_def subsetD underS_I)

lemma ofilter_init_seg_of:
assumes "ofilter F"
shows "Restr r F initial_segment_of r"
using assms unfolding ofilter_def init_seg_of_def under_def by auto

lemma underS_init_seg_of_Collect:
assumes "⋀j1 j2. ⟦j2 ∈ underS i; (j1, j2) ∈ r⟧ ⟹ R j1 initial_segment_of R j2"
shows "{R j |j. j ∈ underS i} ∈ Chains init_seg_of"
using TOTALS assms
by (clarsimp simp: Chains_def) (meson BNF_Least_Fixpoint.underS_Field)

lemma (in wo_rel) Field_init_seg_of_Collect:
assumes "⋀j1 j2. ⟦j2 ∈ Field r; (j1, j2) ∈ r⟧ ⟹ R j1 initial_segment_of R j2"
shows "{R j |j. j ∈ Field r} ∈ Chains init_seg_of"
using TOTALS assms by (auto simp: Chains_def)

subsubsection ‹Successor and limit elements of an ordinal›

definition "succ i ≡ suc {i}"

definition "isSucc i ≡ ∃ j. aboveS j ≠ {} ∧ i = succ j"

definition "zero = minim (Field r)"

definition "isLim i ≡ ¬ isSucc i"

lemma zero_smallest[simp]:
assumes "j ∈ Field r" shows "(zero, j) ∈ r"
by (simp add: assms wo_rel.ofilter_linord wo_rel_axioms zero_def)

lemma zero_in_Field: assumes "Field r ≠ {}"  shows "zero ∈ Field r"
using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def)

lemma leq_zero_imp[simp]:
"(x, zero) ∈ r ⟹ x = zero"
by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest)

lemma leq_zero[simp]:
assumes "Field r ≠ {}"  shows "(x, zero) ∈ r ⟷ x = zero"
using zero_in_Field[OF assms] in_notinI[of x zero] by auto

lemma under_zero[simp]:
assumes "Field r ≠ {}" shows "under zero = {zero}"
using assms unfolding under_def by auto

lemma underS_zero[simp,intro]: "underS zero = {}"
unfolding underS_def by auto

lemma isSucc_succ: "aboveS i ≠ {} ⟹ isSucc (succ i)"
unfolding isSucc_def succ_def by auto

lemma succ_in_diff:
assumes "aboveS i ≠ {}"  shows "(i,succ i) ∈ r ∧ succ i ≠ i"
using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto

lemmas succ_in[simp] = succ_in_diff[THEN conjunct1]
lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2]

lemma succ_in_Field[simp]:
assumes "aboveS i ≠ {}"  shows "succ i ∈ Field r"
using succ_in[OF assms] unfolding Field_def by auto

lemma succ_not_in:
assumes "aboveS i ≠ {}" shows "(succ i, i) ∉ r"
by (metis FieldI2 assms max2_equals1 max2_equals2 succ_diff succ_in)

lemma not_isSucc_zero: "¬ isSucc zero"
by (metis isSucc_def leq_zero_imp succ_in_diff)

lemma isLim_zero[simp]: "isLim zero"
by (metis isLim_def not_isSucc_zero)

lemma succ_smallest:
assumes "(i,j) ∈ r" and "i ≠ j"
shows "(succ i, j) ∈ r"
by (metis Field_iff assms empty_subsetI insert_subset singletonD suc_least succ_def)

lemma isLim_supr:
assumes f: "i ∈ Field r" and l: "isLim i"
shows "i = supr (underS i)"
proof(rule equals_supr)
fix j assume j: "j ∈ Field r" and 1: "⋀ j'. j' ∈ underS i ⟹ (j',j) ∈ r"
show "(i,j) ∈ r"
proof(intro in_notinI[OF _ f j], safe)
assume ji: "(j,i) ∈ r" "j ≠ i"
hence a: "aboveS j ≠ {}" unfolding aboveS_def by auto
hence "i ≠ succ j" using l unfolding isLim_def isSucc_def by auto
moreover have "(succ j, i) ∈ r" using succ_smallest[OF ji] by auto
ultimately have "succ j ∈ underS i" unfolding underS_def by auto
hence "(succ j, j) ∈ r" using 1 by auto
thus False using succ_not_in[OF a] by simp
qed
qed(use f underS_def Field_def in fastforce)+

definition "pred i ≡ SOME j. j ∈ Field r ∧ aboveS j ≠ {} ∧ succ j = i"

lemma pred_Field_succ:
assumes "isSucc i" shows "pred i ∈ Field r ∧ aboveS (pred i) ≠ {} ∧ succ (pred i) = i"
proof-
obtain j where j: "aboveS j ≠ {}" "i = succ j"
using assms unfolding isSucc_def by auto
then obtain "j ∈ Field r" "j ≠ i"
by (metis FieldI1 succ_diff succ_in)
then show ?thesis unfolding pred_def
by (metis (mono_tags, lifting) j someI_ex)
qed

lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1]
lemmas aboveS_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct1]
lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2]

lemma isSucc_pred_in:
assumes "isSucc i"  shows "(pred i, i) ∈ r"
by (metis assms pred_Field_succ succ_in)

lemma isSucc_pred_diff:
assumes "isSucc i"  shows "pred i ≠ i"
by (metis aboveS_pred assms succ_diff succ_pred)

(* todo: pred maximal, pred injective? *)

lemma succ_inj[simp]:
assumes "aboveS i ≠ {}" and "aboveS j ≠ {}"
shows "succ i = succ j ⟷ i = j"
by (metis FieldI1 assms succ_def succ_in supr_under under_underS_suc)

lemma pred_succ[simp]:
assumes "aboveS j ≠ {}"  shows "pred (succ j) = j"
using assms isSucc_def pred_Field_succ succ_inj by blast

lemma less_succ[simp]:
assumes "aboveS i ≠ {}"
shows "(j, succ i) ∈ r ⟷ (j,i) ∈ r ∨ j = succ i"
by (metis FieldI1 assms in_notinI max2_equals1 max2_equals2 max2_iff succ_in succ_smallest)

lemma underS_succ[simp]:
assumes "aboveS i ≠ {}"
shows "underS (succ i) = under i"
unfolding underS_def under_def by (auto simp: assms succ_not_in)

lemma succ_mono:
assumes "aboveS j ≠ {}" and "(i,j) ∈ r"
shows "(succ i, succ j) ∈ r"
by (metis (full_types) assms less_succ succ_smallest)

lemma under_succ[simp]:
assumes "aboveS i ≠ {}"
shows "under (succ i) = insert (succ i) (under i)"
using less_succ[OF assms] unfolding under_def by auto

definition mergeSL :: "('a ⇒ 'b ⇒ 'b) ⇒ (('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b"
where
"mergeSL S L f i ≡ if isSucc i then S (pred i) (f (pred i)) else L f i"

subsubsection ‹Well-order recursion with (zero), succesor, and limit›

definition worecSL :: "('a ⇒ 'b ⇒ 'b) ⇒ (('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ 'a ⇒ 'b"
where "worecSL S L ≡ worec (mergeSL S L)"

definition "adm_woL L ≡ ∀f g i. isLim i ∧ (∀j∈underS i. f j = g j) ⟶ L f i = L g i"

by (smt (verit, ccfv_threshold) isSucc_pred_diff isSucc_pred_in mergeSL_def underS_I)

lemma worec_fixpoint1: "adm_wo H ⟹ worec H i = H (worec H) i"
by (metis worec_fixpoint)

lemma worecSL_isSucc:
assumes a: "adm_woL L" and i: "isSucc i"
shows "worecSL S L i = S (pred i) (worecSL S L (pred i))"
by (metis a i mergeSL mergeSL_def worecSL_def worec_fixpoint)

lemma worecSL_succ:
assumes a: "adm_woL L" and i: "aboveS j ≠ {}"
shows "worecSL S L (succ j) = S j (worecSL S L j)"
by (simp add: a i isSucc_succ worecSL_isSucc)

lemma worecSL_isLim:
assumes a: "adm_woL L" and i: "isLim i"
shows "worecSL S L i = L (worecSL S L) i"
by (metis a i isLim_def mergeSL mergeSL_def worecSL_def worec_fixpoint)

definition worecZSL :: "'b ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ (('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ 'a ⇒ 'b"
where "worecZSL Z S L ≡ worecSL S (λ f a. if a = zero then Z else L f a)"

lemma worecZSL_zero:
shows "worecZSL Z S L zero = Z"
by (smt (verit, best) adm_woL_def assms isLim_zero worecSL_isLim worecZSL_def)

lemma worecZSL_succ:
assumes a: "adm_woL L" and i: "aboveS j ≠ {}"
shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)"
unfolding worecZSL_def
by (smt (verit, best) a adm_woL_def i worecSL_succ)

lemma worecZSL_isLim:
assumes a: "adm_woL L" and "isLim i" and "i ≠ zero"
shows "worecZSL Z S L i = L (worecZSL Z S L) i"
proof-
let ?L = "λ f a. if a = zero then Z else L f a"
have "worecZSL Z S L i = ?L (worecZSL Z S L) i"
unfolding worecZSL_def by (smt (verit, best) adm_woL_def assms worecSL_isLim)
also have "… = L (worecZSL Z S L) i" using assms by simp
finally show ?thesis .
qed

subsubsection ‹Well-order succ-lim induction›

lemma ord_cases:
obtains j where "i = succ j" and "aboveS j ≠ {}"  | "isLim i"
by (metis isLim_def isSucc_def)

lemma well_order_inductSL[case_names Suc Lim]:
assumes "⋀i. ⟦aboveS i ≠ {}; P i⟧ ⟹ P (succ i)"  "⋀i. ⟦isLim i; ⋀j. j ∈ underS i ⟹ P j⟧ ⟹ P i"
shows "P i"
proof(induction rule: well_order_induct)
case (1 x)
then show ?case
by (metis assms ord_cases succ_diff succ_in underS_E)
qed

lemma well_order_inductZSL[case_names Zero Suc Lim]:
assumes "P zero"
and  "⋀i. ⟦aboveS i ≠ {}; P i⟧ ⟹ P (succ i)" and
"⋀i. ⟦isLim i; i ≠ zero; ⋀j. j ∈ underS i ⟹ P j⟧ ⟹ P i"
shows "P i"
by (metis assms well_order_inductSL)

(* Succesor and limit ordinals *)
definition "isSuccOrd ≡ ∃ j ∈ Field r. ∀ i ∈ Field r. (i,j) ∈ r"
definition "isLimOrd ≡ ¬ isSuccOrd"

lemma isLimOrd_succ:
assumes isLimOrd and "i ∈ Field r"
shows "succ i ∈ Field r"
using assms unfolding isLimOrd_def isSuccOrd_def
by (metis REFL in_notinI refl_on_domain succ_smallest)

lemma isLimOrd_aboveS:
assumes l: isLimOrd and i: "i ∈ Field r"
shows "aboveS i ≠ {}"
proof-
obtain j where "j ∈ Field r" and "(j,i) ∉ r"
using assms unfolding isLimOrd_def isSuccOrd_def by auto
hence "(i,j) ∈ r ∧ j ≠ i" by (metis i max2_def max2_greater)
thus ?thesis unfolding aboveS_def by auto
qed

lemma succ_aboveS_isLimOrd:
assumes "∀ i ∈ Field r. aboveS i ≠ {} ∧ succ i ∈ Field r"
shows isLimOrd
using assms isLimOrd_def isSuccOrd_def succ_not_in by blast

lemma isLim_iff:
assumes l: "isLim i" and j: "j ∈ underS i"
shows "∃ k. k ∈ underS i ∧ j ∈ underS k"
by (metis Order_Relation.underS_Field empty_iff isLim_supr j l underS_empty underS_supr)

end (* context wo_rel *)

abbreviation "zero ≡ wo_rel.zero"
abbreviation "succ ≡ wo_rel.succ"
abbreviation "pred ≡ wo_rel.pred"
abbreviation "isSucc ≡ wo_rel.isSucc"
abbreviation "isLim ≡ wo_rel.isLim"
abbreviation "isLimOrd ≡ wo_rel.isLimOrd"
abbreviation "isSuccOrd ≡ wo_rel.isSuccOrd"
abbreviation "worecSL ≡ wo_rel.worecSL"
abbreviation "worecZSL ≡ wo_rel.worecZSL"

subsection ‹Projections of wellorders›

definition "oproj r s f ≡ Field s ⊆ f ` (Field r) ∧ compat r s f"

lemma oproj_in:
assumes "oproj r s f" and "(a,a') ∈ r"
shows "(f a, f a') ∈ s"
using assms unfolding oproj_def compat_def by auto

lemma oproj_Field:
assumes f: "oproj r s f" and a: "a ∈ Field r"
shows "f a ∈ Field s"
using oproj_in[OF f] a unfolding Field_def by auto

lemma oproj_Field2:
assumes f: "oproj r s f" and a: "b ∈ Field s"
shows "∃ a ∈ Field r. f a = b"
using assms unfolding oproj_def by auto

lemma oproj_under:
assumes f:  "oproj r s f" and a: "a ∈ under r a'"
shows "f a ∈ under s (f a')"
using oproj_in[OF f] a unfolding under_def by auto

(* An ordinal is embedded in another whenever it is embedded as an order
(not necessarily as initial segment):*)
theorem embedI:
assumes r: "Well_order r" and s: "Well_order s"
and f: "⋀ a. a ∈ Field r ⟹ f a ∈ Field s ∧ f ` underS r a ⊆ underS s (f a)"
shows "∃ g. embed r s g"
proof-
interpret r: wo_rel r by unfold_locales (rule r)
interpret s: wo_rel s by unfold_locales (rule s)
let ?G = "λ g a. suc s (g ` underS r a)"
define g where "g = worec r ?G"
(*  *)
{fix a assume "a ∈ Field r"
hence "bij_betw g (under r a) (under s (g a)) ∧
g a ∈ under s (f a)"
proof(induction a rule: r.underS_induct)
case (1 a)
hence a: "a ∈ Field r"
and IH1a: "⋀ a1. a1 ∈ underS r a ⟹ inj_on g (under r a1)"
and IH1b: "⋀ a1. a1 ∈ underS r a ⟹ g ` under r a1 = under s (g a1)"
and IH2: "⋀ a1. a1 ∈ underS r a ⟹ g a1 ∈ under s (f a1)"
unfolding underS_def Field_def bij_betw_def by auto
have fa: "f a ∈ Field s" using f[OF a] by auto
have g: "g a = suc s (g ` underS r a)"
using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast
have A0: "g ` underS r a ⊆ Field s"
using IH1b by (metis IH2 image_subsetI in_mono under_Field)
{fix a1 assume a1: "a1 ∈ underS r a"
from IH2[OF this] have "g a1 ∈ under s (f a1)" .
moreover have "f a1 ∈ underS s (f a)" using f[OF a] a1 by auto
ultimately have "g a1 ∈ underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans)
}
hence fa_in: "f a ∈ AboveS s (g ` underS r a)" unfolding AboveS_def
using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def)
hence A: "AboveS s (g ` underS r a) ≠ {}" by auto
have ga: "g a ∈ Field s" unfolding g using s.suc_inField[OF A0 A] .
show ?case
unfolding bij_betw_def
proof (intro conjI)
show "inj_on g (r.under a)"
by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux)
show "g ` r.under a = s.under (g a)"
by (metis A A0 IH1a IH1b a bij_betw_def g ga r s s.suc_greater wellorders_totally_ordered_aux)
show "g a ∈ s.under (f a)"
by (simp add: fa_in g s.suc_least_AboveS under_def)
qed
qed
}
thus ?thesis unfolding embed_def by auto
qed

corollary ordLeq_def2:
"r ≤o s ⟷ Well_order r ∧ Well_order s ∧
(∃ f. ∀ a ∈ Field r. f a ∈ Field s ∧ f ` underS r a ⊆ underS s (f a))"
using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s]
unfolding ordLeq_def by fast

lemma iso_oproj:
assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
shows "oproj r s f"
by (metis embed_Field f iso_Field iso_iff iso_iff3 oproj_def r s)

theorem oproj_embed:
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
shows "∃ g. embed s r g"
proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe)
fix b assume "b ∈ Field s"
thus "inv_into (Field r) f b ∈ Field r"
using oproj_Field2[OF f] by (metis imageI inv_into_into)
next
fix a b assume "b ∈ Field s" "a ≠ b" "(a, b) ∈ s"
"inv_into (Field r) f a = inv_into (Field r) f b"
with f show False
by (meson FieldI1 in_mono inv_into_injective oproj_def)
next
fix a b assume *: "b ∈ Field s" "a ≠ b" "(a, b) ∈ s"
{ assume notin: "(inv_into (Field r) f a, inv_into (Field r) f b) ∉ r"
moreover
from *(3) have "a ∈ Field s" unfolding Field_def by auto
then have "(inv_into (Field r) f b, inv_into (Field r) f a) ∈ r"
by (meson "*"(1) notin f in_mono inv_into_into oproj_def r wo_rel.in_notinI wo_rel.intro)
ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) ∈ r"
using r by (auto simp: well_order_on_def linear_order_on_def total_on_def)
with f[unfolded oproj_def compat_def] *(1) ‹a ∈ Field s›
f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"]
have "(b, a) ∈ s" by (metis in_mono)
with *(2,3) s have False
by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def)
} thus "(inv_into (Field r) f a, inv_into (Field r) f b) ∈ r" by blast
qed

corollary oproj_ordLeq:
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f"
shows "s ≤o r"
using f oproj_embed ordLess_iff ordLess_or_ordLeq r s by blast

end
```