(*  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"
    by (simp add: ord0_leq_refl)
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"
  by (simp add: ord0_le_def ord0_leq_refl)

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})"
  by (simp add: Abs_ordinal_inverse quotientI)

lemma mem_ord0rel_Image [simp, intro!]: "x ∈ ord0rel `` {x}"
  by (simp add: ord0rel_def)

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])
  apply (simp add: ord0rel_def)
  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
    by (auto simp add: ordinal_le_def)
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
    by (auto simp add: ordinal_less_def)
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}"
  by (simp add: wf)


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

lemma ord0_precD: "(x,y) ∈ ord0_prec ==> ∃f n. x = f n ∧ y = ord0_Lim f"
  by (simp add: ord0_prec_def)

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

lemma Abs_ordinal_oStrictLimit:
  "Abs_ordinal (ord0rel `` {ord0_Lim f})
  = oStrictLimit (λn. Abs_ordinal (ord0rel `` {f n}))"
  apply (simp add: oStrictLimit_def)
  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
      by (simp add: Abs_ordinal_oStrictLimit local.step)
  qed
  then show ?thesis
    by (simp add: z)
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