Theory OrdinalRec

(*  Title:       Countable Ordinals

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

section ‹Recursive Definitions›

theory OrdinalRec
imports OrdinalCont
begin

definition
  oPrec :: "ordinal ⇒ ordinal" where
  "oPrec x = (THE p. x = oSuc p)"

lemma oPrec_oSuc [simp]: "oPrec (oSuc x) = x"
  by (simp add: oPrec_def)

lemma oPrec_less: "∃p. x = oSuc p ⟹ oPrec x < x"
  by clarsimp

definition
  ordinal_rec0 ::
    "['a, ordinal ⇒ 'a ⇒ 'a, (nat ⇒ 'a) ⇒ 'a, ordinal] ⇒ 'a" where
  "ordinal_rec0 z s l ≡ wfrec {(x,y). x < y} (λF x.
    if x = 0 then z else
    if (∃p. x = oSuc p) then s (oPrec x) (F (oPrec x)) else
    (THE y. ∀f. (∀n. f n < oLimit f) ∧ oLimit f = x
            ⟶ l (λn. F (f n)) = y))"

lemma ordinal_rec0_0 [simp]: "ordinal_rec0 z s l 0 = z"
  by (simp add: cut_apply def_wfrec[OF ordinal_rec0_def wf])

lemma ordinal_rec0_oSuc: "ordinal_rec0 z s l (oSuc x) = s x (ordinal_rec0 z s l x)"
  by (simp add: cut_apply def_wfrec[OF ordinal_rec0_def wf])

lemma limit_ordinal_not_0: "limit_ordinal x ⟹ x ≠ 0" and limit_ordinal_not_oSuc: "limit_ordinal x ⟹ x ≠ oSuc p"
  by auto


lemma ordinal_rec0_limit_ordinal:
"limit_ordinal x ⟹ ordinal_rec0 z s l x =
 (THE y. ∀f. (∀n. f n < oLimit f) ∧ oLimit f = x ⟶ 
   l (λn. ordinal_rec0 z s l (f n)) = y)"
 apply (rule trans[OF def_wfrec[OF ordinal_rec0_def wf]])
 apply (simp add: limit_ordinal_not_oSuc limit_ordinal_not_0)
 apply (rule_tac f=The in arg_cong, rule ext)
 apply (rule_tac f=All in arg_cong, rule ext)
 apply safe
  apply (simp add: cut_apply)
 apply (simp add: cut_apply)
done


subsection ‹Partial orders›

locale porder =
  fixes le  :: "'a ⇒ 'a ⇒ bool" (infixl ‹<<› 55)
assumes po_refl:    "⋀x. x << x"
    and po_trans:   "⋀x y z. ⟦x << y; y << z⟧ ⟹ x << z"
    and po_antisym: "⋀x y. ⟦x << y; y << x⟧ ⟹ x = y"

lemma porder_order: "porder ((≤) :: 'a::order ⇒ 'a ⇒ bool)"
  using porder_def by fastforce

lemma (in porder) flip: "porder (λx y. y << x)"
  by (metis (no_types, lifting) po_antisym po_refl po_trans porder_def)

locale omega_complete = porder +
  fixes lub :: "(nat ⇒ 'a) ⇒ 'a"
  assumes is_ub_lub: "⋀f n. f n << lub f"
  assumes is_lub_lub: "⋀f x. ∀n. f n << x ⟹ lub f << x"

lemma (in omega_complete) lub_cong_lemma:
"⟦∀n. f n < oLimit f; ∀m. g m < oLimit g; oLimit f ≤ oLimit g;
 ∀y<oLimit g. ∀x≤y. F x << F y⟧
 ⟹ lub (λn. F (f n)) << lub (λn. F (g n))"
 apply (rule is_lub_lub[rule_format])
  by (metis dual_order.trans is_ub_lub leD linorder_le_cases oLimit_leI po_trans)


lemma (in omega_complete) lub_cong:
"⟦∀n. f n < oLimit f; ∀m. g m < oLimit g; oLimit f = oLimit g;
 ∀y<oLimit g. ∀x≤y. F x << F y⟧
 ⟹ lub (λn. F (f n)) = lub (λn. F (g n))"
  by (simp add: lub_cong_lemma po_antisym)

lemma (in omega_complete) ordinal_rec0_mono:
  assumes s: "∀p x. x << s p x" and "x ≤ y"
  shows "ordinal_rec0 z s lub x << ordinal_rec0 z s lub y"
proof -
  have "∀y≤w. ∀x≤y. ordinal_rec0 z s lub x << ordinal_rec0 z s lub y" for w
  proof (induction w rule: oLimit_induct)
    case zero
    then show ?case
      by (simp add: po_refl)
  next
    case (suc x)
    then show ?case
      by (metis le_oSucE oSuc_le_oSuc ordinal_rec0_oSuc po_refl po_trans s)
  next
    case (lim f)
    then have "∀g. (∀n. g n < oLimit g) ∧ oLimit g = oLimit f ⟶
             lub (λn. ordinal_rec0 z s lub (g n)) =
             lub (λn. ordinal_rec0 z s lub (f n))"
      by (metis linorder_not_le lub_cong oLimit_leI order_le_less strict_mono_less_oLimit)
    with lim have "ordinal_rec0 z s lub (oLimit f) =
                     lub (λn. ordinal_rec0 z s lub (f n))"
      apply (simp add: ordinal_rec0_limit_ordinal strict_mono_limit_ordinal)
      by (smt (verit, del_insts) the_equality strict_mono_less_oLimit)
    then show ?case
      by (smt (verit, ccfv_SIG) is_ub_lub le_oLimitE lim.IH order_le_less po_refl po_trans)
  qed
  with assms show ?thesis
    by blast
qed

lemma (in omega_complete) ordinal_rec0_oLimit:
  assumes s: "∀p x. x << s p x"
  shows "ordinal_rec0 z s lub (oLimit f) =
         lub (λn. ordinal_rec0 z s lub (f n))"
proof (cases "∀n. f n < oLimit f")
  case True
  then show ?thesis
    apply (simp add: ordinal_rec0_limit_ordinal limit_ordinal_oLimitI)
    apply (rule the_equality)
     apply (metis lub_cong omega_complete.ordinal_rec0_mono omega_complete_axioms s)
    by simp
next
  case False
  then show ?thesis
    apply (simp add: linorder_not_less, clarify)
    by (smt (verit, best) is_lub_lub is_ub_lub le_oLimit ordinal_rec0_mono po_antisym s)    
qed


subsection ‹Recursive definitions for @{typ "ordinal => ordinal"}›

definition
  ordinal_rec ::
    "[ordinal, ordinal ⇒ ordinal ⇒ ordinal, ordinal] ⇒ ordinal" where
  "ordinal_rec z s = ordinal_rec0 z s oLimit"

lemma omega_complete_oLimit: "omega_complete (≤) oLimit"
  by (simp add: oLimit_leI omega_complete_axioms_def omega_complete_def porder_order)

lemma ordinal_rec_0 [simp]: "ordinal_rec z s 0 = z"
  by (simp add: ordinal_rec_def)

lemma ordinal_rec_oSuc [simp]:
  "ordinal_rec z s (oSuc x) = s x (ordinal_rec z s x)"
  by (unfold ordinal_rec_def, rule ordinal_rec0_oSuc)

lemma ordinal_rec_oLimit:
  assumes s: "∀p x. x ≤ s p x"
  shows "ordinal_rec z s (oLimit f) = oLimit (λn. ordinal_rec z s (f n))"
  by (metis omega_complete.ordinal_rec0_oLimit omega_complete_oLimit ordinal_rec_def s)

lemma continuous_ordinal_rec:
  assumes s: "∀p x. x ≤ s p x"
  shows "continuous (ordinal_rec z s)"
  by (simp add: continuous.intro ordinal_rec_oLimit s)

lemma mono_ordinal_rec:
  assumes s: "∀p x. x ≤ s p x"
  shows "mono (ordinal_rec z s)"
  by (simp add: continuous.mono continuous_ordinal_rec s)

lemma normal_ordinal_rec:
  assumes s: "∀p x. x < s p x"
  shows "normal (ordinal_rec z s)"
  by (simp add: assms continuous.cont continuous_ordinal_rec less_imp_le normalI)

end