Theory HereditarilyFinite.Rank

chapter ‹V-Sets, Epsilon Closure, Ranks›

theory Rank imports Ordinal
begin

section ‹V-sets›

text ‹Definition 4.1›
definition Vset :: "hf  hf"
  where "Vset x = ord_rec 0 HPow (λz. 0) x"

lemma Vset_0 [simp]: "Vset 0 = 0"
  by (simp add: Vset_def)

lemma Vset_succ [simp]: "Ord k  Vset (succ k) = HPow (Vset k)"
  by (simp add: Vset_def)

lemma Vset_non [simp]: "¬ Ord x  Vset x = 0"
  by (simp add: Vset_def)

text ‹Theorem 4.2(a)›
lemma Vset_mono_strict:
  assumes "Ord m" "n  m" shows "Vset n < Vset m"
proof -
  have n: "Ord n"
    by (metis Ord_in_Ord assms)
  hence "Ord m  n  m  Vset n < Vset m"
  proof (induct n arbitrary: m rule: Ord_induct2)
    case 0 thus ?case
      by (metis HPow_iff Ord_cases Vset_0 Vset_succ hemptyE le_imp_less_or_eq zero_le)
  next
    case (succ n)
    then show ?case using Ord m
      by (metis Ord_cases hemptyE HPow_mono_strict_iff Vset_succ mem_succ_iff)
  qed
  thus ?thesis using assms .
qed

lemma Vset_mono: "Ord m; n  m  Vset n  Vset m"
  by (metis Ord_linear2 Vset_mono_strict Vset_non order.order_iff_strict
            order_class.order.antisym zero_le)

text ‹Theorem 4.2(b)›
lemma Vset_Transset: "Ord m  Transset (Vset m)"
  by (induct rule: Ord_induct2) (auto simp: Transset_def)

lemma Ord_sup [simp]: "Ord k  Ord l  Ord (k  l)"
  by (metis Ord_linear_le le_iff_sup sup_absorb1)

lemma Ord_inf [simp]: "Ord k  Ord l  Ord (k  l)"
  by (metis Ord_linear_le inf_absorb2 le_iff_inf)


text ‹Theorem 4.3›
lemma Vset_universal: "n. Ord n  x  Vset n"
proof (induct x rule: hf_induct)
  case 0 thus ?case
    by (metis HPow_iff Ord_0 Ord_succ Vset_succ zero_le)
next
  case (hinsert a b)
  then obtain na nb where nab: "Ord na" "a  Vset na" "Ord nb" "b  Vset nb"
    by blast
  hence "b  Vset nb" using Vset_Transset [of nb]
    by (auto simp: Transset_def)
  also have "...  Vset (na  nb)" using nab
    by (metis Ord_sup Vset_mono sup_ge2)
  finally have "b  a  Vset (succ (na  nb))" using nab
    by simp (metis Ord_sup Vset_mono sup_ge1 rev_hsubsetD)
  thus ?case using nab
    by (metis Ord_succ Ord_sup)
qed


section ‹Least Ordinal Operator›

text ‹Definition 4.4. For every x, let rank(x) be the least ordinal n such that...›

lemma Ord_minimal:
   "Ord k  P k  n. Ord n  P n  (m. Ord m  P m  n  m)"
  by (induct k rule: Ord_induct) (metis Ord_linear2)

lemma OrdLeastI: "Ord k  P k  P(LEAST n. Ord n  P n)"
by (metis (lifting, no_types) Least_equality Ord_minimal)

lemma OrdLeast_le: "Ord k  P k  (LEAST n. Ord n  P n)  k"
by (metis (lifting, no_types) Least_equality Ord_minimal)

lemma OrdLeast_Ord:
  assumes "Ord k" "P k"shows "Ord(LEAST n. Ord n  P n)"
proof -
  obtain n where "Ord n" "P n" "m. Ord m  P m  n  m"
    by (metis Ord_minimal assms)
  thus ?thesis
    by (metis (lifting) Least_equality)
qed


section ‹Rank Function›

definition rank :: "hf  hf"
  where "rank x = (LEAST n. Ord n  x  Vset (succ n))"

lemma [simp]: "rank 0 = 0"
  by (simp add: rank_def) (metis (lifting) HPow_iff Least_equality Ord_0 Vset_succ zero_le)

lemma in_Vset_rank: "a  Vset(succ(rank a))"
proof -
  from Vset_universal [of a]
  obtain na where na: "Ord na" "a  Vset (succ na)"
    by (metis Ord_Union Ord_in_Ord Ord_pred Vset_0 hempty_iff)
  thus ?thesis
    by (unfold rank_def) (rule OrdLeastI)
qed

lemma Ord_rank [simp]: "Ord (rank a)"
  by (metis Ord_succ_iff Vset_non hemptyE in_Vset_rank)

lemma le_Vset_rank: "a  Vset(rank a)"
  by (metis HPow_iff Ord_succ_iff Vset_non Vset_succ hemptyE in_Vset_rank)

lemma VsetI: "succ(rank a)  k  Ord k  a  Vset k"
  by (metis Vset_mono hsubsetCE in_Vset_rank)

lemma Vset_succ_rank_le: "Ord k  a  Vset (succ k)  rank a  k"
  by (unfold rank_def) (rule OrdLeast_le)

lemma Vset_rank_lt: assumes a: "a  Vset k" shows "rank a < k"
proof -
  { assume k: "Ord k"
    hence ?thesis
    proof (cases k rule: Ord_cases)
      case 0 thus ?thesis using a
        by simp
    next
      case (succ l) thus ?thesis using a
        by (metis Ord_lt_succ_iff_le Ord_succ_iff Vset_non Vset_succ_rank_le hemptyE in_Vset_rank)
    qed
  }
  thus ?thesis using a
    by (metis Vset_non hemptyE)
qed

text ‹Theorem 4.5›
theorem rank_lt: "a  b  rank(a) < rank(b)"
  by (metis Vset_rank_lt hsubsetD le_Vset_rank)

lemma rank_mono: "x  y  rank x  rank y"
  by (metis HPow_iff Ord_rank Vset_succ Vset_succ_rank_le dual_order.trans le_Vset_rank)

lemma rank_sup [simp]: "rank (a  b) = rank a  rank b"
proof (rule antisym)
  have o: "Ord (rank a  rank b)"
    by simp
  have "a  Vset (rank a  rank b)  b  Vset (rank a  rank b)"
    by (metis le_Vset_rank order_trans Vset_mono sup_ge1 sup_ge2 o)
  thus "rank (a  b)  rank a  rank b"
    using Vset_succ_rank_le by auto
next
  show "rank a  rank b  rank (a  b)"
    by (metis le_supI le_supI1 le_supI2 order_eq_refl rank_mono)
qed

lemma rank_singleton [simp]: "rank a = succ(rank a)"
proof -
  have oba: "Ord (succ (rank a))"
    by simp
  show ?thesis
    proof (rule antisym)
      show "rank a  succ (rank a)"
        by (metis Vset_succ_rank_le HPow_iff Vset_succ in_Vset_rank less_eq_insert1_iff oba zero_le)
    next
      show "succ (rank a)  ranka"
        by (metis Ord_linear_le Ord_lt_succ_iff_le rank_lt Ord_rank hmem_hinsert less_le_not_le oba)
    qed
qed

lemma rank_hinsert [simp]: "rank (b  a) = rank b  succ(rank a)"
  by (metis hinsert_eq_sup rank_singleton rank_sup)

text ‹Definition 4.6. The transitive closure of @{term x} is
 the minimal transitive set @{term y} such that @{term"xy"}.›


section ‹Epsilon Closure›

definition
  eclose    :: "hf  hf"  where
    "eclose X =  Y  HPow(Vset (rank X)). Transset Y  XY"

lemma eclose_facts:
  shows Transset_eclose: "Transset (eclose X)"
   and  le_eclose: "X  eclose X"
proof -
  have nz: "Y  HPow(Vset (rank X)). Transset Y  XY  0"
    by (simp add: eclose_def hempty_iff) (metis Ord_rank Vset_Transset le_Vset_rank order_refl)
  show "Transset (eclose X)" "X  eclose X" using HInter_iff [OF nz]
    by (auto simp: eclose_def Transset_def)
qed

lemma eclose_minimal:
  assumes Y: "Transset Y" "XY" shows "eclose X  Y"
proof -
  have "Y  HPow(Vset (rank X)). Transset Y  XY  0"
    by (simp add: eclose_def hempty_iff) (metis Ord_rank Vset_Transset le_Vset_rank order_refl)
  moreover have "Transset (Y  Vset (rank X))"
    by (metis Ord_rank Transset_inf Vset_Transset Y(1))
  moreover have "X  Y  Vset (rank X)"
    by (metis Y(2) le_Vset_rank le_inf_iff)
  ultimately show "eclose X  Y"
    apply (clarsimp simp: eclose_def)
    apply (metis hinter_iff le_inf_iff order_refl)
    done
qed

lemma eclose_0 [simp]: "eclose 0 = 0"
  by (metis Ord_0 Vset_0 Vset_Transset eclose_minimal less_eq_hempty)

lemma eclose_sup [simp]: "eclose (a  b) = eclose a  eclose b"
proof (rule order_antisym)
  show "eclose (a  b)  eclose a  eclose b"
    by (metis Transset_eclose Transset_sup eclose_minimal le_eclose sup_mono)
next
  show "eclose a  eclose b  eclose (a  b)"
    by (metis Transset_eclose eclose_minimal le_eclose le_sup_iff)
qed

lemma eclose_singleton [simp]: "eclose a = (eclose a)  a"
proof (rule order_antisym)
  show "eclose a  eclose a  a"
    by (metis eclose_minimal Transset_eclose Transset_hinsert
              le_eclose less_eq_insert1_iff order_refl zero_le)
next
  show "eclose a  a  eclose a"
    by (metis Transset_def Transset_eclose eclose_minimal le_eclose less_eq_insert1_iff)
qed

lemma eclose_hinsert [simp]: "eclose (b  a) = eclose b  (eclose a  a)"
  by (metis eclose_singleton eclose_sup hinsert_eq_sup)

lemma eclose_succ [simp]: "eclose (succ a) = eclose a  a"
  by (auto simp: succ_def)

lemma fst_in_eclose [simp]: "x  eclose x, y"
  by (metis eclose_hinsert hmem_hinsert hpair_def hunion_iff)

lemma snd_in_eclose [simp]: "y  eclose x, y"
  by (metis eclose_hinsert hmem_hinsert hpair_def hunion_iff)

text ‹Theorem 4.7. rank(x) = rank(cl(x)).›
lemma rank_eclose [simp]: "rank (eclose x) = rank x"
proof (induct x rule: hf_induct)
  case 0 thus ?case by simp
next
  case (hinsert a b) thus ?case
    by simp (metis hinsert_eq_sup succ_def sup.left_idem)
qed


section ‹Epsilon-Recursion›

text ‹Theorem 4.9.  Definition of a function by recursion on rank.›

lemma hmem_induct [case_names step]:
  assumes ih: "x. (y. y  x  P y)  P x" shows "P x"
proof -
  have "y. y  x  P y"
  proof (induct x rule: hf_induct)
    case 0 thus ?case by simp
  next
    case (hinsert a b) thus ?case
      by (metis assms hmem_hinsert)
  qed
  thus ?thesis by (metis ih)
qed

definition
  hmem_rel :: "(hf * hf) set" where
  "hmem_rel = trancl {(x,y). x  y}"

lemma wf_hmem_rel: "wf hmem_rel"
  by (metis hmem_induct hmem_rel_def wfPUNIVI wfP_def wf_trancl)

lemma hmem_eclose_le: "y  x  eclose y  eclose x"
  by (metis Transset_def Transset_eclose eclose_minimal hsubsetD le_eclose)

lemma hmem_rel_iff_hmem_eclose: "(x,y)  hmem_rel  x  eclose y"
proof (unfold hmem_rel_def, rule iffI)
  assume "(x, y)  trancl {(x, y). x  y}"
  thus "x  eclose y"
    proof (induct rule: trancl_induct)
      case (base y) thus ?case
        by (metis hsubsetCE le_eclose mem_Collect_eq split_conv)
    next
      case (step y z) thus ?case
        by (metis hmem_eclose_le hsubsetD mem_Collect_eq split_conv)
    qed
next
  have "Transset x  eclose y. (x, y)  hmem_rel" using Transset_eclose
    by (auto simp: Transset_def hmem_rel_def intro: trancl_trans)
  hence "eclose y  x  eclose y. (x, y)  hmem_rel"
    by (rule eclose_minimal) (auto simp: le_HCollect_iff le_eclose hmem_rel_def)
  moreover assume "x  eclose y"
  ultimately show "(x, y)  trancl {(x, y). x  y}"
    by (metis HCollect_iff hmem_rel_def hsubsetD)
qed

definition hmemrec :: "((hf  'a)  hf  'a)  hf  'a" where
  "hmemrec G  wfrec hmem_rel G"

definition ecut :: "(hf  'a)  hf  hf  'a" where
  "ecut f x  (λy. if y  eclose x then f y else undefined)"

lemma hmemrec: "hmemrec G a = G (ecut (hmemrec G) a) a"
  by (simp add: cut_def ecut_def hmem_rel_iff_hmem_eclose def_wfrec [OF hmemrec_def wf_hmem_rel])

text ‹This form avoids giant explosions in proofs.›
lemma def_hmemrec: "f  hmemrec G  f a = G (ecut (hmemrec G) a) a"
  by (metis hmemrec)

lemma ecut_apply: "y  eclose x  ecut f x y = f y"
  by (metis ecut_def)

lemma RepFun_ecut: "y  z  RepFun y (ecut f z) = RepFun y f"
  by (meson RepFun_cong ecut_apply hsubsetCE le_eclose)

text ‹Now, a stronger induction rule, for the transitive closure of membership›
lemma hmem_rel_induct [case_names step]:
  assumes ih: "x. (y. (y,x)  hmem_rel  P y)  P x" shows "P x"
proof -
  have "y. (y,x)  hmem_rel  P y"
  proof (induct x rule: hf_induct)
    case 0 thus ?case
      by (metis eclose_0 hmem_hempty hmem_rel_iff_hmem_eclose)
  next
    case (hinsert a b)
    thus ?case
      by (metis assms eclose_hinsert hmem_hinsert hmem_rel_iff_hmem_eclose hunion_iff)
  qed
  thus ?thesis  by (metis assms)
qed

lemma rank_HUnion_less:  "x  0  rank (x) < rank x"
proof (induction x rule: hf_induct)
  case 0
  then show ?case by auto
next
  case (hinsert x y)
  then show ?case
    apply (clarsimp simp: Ord_lt_succ_iff_le less_supI2)
    by (metis HUnion_hempty Ord_lt_succ_iff_le Ord_rank hunion_hempty_right less_supI1 less_supI2 rank_sup sup.cobounded2)
qed

corollary Sup_ne: "x  0  x  x"
  by (metis less_irrefl rank_HUnion_less)

end