Theory HereditarilyFinite.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"
  by (simp add: succ_def)

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"
  by (simp add: One_hf_eq_succ)

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

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"
  by (simp add: Ord_def Transset_def)

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⟩"
  by (force simp add: is_hpair_def)

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"
  by (simp add: inj_on_def)

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"
  by (simp add: Seq_def succ_def)

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
    by (simp add: Seq_def hfunction_def)
  { 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
    by (simp add: ord_rec_Seq_def)
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"
  by (simp add: ord_recp_def ord_rec_def)

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
      by (simp add: ord_recp_def)
  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