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) ≤ rank⦃a⦄"
        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"x≤y"}.›


section ‹Epsilon Closure›

definition
  eclose    :: "hf ⇒ hf"  where
    "eclose X = ⨅ ⦃Y ❙∈ HPow(Vset (rank X)). Transset Y ∧ X≤Y⦄"

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 ∧ X≤Y⦄ ≠ 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" "X≤Y" shows "eclose X ≤ Y"
proof -
  have "⦃Y ❙∈ HPow(Vset (rank X)). Transset Y ∧ X≤Y⦄ ≠ 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