Theory Universe_Interps

(*  Title:       Universe_Interps
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2026
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

chapter "Interpretations of ‹universe›"

theory Universe_Interps
imports Universe ZFC_in_HOL.ZFC_Cardinals
begin

  text‹
    In this section we give two interpretations of locales defined in
    theory ‹Universe›.  In one interpretation, ``finite'' is taken as
    the notion of smallness and the set of natural numbers is used to interpret the
    @{locale tupling} locale.
    In the second interpretation, the notion ``small'' is as defined in ‹ZFC_in_HOL›
    and the set of elements of the type ‹V› defined in that theory is used as the universe.
    This interpretation interprets the @{locale universe} locale, which augments
    @{locale universe} with the assumption @{locale small_nat} that the set of natural numbers
    is small.
    The purpose of constructing these interpretations is to show the consistency of the
    @{locale universe} locale assumptions (relative, of course to the consistency of
    HOL itself, and of HOL as extended in ‹ZFC_in_HOL›), as well as to provide a
    starting point for the construction of large categories, such as the category of small sets
    which is treated in this article.
  ›

  section "Interpretation using Natural Numbers"

  text‹
    We first give an interpretation for the @{locale tupling} locale, taking the set of natural
    numbers as the universe and taking ``finite'' as the meaning of ``small''.
  ›

  context
  begin

    text‹
      We first establish properties of ‹finite :: nat set ⇒ bool› as our notion of smallness.
    ›

    interpretation smallness ‹finite :: nat set ⇒ bool›
      by unfold_locales (meson finite_surj lepoll_iff)

    text‹
      The notion @{term small} defined by the @{locale smallness} locale agrees with the notion
      ‹finite› given as a locale parameter.
    ›

    lemma finset_small_iff_finite:
    shows "local.small X ⟷ finite X"
      by (metis eqpoll_finite_iff eqpoll_iff_finite_card local.small_def)

    interpretation small_finite ‹finite :: nat set ⇒ bool›
      by unfold_locales blast

    lemma small_finite_finset:
    shows "small_finite (finite :: nat set ⇒ bool)"
      ..

    interpretation small_product ‹finite :: nat set ⇒ bool›
      using eqpoll_iff_finite_card by unfold_locales auto

    lemma small_product_finset:
    shows "small_product (finite :: nat set ⇒ bool)"
      ..

    interpretation small_sum ‹finite :: nat set ⇒ bool›
      by unfold_locales (meson eqpoll_iff_finite_card finite_SigmaI finite_lessThan)

    lemma small_sum_finset:
    shows "small_sum (finite :: nat set ⇒ bool)"
      ..

    interpretation small_powerset ‹finite :: nat set ⇒ bool›
      using eqpoll_iff_finite_card by unfold_locales blast

    lemma small_powerset_finset:
    shows "small_powerset (finite :: nat set ⇒ bool)"
      ..

    interpretation small_funcset ‹finite :: nat set ⇒ bool› ..

    text‹
      As expected, the assumptions of locale @{locale small_nat} are inconsistent with
      the present context.
    ›

    lemma large_nat_finset:
    shows "¬ local.small (UNIV :: nat set)"
      using finset_small_iff_finite large_UNIV by blast

    text‹
      Next, we develop embedding properties of ‹UNIV :: nat set›.
    ›

    interpretation embedding ‹UNIV :: nat set› .

    interpretation lifting ‹UNIV :: nat set›
      by unfold_locales blast

    lemma nat_admits_lifting:
    shows "lifting (UNIV :: nat set)"
      ..

    interpretation pairing ‹UNIV :: nat set›
      by unfold_locales blast

    lemma nat_admits_pairing:
    shows "pairing (UNIV :: nat set)"
      ..

    interpretation powering ‹finite :: nat set ⇒ bool› ‹UNIV :: nat set›
      using inj_on_set_encode small_iff_sml
      by unfold_locales auto

    lemma nat_admits_finite_powering:
    shows "powering (finite :: nat set ⇒ bool) (UNIV :: nat set)"
      ..

    interpretation tupling ‹finite :: nat set ⇒ bool› ‹UNIV :: nat set› ..

    lemma nat_admits_finite_tupling:
    shows "tupling (finite :: nat set ⇒ bool) (UNIV :: nat set)"
      ..

  end

  text‹
    Finally, we give the interpretation of the @{locale tupling} locale, stated in the top-level
    context in order to make it clear that it can be established directly in HOL, without
    depending somehow on any underlying locale assumptions.
  ›

  interpretation nat_tupling: tupling ‹finite :: nat set ⇒ bool› ‹UNIV :: nat set› undefined
    using nat_admits_finite_tupling by blast

  section "Interpretation using ‹ZFC_in_HOL›"

  text‹
    We now give an interpretation for the @{locale universe} locale, taking as the universe the
    set of elements of type ‹V› defined in ‹ZFC_in_HOL› as the universe and
    using the notion @{term ZFC_in_HOL.small} also defined in that theory.
  ›

  context
  begin

    text‹
      We first develop properties of @{term ZFC_in_HOL.small}, which we take
      as our notion of smallness.
    ›

    interpretation smallness ‹ZFC_in_HOL.small :: V set ⇒ bool›
      using lepoll_small by unfold_locales blast

    text‹
      The notion @{term local.small} defined by the @{locale smallness} locale agrees
      with the notion @{term ZFC_in_HOL.small} given as a locale parameter.
    ›

    lemma small_iff_ZFC_small:
    shows "local.small X ⟷ ZFC_in_HOL.small X"
      by (metis eqpoll_sym local.small_def small_eqpoll small_iff)

    interpretation small_finite ‹ZFC_in_HOL.small :: V set ⇒ bool›
      by unfold_locales
         (meson eqpoll_sym finite_atLeastAtMost finite_imp_small small_elts small_eqpoll)

    lemma small_finite_ZFC:
    shows "small_finite (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    interpretation small_product ‹ZFC_in_HOL.small :: V set ⇒ bool›
      by unfold_locales (metis eqpoll_sym small_Times small_elts small_eqpoll)

    lemma small_product_ZFC:
    shows "small_product (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    interpretation small_sum ‹ZFC_in_HOL.small :: V set ⇒ bool›
      by unfold_locales (meson eqpoll_sym small_Sigma small_elts small_eqpoll)

    lemma small_sum_ZFC:
    shows "small_sum (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    text‹
      We need the following, which does not seem to be directly available in
      ‹ZFC_in_HOL›.
    ›

    lemma ZFC_small_implies_small_powerset:
    fixes X
    assumes "ZFC_in_HOL.small X"
    shows "ZFC_in_HOL.small (Pow X)"
    proof -
      obtain f v where f: "inj_on f X ∧ f ` X = elts v"
        using assms imageE ZFC_in_HOL.small_def by meson
      obtain f' where f': "inj_on f' (Pow X) ∧ f' ` (Pow X) = Pow (elts v)"
        using f image_Pow_surj inj_on_image_Pow by metis
      have "ZFC_in_HOL.small (f' ` (Pow X))"
        using assms f' ZFC_in_HOL.small_image_iff [of f' "Pow X"]
        by (metis Pow_iff down elts_VPow inj_onCI inj_on_image_eqpoll_self set_injective
            small_eqpoll)
      moreover have "eqpoll (f' ` (Pow X)) (Pow X)"
        using f' eqpoll_sym inj_on_image_eqpoll_self by meson
      ultimately show "ZFC_in_HOL.small (Pow X)"
        by (metis image_iff inj_on_image_eqpoll_1 ZFC_in_HOL.small_def small_eqpoll)
    qed

    interpretation small_powerset ‹ZFC_in_HOL.small :: V set ⇒ bool›
      by unfold_locales
         (meson eqpoll_sym gcard_eqpoll small_iff ZFC_small_implies_small_powerset)

    lemma small_powerset_ZFC:
    shows "small_powerset (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    interpretation small_funcset ‹ZFC_in_HOL.small :: V set ⇒ bool› ..

    lemma small_funcset_ZFC:
    shows "small_funcset (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    interpretation small_nat ‹ZFC_in_HOL.small :: V set ⇒ bool›
    proof -
      have "ZFC_in_HOL.small (UNIV :: nat set)"
        using small_image_nat by (metis surj_id)
      thus "small_nat (ZFC_in_HOL.small :: V set ⇒ bool)"
        using gcard_eqpoll by unfold_locales auto
    qed

    lemma small_nat_ZFC:
    shows "small_nat (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    interpretation small_funcset_and_nat ‹ZFC_in_HOL.small :: V set ⇒ bool› ..

    lemma small_funcset_and_nat_ZFC:
    shows "small_funcset_and_nat (ZFC_in_HOL.small :: V set ⇒ bool)"
      ..

    text‹
      Next, we develop embedding properties of ‹UNIV :: V set›.
    ›

    interpretation embedding ‹UNIV :: V set› .

    interpretation lifting ‹UNIV :: V set›
    proof
      let ?ι = "λ None ⇒ ZFC_in_HOL.set {}
                | Some x ⇒ ZFC_in_HOL.set {x}"
      have "is_embedding_of ?ι ({None} ∪ Some ` UNIV)"
      proof
        show "?ι ` ({None} ∪ Some ` UNIV) ⊆ UNIV" by blast
        show "inj_on ?ι ({None} ∪ Some ` UNIV)"
        proof
          fix x y
          assume x: "x ∈ {None :: V option} ∪ Some ` UNIV"
          assume y: "y ∈ {None :: V option} ∪ Some ` UNIV"
          assume eq: "?ι x = ?ι y"
          show "x = y"
            by (metis (no_types, lifting) elts_of_set eq insert_not_empty option.case_eq_if
                option.collapse range_constant singleton_eq_iff small_image_nat)
        qed
      qed
      thus "∃ι :: V option ⇒ V. is_embedding_of ι ({None} ∪ Some ` UNIV)"
        by blast
    qed

    lemma V_admits_lifting:
    shows "lifting (UNIV :: V set)"
      ..

    interpretation pairing ‹UNIV :: V set›
    proof
      show "∃ι :: V × V ⇒ V. is_embedding_of ι (UNIV × UNIV)"
        using inj_on_vpair by blast
    qed

    lemma V_admits_pairing:
    shows "pairing (UNIV :: V set)"
      ..

    interpretation powering ‹ZFC_in_HOL.small :: V set => bool› ‹UNIV :: V set›
    proof
      show "∃ι :: V set ⇒ V. is_embedding_of ι {X. X ⊆ UNIV ∧ local.small X}"
        using inj_on_set small_iff_sml by auto
    qed

    lemma V_admits_small_powering:
    shows "powering (ZFC_in_HOL.small :: V set => bool) (UNIV :: V set)"
      ..

    interpretation tupling ‹ZFC_in_HOL.small :: V set => bool› ‹UNIV :: V set› undefined ..

    lemma V_admits_small_tupling:
    shows "tupling (ZFC_in_HOL.small :: V set => bool) (UNIV :: V set)"
      ..

    interpretation universe ‹ZFC_in_HOL.small :: V set => bool› ‹UNIV :: V set› undefined ..

    theorem V_is_universe:
    shows "universe (ZFC_in_HOL.small :: V set => bool) (UNIV :: V set)"
      ..

  end

  text‹
    Finally, we give the interpretation of the @{locale universe} locale, stated in the top-level
    context.  Note however, that this is proved not in ``vanilla HOL'', but rather in HOL as
    extended by the axiomatization in ‹ZFC_in_HOL›.
  ›

  interpretation ZFC_universe: universe ‹ZFC_in_HOL.small :: V set => bool› ‹UNIV :: V set› undefined
    using V_is_universe by blast

end