Theory Mostowski_Collapse

theory Mostowski_Collapse
  imports ZF
begin

section ‹The Mostowski Collapse Theorem›

text ‹
  The Mostowski collapse theorem says that every set-sized well-founded
  extensional relation is isomorphic to membership on a transitive set.  The
  collapsing map is obtained by well-founded recursion:
  each object is sent to the set of the collapses of its predecessors.  We
  work with a set ‹A› and collapse the restriction of a relation ‹r› to
  ‹A›.  The assumptions are therefore ‹wf[A](r)› and extensionality on
  ‹A›; the final isomorphism is stated for ‹r ∩ A*A›.
›

definition extensional_on :: "[i, i] ⇒ o" where
  "extensional_on(A,r) ≡
    ∀x∈A. ∀y∈A. (∀z∈A. ⟨z,x⟩ ∈ r ⟷ ⟨z,y⟩ ∈ r) ⟶ x = y"

definition collapse :: "[i, i, i] ⇒ i" where
  "collapse(A,r,x) ≡
    wfrec[A](r, x, λy f. f `` ((r -`` {y}) ∩ A))"

definition collapse_map :: "[i, i] ⇒ i" where
  "collapse_map(A,r) ≡ (λx∈A. collapse(A,r,x))"

definition collapse_range :: "[i, i] ⇒ i" where
  "collapse_range(A,r) ≡ range(collapse_map(A,r))"

lemma collapse_unfold:
  assumes "wf[A](r)" "x ∈ A"
  shows "collapse(A,r,x) = {collapse(A,r,y). y ∈ (r -`` {x}) ∩ A}"
  unfolding collapse_def
  using assms by (simp add: wfrec_on image_lam)

lemma collapse_memI:
  assumes "wf[A](r)" "x ∈ A" "y ∈ A" "⟨y,x⟩ ∈ r"
  shows "collapse(A,r,y) ∈ collapse(A,r,x)"
proof -
  have "y ∈ (r -`` {x}) ∩ A"
    using assms by (simp add: vimage_singleton_iff)
  with collapse_unfold [OF assms(1,2)] show ?thesis
    by force
qed

lemma collapse_memE:
  assumes "wf[A](r)" "x ∈ A" "u ∈ collapse(A,r,x)"
  obtains y where "y ∈ A" "⟨y,x⟩ ∈ r" "u = collapse(A,r,y)"
  using assms by (auto simp: collapse_unfold vimage_singleton_iff)

lemma collapse_injective:
  assumes wf: "wf[A](r)" and ext: "extensional_on(A,r)"
    and xA: "x ∈ A" and yA: "y ∈ A"
    and eq: "collapse(A,r,x) = collapse(A,r,y)"
  shows "x = y"
proof -
  have "∀y∈A. collapse(A,r,x) = collapse(A,r,y) ⟶ x = y"
    using wf xA
  proof (rule wf_on_induct_raw)
    fix x
    assume xA': "x ∈ A"
      and IH: "∀z∈A. ⟨z,x⟩ ∈ r ⟶
        (∀y∈A. collapse(A,r,z) = collapse(A,r,y) ⟶ z = y)"
    show "∀y∈A. collapse(A,r,x) = collapse(A,r,y) ⟶ x = y"
    proof
      fix y
      assume yA': "y ∈ A"
      show "collapse(A,r,x) = collapse(A,r,y) ⟶ x = y"
      proof
        assume eqxy: "collapse(A,r,x) = collapse(A,r,y)"
        have pred_eq: "∀z∈A. ⟨z,x⟩ ∈ r ⟷ ⟨z,y⟩ ∈ r"
        proof
          fix z
          assume zA: "z ∈ A"
          show "⟨z,x⟩ ∈ r ⟷ ⟨z,y⟩ ∈ r"
          proof
            assume zx: "⟨z,x⟩ ∈ r"
            have "collapse(A,r,z) ∈ collapse(A,r,x)"
              using wf xA' zA zx by (rule collapse_memI)
            then have "collapse(A,r,z) ∈ collapse(A,r,y)"
              using eqxy by simp
            then obtain w where wA: "w ∈ A" and wy: "⟨w,y⟩ ∈ r"
              and zw: "collapse(A,r,z) = collapse(A,r,w)"
              by (rule collapse_memE [OF wf yA'])
            then show "⟨z,y⟩ ∈ r"
              using IH zA zx wA zw by force
          next
            assume zy: "⟨z,y⟩ ∈ r"
            have "collapse(A,r,z) ∈ collapse(A,r,y)"
              using wf yA' zA zy by (rule collapse_memI)
            then have "collapse(A,r,z) ∈ collapse(A,r,x)"
              using eqxy by simp
            then obtain w where wA: "w ∈ A" and wx: "⟨w,x⟩ ∈ r"
              and zw: "collapse(A,r,z) = collapse(A,r,w)"
              by (rule collapse_memE [OF wf xA'])
            then show "⟨z,x⟩ ∈ r"
              using IH zA wx wA zw by force
          qed
        qed
        then show "x = y"
          using ext xA' yA' by (auto simp: extensional_on_def)
      qed
    qed
  qed
  then show ?thesis
    using yA eq by simp
qed

lemma collapse_map_type:
  "collapse_map(A,r) ∈ A → collapse_range(A,r)"
  unfolding collapse_map_def collapse_range_def 
  by (intro lam_type rangeI) (auto simp: lam_def)

lemma collapse_map_apply [simp]:
  "x ∈ A ⟹ collapse_map(A,r) ` x = collapse(A,r,x)"
  by (simp add: collapse_map_def)

lemma collapse_map_inj:
  assumes "wf[A](r)" "extensional_on(A,r)"
  shows "collapse_map(A,r) ∈ inj(A, collapse_range(A,r))"
  unfolding inj_def
proof
  show "collapse_map(A,r) ∈ A → collapse_range(A,r)"
    by (rule collapse_map_type)
next
  show "∀w∈A. ∀x∈A. collapse_map(A,r)`w = collapse_map(A,r)`x ⟶ w = x"
  proof (intro strip)
    fix w x
    assume wA: "w ∈ A" and xA: "x ∈ A" and eq: "collapse_map(A,r)`w = collapse_map(A,r)`x"
    then have "collapse(A,r,w) = collapse(A,r,x)"
      by simp
    then show "w = x"
      by (rule collapse_injective [OF assms wA xA])
  qed
qed

lemma collapse_map_bij:
  assumes "wf[A](r)" "extensional_on(A,r)"
  shows "collapse_map(A,r) ∈ bij(A, collapse_range(A,r))"
  using collapse_map_inj [OF assms]
  unfolding collapse_range_def
  by (rule inj_bij_range)

lemma collapse_range_iff:
  "u ∈ collapse_range(A,r) ⟷ (∃x ∈ A. u = collapse(A,r,x))"
  unfolding collapse_range_def collapse_map_def range_def lam_def
  by blast

lemma collapse_range_transitive:
  assumes wf: "wf[A](r)"
  shows "Transset(collapse_range(A,r))"
  unfolding Transset_def
  by (force simp: collapse_range_iff elim: collapse_memE [OF wf])

lemma collapse_mem_iff:
  assumes wf: "wf[A](r)" and ext: "extensional_on(A,r)"
    and xA: "x ∈ A" and yA: "y ∈ A"
  shows "collapse(A,r,x) ∈ collapse(A,r,y) ⟷ ⟨x,y⟩ ∈ r"
proof
  assume "collapse(A,r,x) ∈ collapse(A,r,y)"
  then obtain z where zA: "z ∈ A" and zy: "⟨z,y⟩ ∈ r"
    and xz: "collapse(A,r,x) = collapse(A,r,z)"
    by (rule collapse_memE [OF wf yA])
  have "x = z"
    using collapse_injective [OF wf ext xA zA xz] .
  then show "⟨x,y⟩ ∈ r"
    using zy by simp
next
  assume "⟨x,y⟩ ∈ r"
  then show "collapse(A,r,x) ∈ collapse(A,r,y)"
    by (rule collapse_memI [OF wf yA xA])
qed

lemma collapse_ord_iso:
  assumes wf: "wf[A](r)" and ext: "extensional_on(A,r)"
  shows "collapse_map(A,r) ∈
    ord_iso(A, r ∩ A*A, collapse_range(A,r), Memrel(collapse_range(A,r)))"
proof (rule ord_isoI)
  show "collapse_map(A,r) ∈ bij(A, collapse_range(A,r))"
    using wf ext by (rule collapse_map_bij)
next
  fix x y
  assume xA: "x ∈ A" and yA: "y ∈ A"
  show "⟨x,y⟩ ∈ r ∩ A*A ⟷
      ⟨collapse_map(A,r)`x, collapse_map(A,r)`y⟩ ∈ Memrel(collapse_range(A,r))"
    using xA yA collapse_mem_iff [OF wf ext xA yA]
    by (auto simp: collapse_range_iff)
qed

theorem mostowski_collapse:
  assumes "wf[A](r)" "extensional_on(A,r)"
  shows "Transset(collapse_range(A,r)) ∧
    collapse_map(A,r) ∈
      ord_iso(A, r ∩ A*A, collapse_range(A,r), Memrel(collapse_range(A,r)))"
  using assms
  by (simp add: collapse_range_transitive collapse_ord_iso)

theorem mostowski_collapse_exists:
  assumes "wf[A](r)" "extensional_on(A,r)"
  shows "∃M f. Transset(M) ∧ f ∈ ord_iso(A, r ∩ A*A, M, Memrel(M))"
  using mostowski_collapse [OF assms] by blast

lemma collapse_unique:
  assumes wf: "wf[A](r)"
    and ftype: "f ∈ A → B"
    and frec: "⋀x. x ∈ A ⟹ f`x = f `` ((r -`` {x}) ∩ A)"
    and xA: "x ∈ A"
  shows "f`x = collapse(A,r,x)"
  using wf xA
proof (rule wf_on_induct_raw)
  fix x
  assume xA': "x ∈ A"
    and IH: "∀y∈A. ⟨y,x⟩ ∈ r ⟶ f ` y = collapse(A,r,y)"
  have "f`x = f `` ((r -`` {x}) ∩ A)"
    using frec xA' by simp
  also have "... = {collapse(A,r,y). y ∈ (r -`` {x}) ∩ A}"
  proof (rule equalityI)
    show "f `` ((r -`` {x}) ∩ A) ⊆
      {collapse(A,r,y). y ∈ (r -`` {x}) ∩ A}"
    proof
      fix u
      assume "u ∈ f `` ((r -`` {x}) ∩ A)"
      then obtain y where pair: "⟨y,u⟩ ∈ f"
        and ypred: "y ∈ (r -`` {x}) ∩ A"
        by (rule imageE)
      have uy: "u = f`y"
        using pair ftype by (simp add: apply_equality)
      have "f`y = collapse(A,r,y)"
        using IH ypred by (simp add: vimage_singleton_iff)
      then have "u = collapse(A,r,y)"
        using uy by simp
      moreover have "y ∈ (r -`` {x}) ∩ A"
        by (rule ypred)
      ultimately show "u ∈ {collapse(A,r,y). y ∈ (r -`` {x}) ∩ A}"
        by (rule RepFun_eqI)
    qed
  next
    show "{collapse(A,r,y). y ∈ (r -`` {x}) ∩ A} ⊆
      f `` ((r -`` {x}) ∩ A)"
    proof
      fix u
      assume "u ∈ {collapse(A,r,y). y ∈ (r -`` {x}) ∩ A}"
      then obtain y where ypred: "y ∈ (r -`` {x}) ∩ A"
        and uy: "u = collapse(A,r,y)"
        by (rule RepFunE)
      have "y ∈ A"
        using ypred by simp
      then have pair: "⟨y,f`y⟩ ∈ f"
        by (rule apply_Pair [OF ftype])
      have "f`y = collapse(A,r,y)"
        using IH ypred by (simp add: vimage_singleton_iff)
      then have "⟨y,u⟩ ∈ f"
        using uy pair by simp
      then show "u ∈ f `` ((r -`` {x}) ∩ A)"
        using ypred by (rule imageI)
    qed
  qed
  also have "... = collapse(A,r,x)"
    using collapse_unfold [OF wf xA'] by simp
  finally show "f`x = collapse(A,r,x)" .
qed

lemma collapse_map_unique:
  assumes wf: "wf[A](r)"
    and ftype: "f ∈ A → B"
    and frec: "⋀x. x ∈ A ⟹ f`x = f `` ((r -`` {x}) ∩ A)"
  shows "f = collapse_map(A,r)"
  unfolding collapse_map_def
  using collapse_unique [OF wf ftype frec]
  by (force intro: fun_extension ftype lam_type)

lemma collapse_range_unique:
  assumes wf: "wf[A](r)"
    and ftype: "f ∈ A → B"
    and frec: "⋀x. x ∈ A ⟹ f`x = f `` ((r -`` {x}) ∩ A)"
    and M: "M = range(f)"
  shows "M = collapse_range(A,r)"
  using collapse_map_unique [OF wf ftype frec] M
  unfolding collapse_range_def by simp

end