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]: "(x1. P x) = P 0"
  by (simp add: One_hf_eq_succ)

lemma hbex_One [simp]: "(x1. 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: " ij;  jk;  Ord(k)    ik"
  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)  kl  k=l  lk"
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) "kl" | (eq) "k=l" | (gt) "lk"
by (metis Ord_linear o)

lemma Ord_linear2:
  assumes o: "Ord(k)" "Ord(l)"
  obtains (lt) "kl" | (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)  kl  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. iA  Ord(i)    Ord( A)"
  by (auto simp: Ord_def Transset_def) blast

lemma Ord_Inter [intro,simp]:
  assumes "i. iA  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: "A0; i. iA  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: "A0; i. iA  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  i2k"
  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