Theory CZH_Sets_ZQR

(* Copyright 2021 (C) Mihails Milehins *)

section‹
Construction of integer numbers, rational numbers and real numbers
›
theory CZH_Sets_ZQR
  imports
    "HOL-Library.Rewrite"
    CZH_Sets_NOP
    CZH_Sets_VNHS
    "Cardinality_Continuum.Cardinality_Continuum"
begin



subsection‹Background›


text‹

The set of real numbers  is defined in a way such that it agrees 
with the set of natural numbers constω. However, otherwise, 
real numbers are allowed to be arbitrary sets 
in termVset (ω + ω).\footnote{
The idea itself is not new, e.g., see cite"chen_hotg_2021".
}
Integer and rational numbers are exposed via canonical injections into
the set of real numbers from the types typint and typrat, respectively.
Lastly, common operations on the real, integer and rational numbers
are defined and some of their main properties are exposed. 

The primary reference for this section is the textbook
The Real Numbers and Real Analysis› by E. Bloch
cite"bloch_real_2010". Nonetheless, it is not claimed that the exposition of 
the subject presented in this section is entirely congruent with the exposition
in the aforementioned reference.

›

declare One_nat_def[simp del]

named_theorems vnumber_simps

lemmas [vnumber_simps] =  
  Collect_mem_eq Ball_def[symmetric] Bex_def[symmetric] vsubset_eq[symmetric]


text‹
Supplementary material for the evaluation of the upper bound of the
cardinality of the continuum.
›

lemma inj_image_ord_of_nat: "inj (image ord_of_nat)"
  by (intro injI) (simp add: inj_image_eq_iff inj_ord_of_nat)

lemma vlepoll_VPow_omega_if_vreal_lepoll_real:
  assumes "x  (UNIV::real set)" 
  shows "set x  VPow ω"
proof-
  note assms
  also from eqpoll_UNIV_real have "  (UNIV::nat set set)"
    unfolding Pow_UNIV by (simp add: eqpoll_imp_lepoll)
  also from inj_image_ord_of_nat have "  Pow (elts ω)"
    unfolding lepoll_def by auto
  also from down have "  elts (VPow ω)"
    unfolding lepoll_def
    by (intro exI[of _ set] conjI inj_onI) (auto simp: elts_VPow)
  finally show "set x  VPow ω" by simp
qed



subsection‹Real numbers›


subsubsection‹Definition›

abbreviation real :: "nat  real"
  where "real  of_nat"

definition nat_of_real :: "real  nat"
  where "nat_of_real = inv_into UNIV real"

definition vreal_of_real_impl :: "real  V"
  where "vreal_of_real_impl = (SOME V_of::realV. inj V_of)"

lemma inj_vreal_of_real_impl: "inj vreal_of_real_impl" 
  unfolding vreal_of_real_impl_def 
  by (metis embeddable_class.ex_inj verit_sko_ex')

lemma inj_on_inv_vreal_of_real_impl: 
  "inj_on (inv vreal_of_real_impl) (range vreal_of_real_impl)"
  by (intro inj_onI) (fastforce intro: inv_into_injective)

lemma range_vreal_of_real_impl_vlepoll_VPow_omega: 
  "set (range vreal_of_real_impl)  VPow ω"
proof-
  have "range vreal_of_real_impl  (UNIV::real set)"
    unfolding lepoll_def by (auto intro: inj_on_inv_vreal_of_real_impl)
  from vlepoll_VPow_omega_if_vreal_lepoll_real[OF this] show ?thesis .
qed

definition vreal_impl :: V
  where "vreal_impl =
    (
      SOME y. 
        range vreal_of_real_impl  elts y 
        vdisjnt y ω 
        y  Vset (ω + ω)
    )"

lemma vreal_impl_eqpoll: "range vreal_of_real_impl  elts vreal_impl" 
  and vreal_impl_vdisjnt: "vdisjnt vreal_impl ω"
  and vreal_impl_in_Vset_ss_omega: "vreal_impl  Vset (ω + ω)"
proof-
  from Ord_ω have VPow_in_Vset: "VPow ω  Vset (succ (succ ω))"
    by (intro Ord_VPow_in_Vset_succI) 
      (auto simp: less_TC_succ Ord_iff_rank VsetI)
  have [simp]: "small (range vreal_of_real_impl)" by simp
  then obtain x where x: "range vreal_of_real_impl = elts x"
    unfolding small_iff by clarsimp
  from range_vreal_of_real_impl_vlepoll_VPow_omega[unfolded x] have 
    "x  VPow ω" 
    by simp
  then obtain f where "v11 f" and "𝒟 f = x" and " f  VPow ω" by auto
  moreover have Oω2: "Ord (succ (succ ω))" by auto
  ultimately have x_Rf: "x   f" and " f  Vset (succ (succ ω))"
    by (auto intro: VPow_in_Vset)
  then have "ω   f  Vset (succ (succ ω))" and " f  ω   f"
    by (auto simp: VPow_in_Vset VPow_in_Vset_revD vunion_in_VsetI)
  from Ord_ex_eqpoll_vdisjnt[OF Oω2 this(2,1)] obtain z
    where Rf_z: " f  z" 
      and "vdisjnt z (ω   f)"
      and z: "z  Vset (succ (succ (succ ω)))"
    by auto
  then have vdisjnt_zω: "vdisjnt z ω" 
    and z_ssssω: "z  Vset (succ (succ (succ (succ ω))))"    
    by 
      (
        auto simp: 
          vdisjnt_vunion_right vsubset_in_VsetI Ord_succ Ord_Vset_in_Vset_succI
      )
  have "Limit (ω + ω)" by simp
  then have "succ (succ (succ (succ ω)))  ω + ω"
    by (metis Limit_def add.right_neutral add_mem_right_cancel Limit_omega)
  then have "Vset (succ (succ (succ (succ ω))))  Vset (ω + ω)"
    by (simp add: Vset_in_mono)
  with z z_ssssω have "z  Vset (ω + ω)" by auto
  moreover from x_Rf Rf_z have "range vreal_of_real_impl  elts z"
    unfolding x by (auto intro: eqpoll_trans)
  ultimately show "range vreal_of_real_impl  elts vreal_impl" 
    and "vdisjnt vreal_impl ω"
    and "vreal_impl  Vset (ω + ω)"
    using vdisjnt_zω 
    unfolding vreal_impl_def
    by (metis (mono_tags, lifting) verit_sko_ex')+
qed

definition vreal_of_real_impl' :: "V  V"
  where "vreal_of_real_impl' = 
    (SOME f. bij_betw f (range vreal_of_real_impl) (elts vreal_impl))"

lemma vreal_of_real_impl'_bij_betw: 
  "bij_betw vreal_of_real_impl' (range vreal_of_real_impl) (elts vreal_impl)"
proof-
  from eqpoll_def obtain f where f: 
    "bij_betw f (range vreal_of_real_impl) (elts vreal_impl)"
    by (auto intro: vreal_impl_eqpoll)
  then show ?thesis unfolding vreal_of_real_impl'_def by (metis verit_sko_ex')
qed

definition vreal_of_real_impl'' :: "real  V"
  where "vreal_of_real_impl'' = vreal_of_real_impl'  vreal_of_real_impl"

lemma vreal_of_real_impl'': "disjnt (range vreal_of_real_impl'') (elts ω)"
proof-
  from comp_apply vreal_impl_vdisjnt vreal_of_real_impl'_bij_betw have 
    "vreal_of_real_impl'' y  ω" for y
    unfolding vreal_of_real_impl''_def by fastforce
  then show ?thesis unfolding disjnt_iff by clarsimp
qed

lemma inj_vreal_of_real_impl'': "inj vreal_of_real_impl''"
  unfolding vreal_of_real_impl''_def 
  by 
    (
      meson 
        bij_betwE 
        comp_inj_on 
        inj_vreal_of_real_impl 
        vreal_of_real_impl'_bij_betw
    )


text‹Main definitions.›

definition vreal_of_real :: "real  V"
  where "vreal_of_real x = 
    (if x   then (nat_of_real x) else vreal_of_real_impl'' x)"

notation vreal_of_real (‹_ [1000] 999)

declare [[coercion "vreal_of_real :: real  V"]]

definition vreal :: V ()
  where "vreal = set (range vreal_of_real)"

definition real_of_vreal :: "V  real"
  where "real_of_vreal = inv_into UNIV vreal_of_real"


text‹Rules.›

lemma vreal_of_real_in_vrealI[intro, simp]: "a  " 
  by (simp add: vreal_def)

lemma vreal_of_real_in_vrealE[elim]:
  assumes "a  "
  obtains b where "b = a"
  using assms unfolding vreal_def by auto


text‹Elementary properties.›

lemma vnat_eq_vreal: "x = x" by (simp add: nat_of_real_def vreal_of_real_def)

lemma omega_vsubset_vreal: "ω  "
proof
  fix x assume "x  ω"
  with nat_of_omega obtain y where x_def: "x = y" by auto
  then have "vreal_of_real (real y) = (nat_of_real (real y))" 
    unfolding vreal_of_real_def by simp
  moreover have "(nat_of_real (real y)) = x"
    by (simp add: nat_of_real_def x_def)
  ultimately show "x  " unfolding vreal_def by clarsimp
qed

lemma inj_vreal_of_real: "inj vreal_of_real"
proof
  fix x y assume prems: "vreal_of_real x = vreal_of_real y"
  consider 
    (xy) x    y   | 
    (x_ny) x    y   | 
    (nx_y) x    y   | 
    (nxy) x    y    
    by auto 
  then show "x = y"
  proof cases
    case xy
    then have "(nat_of_real x) = (nat_of_real y)"
      using vreal_of_real_def prems by simp
    then show ?thesis
      by (metis Nats_def f_inv_into_f nat_of_real_def ord_of_nat_inject xy)
  next
    case x_ny
    with prems have eq: "(nat_of_real x) = vreal_of_real_impl'' y"
      unfolding vreal_of_real_def by simp
    have "vreal_of_real_impl'' y  ω"
      by (meson disjnt_iff rangeI vreal_of_real_impl'')
    then show ?thesis unfolding eq[symmetric] by auto
  next
    case nx_y
    with prems have eq: "(nat_of_real y) = vreal_of_real_impl'' x"
      unfolding vreal_of_real_def by simp
    have "vreal_of_real_impl'' x  ω"
      by (meson disjnt_iff rangeI vreal_of_real_impl'')
    then show ?thesis unfolding eq[symmetric] by auto
  next
    case nxy
    then have "x  " and "y  " by auto
    with prems 
    have "vreal_of_real_impl'' x = vreal_of_real_impl'' y"
      unfolding vreal_of_real_def by simp
    then show ?thesis by (meson inj_def inj_vreal_of_real_impl'')
  qed
qed

lemma vreal_in_Vset_ω2: "  Vset (ω + ω)"
  unfolding vreal_def
proof-
  have "set (range vreal_of_real)  set (range vreal_of_real_impl'')  ω"
    unfolding vreal_of_real_def by auto
  moreover from vreal_of_real_impl'_bij_betw have 
    "set (range vreal_of_real_impl'')  vreal_impl"
    unfolding vreal_of_real_impl''_def by fastforce
  ultimately show "set (range vreal_of_real)  Vset (ω + ω)"
    using Ord_ω Ord_add 
    by 
      ( 
        auto simp: 
          Ord_iff_rank 
          Ord_VsetI
          vreal_impl_in_Vset_ss_omega 
          vsubset_in_VsetI 
          vunion_in_VsetI
      )
qed

lemma real_of_vreal_vreal_of_real[simp]: "real_of_vreal (a) = a"
  by (simp add: inj_vreal_of_real real_of_vreal_def)


subsubsection‹Transfer rules›

definition cr_vreal :: "V  real  bool"
  where "cr_vreal a b  (a = vreal_of_real b)"

lemma cr_vreal_right_total[transfer_rule]: "right_total cr_vreal"
  unfolding cr_vreal_def right_total_def by simp

lemma cr_vreal_bi_uniqie[transfer_rule]: "bi_unique cr_vreal"
  unfolding cr_vreal_def bi_unique_def
  by (simp add: inj_eq inj_vreal_of_real)

lemma cr_vreal_transfer_domain_rule[transfer_domain_rule]: 
  "Domainp cr_vreal = (λx. x  )"
  unfolding cr_vreal_def by force

lemma vreal_transfer[transfer_rule]: 
  "(rel_set cr_vreal) (elts ) (UNIV::real set)"
  unfolding cr_vreal_def rel_set_def by auto

lemma vreal_of_real_transfer[transfer_rule]: "cr_vreal (vreal_of_real a) a"
  unfolding cr_vreal_def by auto


subsubsection‹Constants and operations›


text‹Auxiliary.›

lemma vreal_fsingleton_in_fproduct_vreal: "[a]   ^× 1" by auto

lemma vreal_fpair_in_fproduct_vreal: "[a, b]   ^× 2" by force


text‹Zero.›

lemma vreal_zero: "0 = (0::V)" 
  by (simp add: ord_of_nat_vempty vnat_eq_vreal)


text‹One.›

lemma vreal_one: "1 = (1::V)" 
  by (simp add: ord_of_nat_vone vnat_eq_vreal)


text‹Addition.›

definition vreal_plus :: V 
  where "vreal_plus = 
    (λx ^× 2. (real_of_vreal (x0) + real_of_vreal (x1)))"

abbreviation vreal_plus_app :: "V  V  V" (infixl "+" 65)
  where "vreal_plus_app a b  vreal_plusa, b"
notation vreal_plus_app (infixl "+" 65)

lemma vreal_plus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal ===> cr_vreal) 
    (+) (+)"
  using vreal_fpair_in_fproduct_vreal 
  by (intro rel_funI, unfold vreal_plus_def cr_vreal_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Multiplication.›

definition vreal_mult :: V 
  where "vreal_mult = 
    (λx ^× 2. (real_of_vreal (x0) * real_of_vreal (x1)))"

abbreviation vreal_mult_app (infixl "*" 70) 
  where "vreal_mult_app a b  vreal_multa, b"
notation vreal_mult_app (infixl "*" 70)

lemma vreal_mult_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal ===> cr_vreal) (*) (*)"
  using vreal_fpair_in_fproduct_vreal 
  by (intro rel_funI, unfold vreal_mult_def cr_vreal_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Unary minus.›

definition vreal_uminus :: V 
  where "vreal_uminus = (λx. (uminus (real_of_vreal x)))"

abbreviation vreal_uminus_app (- _› [81] 80) 
  where "- a  vreal_uminusa"

lemma vreal_uminus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal) (vreal_uminus_app) (uminus)"
  using vreal_fsingleton_in_fproduct_vreal
  by (intro rel_funI, unfold vreal_uminus_def cr_vreal_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Multiplicative inverse.›

definition vreal_inverse :: V 
  where "vreal_inverse = (λx. (inverse (real_of_vreal x)))"

abbreviation vreal_inverse_app ((_¯) [1000] 999) 
  where "a¯  vreal_inversea"

lemma vreal_inverse_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal) (vreal_inverse_app) (inverse)"
  using vreal_fsingleton_in_fproduct_vreal 
  by (intro rel_funI, unfold vreal_inverse_def cr_vreal_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Order.›

definition vreal_le :: V 
  where "vreal_le =
    set {[a, b] | a b. [a, b]   ^× 2  real_of_vreal a  real_of_vreal b}"

abbreviation vreal_le' ((_/  _)  [51, 51] 50)
  where "a  b  [a, b]  vreal_le"

lemma small_vreal_le[simp]: 
  "small 
    {[a, b] | a b. [a, b]   ^× 2  real_of_vreal a  real_of_vreal b}"
proof-
  have small: "small {[a, b] | a b. [a, b]   ^× 2}" by simp
  show ?thesis by (rule smaller_than_small[OF small]) auto
qed

lemma vreal_le_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal ===> (=)) vreal_le' (≤)"
  using vreal_fsingleton_in_fproduct_vreal 
  by (intro rel_funI, unfold cr_scalar_def cr_vreal_def vreal_le_def)
    (auto simp: nat_omega_simps)


text‹Strict order.›

definition vreal_ls :: V 
  where "vreal_ls =
    set {[a, b] | a b. [a, b]   ^× 2  real_of_vreal a < real_of_vreal b}"

abbreviation vreal_ls' ((_/ < _) [51, 51] 50)
  where "a < b  [a, b]  vreal_ls"

lemma small_vreal_ls[simp]: 
  "small 
    {[a, b] | a b. [a, b]   ^× 2  real_of_vreal a < real_of_vreal b}"
proof-
  have small: "small {[a, b] | a b. [a, b]   ^× 2}" by simp
  show ?thesis by (rule smaller_than_small[OF small]) auto
qed

lemma vreal_ls_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal ===> (=)) vreal_ls' (<)"
  by (intro rel_funI, unfold cr_scalar_def cr_vreal_def vreal_ls_def)
    (auto simp: nat_omega_simps)
  

text‹Subtraction.›

definition vreal_minus :: V 
  where "vreal_minus =
    (λx ^× 2. (real_of_vreal (x0) - real_of_vreal (x1)))"

abbreviation vreal_minus_app (infixl "-" 65) 
  where "vreal_minus_app a b  vreal_minusa, b"

lemma vreal_minus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vreal ===> cr_vreal ===> cr_vreal) (-) (-)"
  using vreal_fpair_in_fproduct_vreal 
  by (intro rel_funI, unfold vreal_minus_def cr_vreal_def cr_scalar_def) 
    (simp add: nat_omega_simps)


subsubsection‹Axioms of an ordered field with the least upper bound property.›


text‹
The exposition follows the Definitions 2.2.1 and 2.2.3 from 
the textbook The Real Numbers and Real Analysis› by E. Bloch
cite"bloch_real_2010".
›

lemma vreal_zero_closed: "0  "
proof-
  have "(0::real)  UNIV" by simp
  from this[untransferred] show ?thesis.
qed

lemma vreal_one_closed: "1  "
proof-
  have "(1::real)  UNIV" by simp
  from this[untransferred] show ?thesis.
qed

lemma vreal_plus_closed: 
  assumes "x  " and "y  " 
  shows "x + y  "
proof-
  have "x' + y'  UNIV" for x' y' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vreal_uminus_closed: 
  assumes "x  "
  shows "- x  "
proof-
  have "-x'  UNIV" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vreal_mult_closed:
  assumes "x  " and "y  " 
  shows "x * y  "
proof-
  have "x' * y'  UNIV" for x' y' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vreal_inverse_closed: 
  assumes "x  "
  shows "x¯  "
proof-    
  have "inverse x'  UNIV" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Associative Law for Addition: Definition 2.2.1.a.›

lemma vreal_assoc_law_addition: 
  assumes "x  " and "y  " and "z  " 
  shows "(x + y) + z = x + (y + z)"
proof-
  have "(x' + y') + z' = x' + (y' + z')" for x' y' z' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Commutative Law for Addition: Definition 2.2.1.b.›

lemma vreal_commutative_law_addition:
  assumes "x  " and "y  " 
  shows "x + y = y + x"
proof-
  have "(x' + y') = y' + x' " for x' y' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Identity Law for Addition: Definition 2.2.1.c.›

lemma vreal_identity_law_addition:
  assumes "x  "
  shows "x + 0 = x"
proof-
  have "x' + 0 = x'" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Inverses Law for Addition: Definition 2.2.1.d.›

lemma vreal_inverses_law_addition:
  assumes "x  "
  shows "x + (- x) = 0"
proof-
  have "x' + (-x') = 0" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Associative Law for Multiplication: Definition 2.2.1.e.›

lemma vreal_assoc_law_multiplication: 
  assumes "x  " and "y  " and "z  "
  shows "(x * y) * z = x * (y * z)"
proof-
  have "(x' * y') * z' = x' * (y' * z')" for x' y' z' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Commutative Law for Multiplication: Definition 2.2.1.f.›

lemma vreal_commutative_law_multiplication:
  assumes "x  " and "y  " 
  shows "x * y = y * x"
proof-
  have "(x' * y') = y' * x' " for x' y' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Identity Law for Multiplication: Definition 2.2.1.g.›

lemma vreal_identity_law_multiplication:
  assumes "x  "
  shows "x * 1 = x"
proof-
  have "x' * 1 = x'" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Inverses Law for Multiplication: Definition 2.2.1.h.›

lemma vreal_inverses_law_multiplication:
  assumes "x  " and "x  0" 
  shows "x * x¯ = 1"
proof-
  have "x'  0  x' * inverse x' = 1" for x' :: real by simp  
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Distributive Law: Definition 2.2.1.i.›

lemma vreal_distributive_law:
  assumes "x  " and "y  " and "z  "
  shows "x * (y + z) = x * y + x * z"
proof-
  have "x' * (y' + z') = (x' * y') + (x' * z')" for x' y' z' :: real 
    by (simp add: field_simps)
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Trichotomy Law: Definition 2.2.1.j.›

lemma vreal_trichotomy_law:
  assumes "x  " "y  "
  shows 
    "(x < y  ~(x = y)  ~(y < x))  
    (~(x < y)  x = y  ~(y < x)) 
    (~(x < y)  ~(x = y)  y < x)"
proof-
  have "(x' < y'  ~(x' = y')  ~(y' < x'))  
    (~(x' < y')  x' = y'  ~(y' < x')) 
    (~(x' < y')  ~(x' = y')  y' < x')"
    for x' y' z' :: real 
    by auto
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Transitive Law: Definition 2.2.1.k.›

lemma vreal_transitive_law:
  assumes "x  " 
    and "y  " 
    and "z  " 
    and "x < y" and "y < z"
  shows "x < z"
proof-
  have "x' < y'  y' < z'  x' < z'" for x' y' z' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Addition Law of Order: Definition 2.2.1.l.›

lemma vreal_addition_law_of_order:
  assumes "x  " and "y  " and "z  " and "x < y"
  shows "x + z < y + z"
proof-
  have "x' < y'  x' + z' < y' + z'" for x' y' z' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Multiplication Law of Order: Definition 2.2.1.m.›

lemma vreal_multiplication_law_of_order:
  assumes "x  " 
    and "y  " 
    and "z  " 
    and "x < y" 
    and "0 < z"
  shows "x * z < y * z"
proof-
  have "x' < y'  0 < z'  x' * z' < y' * z'" for x' y' z' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Non-Triviality: Definition 2.2.1.n.›

lemma vreal_non_triviality: "0  1"
proof-
  have "0  (1::real)" by simp
  from this[untransferred] show ?thesis.
qed


text‹Least upper bound property: Definition 2.2.3.›

lemma least_upper_bound_property:
  defines "vreal_ub S M  (S    M    (xS. x  M))"
  assumes "A  " and "A  0" and "M. vreal_ub A M"
  obtains M where "vreal_ub A M" and "T. vreal_ub A T  M  T"
proof-
  note complete_real = 
    complete_real[
      untransferred, of elts A, unfolded vnumber_simps, OF assms(2)
      ]
  from assms obtain x where "x  A" by force
  moreover with assms have "x  " by auto
  ultimately have 1: "x. x  A" by auto
  from assms have 2: "x. yA. y  x" by auto
  from complete_real[OF 1 2] 
    obtain M
      where "M  " 
        and "x. x  A  x  M" 
        and [simp]: "T. T    (x. x  A  x  T)  M  T"
    by force
  with assms(2) have "vreal_ub A M" unfolding vreal_ub_def by simp
  moreover have "vreal_ub A T  M  T" for T unfolding vreal_ub_def by simp
  ultimately show ?thesis using that by auto
qed


subsubsection‹Fundamental properties of other operations›


text‹Minus.›

lemma vreal_minus_closed: 
  assumes "x  " and "y  "
  shows "x - y  "
proof-
  have "x' - y'  UNIV" for x' y' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vreal_minus_eq_plus_uminus: 
  assumes "x  " and "y  "
  shows "x - y = x + (- y)"
proof-
  have "x' - y' = x' + (-y')" for x' y' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Unary minus.›

lemma vreal_uminus_uminus: 
  assumes "x  " 
  shows "x = - (- x)"
proof-
  have "x' = -(-x')" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Multiplicative inverse.›

lemma vreal_inverse_inverse: 
  assumes "x  " 
  shows "x = (x¯)¯"
proof-
  have "x' = inverse (inverse x')" for x' :: real by simp
  from this[untransferred, OF assms] show ?thesis.
qed


subsubsection‹Further properties›


text‹Addition.›

global_interpretation vreal_plus: binop_onto  vreal_plus
proof-
  have binop: "binop  vreal_plus"
  proof(intro binopI nopI)
    show vsv: "vsv vreal_plus" unfolding vreal_plus_def by auto
    interpret vsv vreal_plus by (rule vsv)
    show "2  ω" by simp
    show dom: "𝒟 vreal_plus =  ^× 2" unfolding vreal_plus_def by simp
    show " vreal_plus  "
    proof(intro vsubsetI)
      fix y assume "y   vreal_plus"
      then obtain ab where "ab   ^× 2" and y_def: "y = vreal_plusab" 
        unfolding dom[symmetric] by force
      then obtain a b 
        where ab_def: "ab = [a, b]" and a: "a  " and b: "b  "
        by blast
      then show "y  " by (simp add: vreal_plus_closed y_def)
    qed
  qed
  interpret binop  vreal_plus by (rule binop)
  show "binop_onto  vreal_plus"
  proof(intro binop_ontoI')
    show "binop  vreal_plus" by (rule binop_axioms)
    show "   vreal_plus"
    proof(intro vsubsetI)
      fix y assume prems: "y  "
      moreover from vreal_zero vreal_zero_closed have "0  " by auto
      ultimately have "y + 0   vreal_plus" by auto
      moreover from prems vreal_identity_law_addition have "y = y + 0" 
        by (simp add: vreal_zero)
      ultimately show "y   vreal_plus" by simp
    qed
  qed
qed


text‹Unary minus.›

global_interpretation vreal_uminus: v11 vreal_uminus
  rewrites vreal_uminus_vdomain[simp]: "𝒟 vreal_uminus = "
    and vreal_uminus_vrange[simp]: " vreal_uminus = "
proof-
  show v11: "v11 vreal_uminus" 
  proof(intro v11I)
    show vsv: "vsv vreal_uminus" unfolding vreal_uminus_def by simp
    interpret vsv vreal_uminus by (rule vsv)
    show "vsv (vreal_uminus¯)"
    proof(intro vsvI)
      show "vbrelation (vreal_uminus¯)" by clarsimp
      fix a b c
      assume prems: "a, b  vreal_uminus¯" "a, c  vreal_uminus¯"
      then have ba: "b, a  vreal_uminus" and ca: "c, a  vreal_uminus" 
        by auto
      then have b: "b  " and c: "c  " 
        by (simp_all add: VLambda_iff2 vreal_uminus_def)
      from ba ca have "a = - b" "a = - c" by simp_all
      with ba ca b c show "b = c"  by (metis vreal_uminus_uminus)
    qed
  qed
  interpret v11 vreal_uminus by (rule v11)
  show dom: "𝒟 vreal_uminus = " unfolding vreal_uminus_def by simp
  have " vreal_uminus  "
  proof(intro vsubsetI)
    fix y assume "y   vreal_uminus"
    then obtain x where "x  " and y_def: "y = - x" 
      unfolding dom[symmetric] by force
    then show "y  " by (simp add: vreal_uminus_closed)
  qed
  moreover have "   vreal_uminus"
    by (intro vsubsetI) 
      (metis dom vdomain_atD vreal_uminus_closed vreal_uminus_uminus)
  ultimately show " vreal_uminus = " by simp
qed


text‹Multiplication.›

global_interpretation vreal_mult: binop_onto  vreal_mult
proof-
  have binop: "binop  vreal_mult"
  proof(intro binopI nopI)
    show vsv: "vsv vreal_mult" unfolding vreal_mult_def by auto
    interpret vsv vreal_mult by (rule vsv)
    show "2  ω" by simp
    show dom: "𝒟 vreal_mult =  ^× 2" unfolding vreal_mult_def by simp
    show " vreal_mult  "
    proof(intro vsubsetI)
      fix y assume "y   vreal_mult"
      then obtain ab where "ab   ^× 2" and y_def: "y = vreal_multab" 
        unfolding dom[symmetric] by force
      then obtain a b 
        where ab_def: "ab = [a, b]" and a: "a  " and b: "b  "
        by blast
      then show "y  " by (simp add: vreal_mult_closed y_def)
    qed
  qed
  interpret binop  vreal_mult by (rule binop)
  show "binop_onto  vreal_mult"
  proof(intro binop_ontoI')
    show "binop  vreal_mult" by (rule binop_axioms)
    show "   vreal_mult"
    proof(intro vsubsetI)
      fix y assume prems: "y  "
      moreover from vreal_one vreal_one_closed have "1  " by auto
      ultimately have "y * 1   vreal_mult" by auto
      moreover from prems vreal_identity_law_multiplication have "y = y * 1" 
        by (simp add: vreal_one)
      ultimately show "y   vreal_mult" by simp
    qed
  qed
qed


text‹Multiplicative inverse.›

global_interpretation vreal_inverse: v11 vreal_inverse
  rewrites vreal_inverse_vdomain[simp]: "𝒟 vreal_inverse = "
    and vreal_inverse_vrange[simp]: " vreal_inverse = "
proof-
  show v11: "v11 vreal_inverse" 
  proof(intro v11I)
    show vsv: "vsv vreal_inverse" unfolding vreal_inverse_def by simp
    interpret vsv vreal_inverse by (rule vsv)
    show "vsv (vreal_inverse¯)"
    proof(intro vsvI)
      show "vbrelation (vreal_inverse¯)" by clarsimp
      fix a b c
      assume prems: "a, b  vreal_inverse¯" "a, c  vreal_inverse¯"
      then have ba: "b, a  vreal_inverse" and ca: "c, a  vreal_inverse" 
        by auto
      then have b: "b  " and c: "c  " 
        by (simp_all add: VLambda_iff2 vreal_inverse_def)
      from ba ca have "a = b¯" "a = c¯" by simp_all
      with ba ca b c show "b = c"  by (metis vreal_inverse_inverse)
    qed
  qed
  interpret v11 vreal_inverse by (rule v11)
  show dom: "𝒟 vreal_inverse = " unfolding vreal_inverse_def by simp
  have " vreal_inverse  "
  proof(intro vsubsetI)
    fix y assume "y   vreal_inverse"
    then obtain x where "x  " and y_def: "y = x¯" 
      unfolding dom[symmetric] by force
    then show "y  " by (simp add: vreal_inverse_closed)
  qed
  moreover have "   vreal_inverse"
    by (intro vsubsetI) 
      (metis dom vdomain_atD vreal_inverse_closed vreal_inverse_inverse)
  ultimately show " vreal_inverse = " by simp
qed



subsection‹Integer numbers›


subsubsection‹Definition›

definition vint_of_int :: "int  V"
  where "vint_of_int = vreal_of_real"

notation vint_of_int (‹_ [999] 999)

declare [[coercion "vint_of_int :: int  V"]]

definition vint :: V ()
  where "vint = set (range vint_of_int)"

definition int_of_vint :: "V  int"
  where "int_of_vint = inv_into UNIV vint_of_int"


text‹Rules.›

lemma vint_of_int_in_vintI[intro, simp]: "a  " by (simp add: vint_def)

lemma vint_of_int_in_vintE[elim]:
  assumes "a  "
  obtains b where "b = a"
  using assms unfolding vint_def by auto


subsubsection‹Elementary properties›

lemma vint_vsubset_vreal: "  "
  unfolding vint_def vint_of_int_def vreal_def using image_cong by auto

lemma inj_vint_of_int: "inj vint_of_int"
  using inj_vreal_of_real 
  unfolding vint_of_int_def inj_def of_int_eq_iff
  by force

lemma vint_in_Vset_ω2: "  Vset (ω + ω)"
  using vint_vsubset_vreal vreal_in_Vset_ω2 by auto

lemma int_of_vint_vint_of_int[simp]: "int_of_vint (a) = a"
  by (simp add: inj_vint_of_int int_of_vint_def)


text‹Transfer rules.›

definition cr_vint :: "V  int  bool"
  where "cr_vint a b  (a = vint_of_int b)"

lemma cr_vint_right_total[transfer_rule]: "right_total cr_vint"
  unfolding cr_vint_def right_total_def by simp

lemma cr_vint_bi_unqie[transfer_rule]: "bi_unique cr_vint"
  unfolding cr_vint_def bi_unique_def
  by (simp add: inj_eq inj_vint_of_int)

lemma cr_vint_transfer_domain_rule[transfer_domain_rule]: 
  "Domainp cr_vint = (λx. x  )"
  unfolding cr_vint_def by force

lemma vint_transfer[transfer_rule]: 
  "(rel_set cr_vint) (elts ) (UNIV::int set)"
  unfolding cr_vint_def rel_set_def by auto

lemma vint_of_int_transfer[transfer_rule]: "cr_vint (vint_of_int a) a"
  unfolding cr_vint_def by auto


subsubsection‹Constants and operations›


text‹Auxiliary.›

lemma vint_fsingleton_in_fproduct_vint: "[a]   ^× 1" by auto

lemma vint_fpair_in_fproduct_vint: "[a, b]   ^× 2" by force


text‹Zero.›

lemma vint_zero: "0 = (0::V)" by (simp add: vint_of_int_def vreal_zero)


text‹One.›

lemma vint_one: "1 = (1::V)" by (simp add: vreal_one vint_of_int_def)
  

text‹Addition.›

definition vint_plus :: V 
  where "vint_plus = 
    (λx ^× 2. (int_of_vint (x0) + int_of_vint (x1)))"

abbreviation vint_plus_app (infixl "+" 65) 
  where "vint_plus_app a b  vint_plusa, b"

lemma vint_plus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vint ===> cr_vint ===> cr_vint) (+) (+)"
  using vint_fpair_in_fproduct_vint
  by (intro rel_funI, unfold vint_plus_def cr_vint_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Multiplication.›

definition vint_mult :: V 
  where "vint_mult = 
    (λx ^× 2. (int_of_vint (x0) * int_of_vint (x1)))"

abbreviation vint_mult_app (infixl "*" 65) 
  where "vint_mult_app a b  vint_multa, b"

lemma vint_mult_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vint ===> cr_vint ===> cr_vint) (*) (*)"
  using vint_fpair_in_fproduct_vint
  by (intro rel_funI, unfold vint_mult_def cr_vint_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Unary minus.›

definition vint_uminus :: V 
  where "vint_uminus = (λx. (uminus (int_of_vint x)))"

abbreviation vint_uminus_app ("- _" [81] 80) 
  where "- a  vint_uminusa"

lemma vint_uminus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vint ===> cr_vint) (vint_uminus_app) (uminus)"
  using vint_fsingleton_in_fproduct_vint 
  by (intro rel_funI, unfold vint_uminus_def cr_vint_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Order.›

definition vint_le :: V 
  where "vint_le =
    set {[a, b] | a b. [a, b]   ^× 2  int_of_vint a  int_of_vint b}"

abbreviation vint_le' ("(_/  _)"  [51, 51] 50)
  where "a  b  [a, b]  vint_le"

lemma small_vint_le[simp]: 
  "small {[a, b] | a b. [a, b]   ^× 2  int_of_vint a  int_of_vint b}"
proof-
  have small: "small {[a, b] | a b. [a, b]   ^× 2}" by simp
  show ?thesis by (rule smaller_than_small[OF small]) auto
qed

lemma vint_le_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vint ===> cr_vint ===> (=)) vint_le' (≤)"
  using vint_fsingleton_in_fproduct_vint 
  by (intro rel_funI, unfold cr_scalar_def cr_vint_def vint_le_def)
    (auto simp: nat_omega_simps)


text‹Strict order.›

definition vint_ls :: V 
  where "vint_ls =
    set {[a, b] | a b. [a, b]   ^× 2  int_of_vint a < int_of_vint b}"

abbreviation vint_ls' ("(_/ < _)"  [51, 51] 50)
  where "a < b  [a, b]  vint_ls"

lemma small_vint_ls[simp]: 
  "small {[a, b] | a b. [a, b]   ^× 2  int_of_vint a < int_of_vint b}"
proof-
  have small: "small {[a, b] | a b. [a, b]   ^× 2}" by simp
  show ?thesis by (rule smaller_than_small[OF small]) auto
qed

lemma vint_ls_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vint ===> cr_vint ===> (=)) vint_ls' (<)"
  using vint_fsingleton_in_fproduct_vint 
  by (intro rel_funI, unfold cr_scalar_def cr_vint_def vint_ls_def)
    (auto simp: nat_omega_simps)


text‹Subtraction.›

definition vint_minus :: V 
  where "vint_minus = 
    (λx ^× 2. (int_of_vint (x0) - int_of_vint (x1)))"

abbreviation vint_minus_app (infixl "-" 65) 
  where "vint_minus_app a b  vint_minusa, b"

lemma vint_minus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vint ===> cr_vint ===> cr_vint) (-) (-)"
  using vint_fpair_in_fproduct_vint
  by (intro rel_funI, unfold vint_minus_def cr_vint_def cr_scalar_def) 
    (simp add: nat_omega_simps)


subsubsection‹Axioms of a well ordered integral domain›


text‹The exposition follows Definition 1.4.1 from the textbook 
The Real Numbers and Real Analysis› by E. Bloch
cite"bloch_real_2010".›

lemma vint_zero_closed: "0  " by auto

lemma vint_one_closed: "1  " by auto

lemma vint_plus_closed: 
  assumes "x  " and "y  "
  shows "x + y  "
proof-
  have "x' + y'  UNIV" for x' y' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vint_mult_closed:
  assumes "x  " and "y  " 
  shows "x * y  "
proof-
  have "(x'::int) * y'  UNIV" for x' y' by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vint_uminus_closed: 
  assumes "x  "
  shows "- x  "
proof-
  have "(-x'::int)  UNIV" for x' by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Associative Law for Addition: Definition 1.4.1.a.›

lemma vint_assoc_law_addition: 
  assumes "x  " and "y  " and "z  "  
  shows "(x + y) + z = x + (y + z)"
proof-
  have "(x' + y') + z' = x' + (y' + z')" for x' y' z' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Commutative Law for Addition: Definition 1.4.1.b.›

lemma vint_commutative_law_addition: 
  assumes "x  " and "y  "    
  shows "x + y = y + x"
proof-
  have "x' + y' = y' + x'" for x' y' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Identity Law for Addition: Definition 1.4.1.c.›

lemma vint_identity_law_addition: 
  assumes [simp]: "x  "
  shows "x + 0 = x"
proof-
  have "x' + 0 = x'" for x' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Inverses Law for Addition: Definition 1.4.1.d.›

lemma vint_inverses_law_addition: 
  assumes [simp]: "x  "
  shows "x + (- x) = 0"
proof-
  have "x' + (-x') = 0" for x' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Associative Law for Multiplication: Definition 1.4.1.e.›

lemma vint_assoc_law_multiplication: 
  assumes "x  " and "y  " and "z  "  
  shows "(x * y) * z = x * (y * z)"
proof-
  have "(x' * y') * z' = x' * (y' * z')" for x' y' z' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Commutative Law for Multiplication: Definition 1.4.1.f.›

lemma vint_commutative_law_multiplication: 
  assumes "x  " and "y  " 
  shows "x * y = y * x"
proof-
  have "x' * y' = y' * x'" for x' y' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Identity Law for multiplication: Definition 1.4.1.g.›

lemma vint_identity_law_multiplication: 
  assumes "x  "
  shows "x * 1 = x"
proof-
  have "x' * 1 = x'" for x' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Distributive Law for Multiplication: Definition 1.4.1.h.›

lemma vint_distributive_law: 
  assumes "x  " and "y  " and "z  "  
  shows "x * (y + z) = (x * y) + (x * z)"
proof-
  have "x' * (y' + z') = (x' * y') + (x' * z')" for x' y' z' :: int 
    by (simp add: algebra_simps)
  from this[untransferred, OF assms] show ?thesis.
qed


text‹No Zero Divisors Law: Definition 1.4.1.i.›

lemma vint_no_zero_divisors_law: 
  assumes "x  " and "y  " and "x * y = 0"
  shows "x = 0  y = 0" 
proof-
  have "x' * y' = 0  x' = 0  y' = 0" for x' y' z' :: int 
    by (simp add: algebra_simps)
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Trichotomy Law: Definition 1.4.1.j›

lemma vint_trichotomy_law:
  assumes "x  " and "y  "
  shows 
    "(x < y  ~(x = y)  ~(y < x))  
    (~(x < y)  x = y  ~(y < x)) 
    (~(x < y)  ~(x = y)  y < x)"
proof-
  have
    "(x' < y'  ~(x' = y')  ~(y' < x'))  
    (~(x' < y')  x' = y'  ~(y' < x')) 
    (~(x' < y')  ~(x' = y')  y' < x')"
    for x' y' z' :: int
    by auto
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Transitive Law: Definition 1.4.1.k›

lemma vint_transitive_law:
  assumes "x  " 
    and "y  " 
    and "z  " 
    and "x < y" 
    and "y < z"
  shows "x < z"
proof-
  have "x' < y'  y' < z'  x' < z'" for x' y' z' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Addition Law of Order: Definition 1.4.1.l›

lemma vint_addition_law_of_order:
  assumes "x  " and "y  " and "z  " and "x < y"
  shows "x + z < y + z"
proof-
  have "x' < y'  x' + z' < y' + z'" for x' y' z' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Multiplication Law of Order: Definition 1.4.1.m›

lemma vint_multiplication_law_of_order:
  assumes "x  " 
    and "y  " 
    and "z  " 
    and "x < y"
    and "0 < z"
  shows "x * z < y * z"
proof-
  have "x' < y'  0 < z'  x' * z' < y' * z'" for x' y' z' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Non-Triviality: Definition 1.4.1.n›

lemma vint_non_triviality: "0  1"
proof-
  have "0  (1::int)" by simp
  from this[untransferred] show ?thesis.
qed


text‹Well-Ordering Principle.›

lemma well_ordering_principle:
  assumes "A  " 
    and "a  " 
    and "A  0" 
    and "x. x  A  a < x"
  obtains b where "b  A" and "x. x  A  b  x"
proof-
  {
    fix A' and a' :: int assume prems: "A'  {}" "x  A'  a' < x" for x
    then obtain a'' where a'': "a''  A'" by auto
    from wfE_min[OF wf_int_ge_less_than[of a'], OF a''] obtain b'
      where b'_A': "b'  A'" 
        and yb': "(y, b')  int_ge_less_than a'  y  A'" 
      for y
      by auto
    moreover from prems b'_A' yb' have "x. x  A'  b'  x" 
      unfolding int_ge_less_than_def by fastforce
    with b'_A' have "b. b  A'  (x. x  A'  b  x)" by blast
  }
  note real_wo = this
  from real_wo[
      untransferred, of elts A, unfolded vnumber_simps, OF assms(1,2)
      ]
  obtain b 
    where "b  " 
      and "b  A" 
      and "x. x    x  A  b  x"
    by (auto simp: assms(3,4))
  with assms that show ?thesis unfolding vsubset_iff by simp
qed


subsubsection‹Fundamental properties of other operations›


text‹Minus.›

lemma vint_minus_closed: 
  assumes "x  " and "y  "
  shows "x - y  "
proof-
  have "x' - y'  UNIV" for x' y' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vint_minus_eq_plus_uminus: 
  assumes "x  " and "y  "
  shows "x - y = x + (- y)"
proof-
  have "x' - y' = x' + (-y')" for x' y' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Unary minus.›

lemma vint_uminus_uminus: 
  assumes "x  " 
  shows "x = - (- x)"
proof-
  have "x' = -(-x')" for x' :: int by simp
  from this[untransferred, OF assms] show ?thesis.
qed


subsubsection‹Further properties›


text‹Addition.›

global_interpretation vint_plus: binop_onto  vint_plus
proof-
  have binop: "binop  vint_plus"
  proof(intro binopI nopI)
    show vsv: "vsv vint_plus" unfolding vint_plus_def by auto
    interpret vsv vint_plus by (rule vsv)
    show "2  ω" by simp
    show dom: "𝒟 vint_plus =  ^× 2" unfolding vint_plus_def by simp
    show " vint_plus  "
    proof(intro vsubsetI)
      fix y assume "y   vint_plus"
      then obtain ab where "ab   ^× 2" and y_def: "y = vint_plusab" 
        unfolding dom[symmetric] by force
      then obtain a b 
        where ab_def: "ab = [a, b]" and a: "a  " and b: "b  "
        by blast
      then show "y  " by (simp add: vint_plus_closed y_def)
    qed
  qed
  interpret binop  vint_plus by (rule binop)
  show "binop_onto  vint_plus"
  proof(intro binop_ontoI')
    show "binop  vint_plus" by (rule binop_axioms)
    show "   vint_plus"
    proof(intro vsubsetI)
      fix y assume prems: "y  "
      moreover from vint_zero vint_zero_closed have "0  " by auto
      ultimately have "y + 0   vint_plus" by auto
      moreover from prems vint_identity_law_addition have "y = y + 0" 
        by (simp add: vint_zero)
      ultimately show "y   vint_plus" by simp
    qed
  qed
qed


text‹Unary minus.›

global_interpretation vint_uminus: v11 vint_uminus
  rewrites vint_uminus_vdomain[simp]: "𝒟 vint_uminus = "
    and vint_uminus_vrange[simp]: " vint_uminus = "
proof-
  show v11: "v11 vint_uminus" 
  proof(intro v11I)
    show vsv: "vsv vint_uminus" unfolding vint_uminus_def by simp
    interpret vsv vint_uminus by (rule vsv)
    show "vsv (vint_uminus¯)"
    proof(intro vsvI)
      show "vbrelation (vint_uminus¯)" by clarsimp
      fix a b c
      assume prems: "a, b  vint_uminus¯" "a, c  vint_uminus¯"
      then have ba: "b, a  vint_uminus" and ca: "c, a  vint_uminus" 
        by auto
      then have b: "b  " and c: "c  " 
        by (simp_all add: VLambda_iff2 vint_uminus_def)
      from ba ca have "a = - b" "a = - c" by simp_all
      with ba ca b c show "b = c"  by (metis vint_uminus_uminus)
    qed
  qed
  interpret v11 vint_uminus by (rule v11)
  show dom: "𝒟 vint_uminus = " unfolding vint_uminus_def by simp
  have " vint_uminus  "
  proof(intro vsubsetI)
    fix y assume "y   vint_uminus"
    then obtain x where "x  " and y_def: "y = - x" 
      unfolding dom[symmetric] by force
    then show "y  " by (simp add: vint_uminus_closed)
  qed
  moreover have "   vint_uminus"
    by (intro vsubsetI) 
      (metis dom vdomain_atD vint_uminus_closed vint_uminus_uminus)
  ultimately show " vint_uminus = " by simp
qed


text‹Multiplication.›

global_interpretation vint_mult: binop_onto  vint_mult
proof-
  have binop: "binop  vint_mult"
  proof(intro binopI nopI)
    show vsv: "vsv vint_mult" unfolding vint_mult_def by auto
    interpret vsv vint_mult by (rule vsv)
    show "2  ω" by simp
    show dom: "𝒟 vint_mult =  ^× 2" unfolding vint_mult_def by simp
    show " vint_mult  "
    proof(intro vsubsetI)
      fix y assume "y   vint_mult"
      then obtain ab where "ab   ^× 2" and y_def: "y = vint_multab" 
        unfolding dom[symmetric] by force
      then obtain a b 
        where ab_def: "ab = [a, b]" and a: "a  " and b: "b  "
        by blast
      then show "y  " by (simp add: vint_mult_closed y_def)
    qed
  qed
  interpret binop  vint_mult by (rule binop)
  show "binop_onto  vint_mult"
  proof(intro binop_ontoI')
    show "binop  vint_mult" by (rule binop_axioms)
    show "   vint_mult"
    proof(intro vsubsetI)
      fix y assume prems: "y  "
      moreover from vint_one vint_one_closed have 0: "1  " by auto
      ultimately have "y * 1   vint_mult" by auto
      moreover from prems vint_identity_law_multiplication have "y = y * 1" 
        by (simp add: vint_one)
      ultimately show "y   vint_mult" by simp
    qed
  qed
qed


text‹Misc.›

lemma (in 𝒵) vint_in_Vset[intro]: "  Vset α"
  using vint_in_Vset_ω2 vsubsetD by (auto intro!: 𝒵_Vset_ω2_vsubset_Vset)



subsection‹Rational numbers›


subsubsection‹Definition›

definition vrat_of_rat :: "rat  V"
  where "vrat_of_rat x = vreal_of_real (real_of_rat x)"

notation vrat_of_rat (‹_ [999] 999)

declare [[coercion "vrat_of_rat :: rat  V"]]

definition vrat :: V ()
  where "vrat = set (range vrat_of_rat)"

definition rat_of_vrat :: "V  rat"
  where "rat_of_vrat = inv_into UNIV vrat_of_rat"


text‹Rules.›

lemma vrat_of_rat_in_vratI[intro, simp]: "a  " by (simp add: vrat_def)

lemma vrat_of_rat_in_vratE[elim]:
  assumes "a  "
  obtains b where "b = a"
  using assms unfolding vrat_def by auto


subsubsection‹Elementary properties›

lemma vrat_vsubset_vreal: "  "
  unfolding vrat_def vrat_of_rat_def vreal_def using image_cong by auto

lemma vrat_in_Vset_ω2: "  Vset (ω + ω)"
  using vrat_vsubset_vreal vreal_in_Vset_ω2 by auto

lemma inj_vrat_of_rat: "inj vrat_of_rat"
  using inj_vreal_of_real 
  unfolding vrat_of_rat_def inj_def of_rat_eq_iff
  by force

lemma rat_of_vrat_vrat_of_rat[simp]: "rat_of_vrat (a) = a"
  by (simp add: inj_vrat_of_rat rat_of_vrat_def)


text‹Transfer rules.›

definition cr_vrat :: "V  rat  bool"
  where "cr_vrat a b  (a = vrat_of_rat b)"

lemma cr_vrat_right_total[transfer_rule]: "right_total cr_vrat"
  unfolding cr_vrat_def right_total_def by simp

lemma cr_vrat_bi_unqie[transfer_rule]: "bi_unique cr_vrat"
  unfolding cr_vrat_def bi_unique_def
  by (simp add: inj_eq inj_vrat_of_rat)

lemma cr_vrat_transfer_domain_rule[transfer_domain_rule]: 
  "Domainp cr_vrat = (λx. x  )"
  unfolding cr_vrat_def by force

lemma vrat_transfer[transfer_rule]: 
  "(rel_set cr_vrat) (elts ) (UNIV::rat set)"
  unfolding cr_vrat_def rel_set_def by auto

lemma vrat_of_rat_transfer[transfer_rule]: "cr_vrat (vrat_of_rat a) a"
  unfolding cr_vrat_def by auto


subsubsection‹Operations›

lemma vrat_fsingleton_in_fproduct_vrat: "[a]   ^× 1" by auto

lemma vrat_fpair_in_fproduct_vrat: "[a, b]   ^× 2" by force


text‹Zero.›

lemma vrat_zero: "0 = (0::V)" by (simp add: vrat_of_rat_def vreal_zero)


text‹One.›

lemma vrat_one: "1 = (1::V)" by (simp add: vreal_one vrat_of_rat_def)
  

text‹Addition.›

definition vrat_plus :: V 
  where "vrat_plus = 
    (λx ^× 2. (rat_of_vrat (x0) + rat_of_vrat (x1)))"

abbreviation vrat_plus_app (infixl "+" 65) 
  where "vrat_plus_app a b  vrat_plusa, b"

lemma vrat_plus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat ===> cr_vrat) (+) (+)"
  using vrat_fpair_in_fproduct_vrat
  by (intro rel_funI, unfold vrat_plus_def cr_vrat_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Multiplication.›

definition vrat_mult :: V 
  where "vrat_mult =
    (λx ^× 2. (rat_of_vrat (x0) * rat_of_vrat (x1)))"

abbreviation vrat_mult_app (infixl "*" 65) 
  where "vrat_mult_app a b  vrat_multa, b"

lemma vrat_mult_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat ===> cr_vrat) (*) (*)"
  using vrat_fpair_in_fproduct_vrat
  by (intro rel_funI, unfold vrat_mult_def cr_vrat_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Unary minus.›

definition vrat_uminus :: V 
  where "vrat_uminus = (λx. (uminus (rat_of_vrat x)))"

abbreviation vrat_uminus_app ("- _" [81] 80) 
  where "- a  vrat_uminusa"

lemma vrat_uminus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat) (vrat_uminus_app) (uminus)"
  using vrat_fsingleton_in_fproduct_vrat 
  by (intro rel_funI, unfold vrat_uminus_def cr_vrat_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Multiplicative inverse.›

definition vrat_inverse :: V 
  where "vrat_inverse = (λx. (inverse (rat_of_vrat x)))"

abbreviation vrat_inverse_app ("(_¯)" [1000] 999) 
  where "a¯  vrat_inversea"

lemma vrat_inverse_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat) (vrat_inverse_app) (inverse)"
  using vrat_fsingleton_in_fproduct_vrat 
  by (intro rel_funI, unfold vrat_inverse_def cr_vrat_def cr_scalar_def) 
    (simp add: nat_omega_simps)


text‹Order.›

definition vrat_le :: V 
  where "vrat_le =
    set {[a, b] | a b. [a, b]   ^× 2  rat_of_vrat a  rat_of_vrat b}"

abbreviation vrat_le' ("(_/  _)"  [51, 51] 50)
  where "a  b  [a, b]  vrat_le"

lemma small_vrat_le[simp]: 
  "small {[a, b] | a b. [a, b]   ^× 2  rat_of_vrat a  rat_of_vrat b}"
proof-
  have small: "small {[a, b] | a b. [a, b]   ^× 2}" by simp
  show ?thesis by (rule smaller_than_small[OF small]) auto
qed

lemma vrat_le_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat ===> (=)) vrat_le' (≤)"
  using vrat_fsingleton_in_fproduct_vrat 
  by (intro rel_funI, unfold cr_scalar_def cr_vrat_def vrat_le_def)
    (auto simp: nat_omega_simps)


text‹Strict order.›

definition vrat_ls :: V 
  where "vrat_ls =
    set {[a, b] | a b. [a, b]   ^× 2  rat_of_vrat a < rat_of_vrat b}"

abbreviation vrat_ls' ("(_/ < _)"  [51, 51] 50)
  where "a < b  [a, b]  vrat_ls"

lemma small_vrat_ls[simp]: 
  "small {[a, b] | a b. [a, b]   ^× 2  rat_of_vrat a < rat_of_vrat b}"
proof-
  have small: "small {[a, b] | a b. [a, b]   ^× 2}" by simp
  show ?thesis by (rule smaller_than_small[OF small]) auto
qed

lemma vrat_ls_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat ===> (=)) vrat_ls' (<)"
  by (intro rel_funI, unfold cr_scalar_def cr_vrat_def vrat_ls_def)
    (auto simp: nat_omega_simps)
  

text‹Subtraction.›

definition vrat_minus :: V 
  where "vrat_minus = 
    (λx ^× 2. (rat_of_vrat (x0) - rat_of_vrat (x1)))"

abbreviation vrat_minus_app (infixl "-" 65) 
  where "vrat_minus_app a b  vrat_minusa, b"

lemma vrat_minus_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vrat ===> cr_vrat ===> cr_vrat)
    (-) (-)"
  using vrat_fpair_in_fproduct_vrat 
  by (intro rel_funI, unfold vrat_minus_def cr_vrat_def cr_scalar_def) 
    (simp add: nat_omega_simps)


subsubsection‹Axioms of an ordered field›


text‹The exposition follows Theorem 1.5.5 from the textbook
The Real Numbers and Real Analysis› by E. Bloch
cite"bloch_real_2010".›

lemma vrat_zero_closed: "0  " by auto

lemma vrat_one_closed: "1  " by auto

lemma vrat_plus_closed: 
  assumes "x  " "y  "
  shows "x + y  "
proof-
  have "x' + y'  UNIV" for x' y' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vrat_mult_closed:
  assumes "x  " and "y  " 
  shows "x * y  "
proof-
  have "(x'::rat) * y'  UNIV" for x' y' by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vrat_uminus_closed: 
  assumes "x  "
  shows "- x  "
proof-
  have "(-x'::rat)  UNIV" for x' by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vrat_inverse_closed: 
  assumes "x  "
  shows "x¯  "
proof-
  have "inverse (x'::rat)  UNIV" for x' by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Associative Law for Addition: Theorem 1.5.5.1.›

lemma vrat_assoc_law_addition: 
  assumes "x  " and "y  " and "z  "  
  shows "(x + y) + z = x + (y + z)"
proof-
  have "(x' + y') + z' = x' + (y' + z')" for x' y' z' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Commutative Law for Addition: Theorem 1.5.5.2.›

lemma vrat_commutative_law_addition: 
  assumes "x  " and "y  "    
  shows "x + y = y + x"
proof-
  have "x' + y' = y' + x'" for x' y' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Identity Law for Addition: Theorem 1.5.5.3.›

lemma vrat_identity_law_addition: 
  assumes [simp]: "x  "
  shows "x + 0 = x"
proof-
  have "x' + 0 = x'" for x' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Inverses Law for Addition: Theorem 1.5.5.4.›

lemma vrat_inverses_law_addition: 
  assumes [simp]: "x  "
  shows "x + (- x) = 0"
proof-
  have "x' + (-x') = 0" for x' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Associative Law for Multiplication: Theorem 1.5.5.5.›

lemma vrat_assoc_law_multiplication: 
  assumes "x  " and "y  " and "z  "  
  shows "(x * y) * z = x * (y * z)"
proof-
  have "(x' * y') * z' = x' * (y' * z')" for x' y' z' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Commutative Law for Multiplication: Theorem 1.5.5.6.›

lemma vrat_commutative_law_multiplication: 
  assumes "x  " and "y  " 
  shows "x * y = y * x"
proof-
  have "x' * y' = y' * x'" for x' y' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Identity Law for multiplication: Theorem 1.5.5.7.›

lemma vrat_identity_law_multiplication: 
  assumes "x  "
  shows "x * 1 = x"
proof-
  have "x' * 1 = x'" for x' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Inverses Law for Multiplication: Definition 2.2.1.8.›

lemma vrat_inverses_law_multiplication:
  assumes "x  " and "x  0" 
  shows "x * x¯ = 1"
proof-
  have "x'  0  x' * inverse x' = 1" for x' :: rat by simp  
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Distributive Law for Multiplication: Theorem 1.5.5.9.›

lemma vrat_distributive_law: 
  assumes "x  " and "y  " and "z  "  
  shows "x * (y + z) = (x * y) + (x * z)"
proof-
  have "x' * (y' + z') = (x' * y') + (x' * z')" for x' y' z' :: rat 
    by (simp add: algebra_simps)
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Trichotomy Law: Theorem 1.5.5.10.›

lemma vrat_trichotomy_law:
  assumes "x  " and "y  "
  shows 
    "(x < y  ~(x = y)  ~(y < x))  
    (~(x < y)  x = y  ~(y < x)) 
    (~(x < y)  ~(x = y)  y < x)"
proof-
  have
    "(x' < y'  ~(x' = y')  ~(y' < x'))  
    (~(x' < y')  x' = y'  ~(y' < x')) 
    (~(x' < y')  ~(x' = y')  y' < x')"
    for x' y' z' :: rat
    by auto
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Transitive Law: Theorem 1.5.5.11.›

lemma vrat_transitive_law:
  assumes "x  " 
    and "y  " 
    and "z  " 
    and "x < y" 
    and "y < z"
  shows "x < z"
proof-
  have "x' < y'  y' < z'  x' < z'" for x' y' z' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Addition Law of Order: Theorem 1.5.5.12.›

lemma vrat_addition_law_of_order:
  assumes "x  " and "y  " and "z  " and "x < y"
  shows "x + z < y + z"
proof-
  have "x' < y'  x' + z' < y' + z'" for x' y' z' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Multiplication Law of Order: Theorem 1.5.5.13.›

lemma vrat_multiplication_law_of_order:
  assumes "x  " 
    and "y  " 
    and "z  " 
    and "x < y"
    and "0 < z"
  shows "x * z < y * z"
proof-
  have "x' < y'  0 < z'  x' * z' < y' * z'" for x' y' z' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Non-Triviality: Theorem 1.5.5.14.›

lemma vrat_non_triviality: "0  1"
proof-
  have "0  (1::rat)" by simp
  from this[untransferred] show ?thesis.
qed


subsubsection‹Fundamental properties of other operations›


text‹Minus.›

lemma vrat_minus_closed: 
  assumes "x  " and "y  "
  shows "x - y  "
proof-
  have "x' - y'  UNIV" for x' y' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed

lemma vrat_minus_eq_plus_uminus: 
  assumes "x  " and "y  "
  shows "x - y = x + (- y)"
proof-
  have "x' - y' = x' + (-y')" for x' y' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Unary minus.›

lemma vrat_uminus_uminus: 
  assumes "x  " 
  shows "x = - (- x)"
proof-
  have "x' = -(-x')" for x' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


text‹Multiplicative inverse.›

lemma vrat_inverse_inverse: 
  assumes "x  " 
  shows "x = (x¯)¯"
proof-
  have "x' = inverse (inverse x')" for x' :: rat by simp
  from this[untransferred, OF assms] show ?thesis.
qed


subsubsection‹Further properties›


text‹Addition.›

global_interpretation vrat_plus: binop_onto  vrat_plus
proof-
  have binop: "binop  vrat_plus"
  proof(intro binopI nopI)
    show vsv: "vsv vrat_plus" unfolding vrat_plus_def by auto
    interpret vsv vrat_plus by (rule vsv)
    show "2  ω" by simp
    show dom: "𝒟 vrat_plus =  ^× 2" unfolding vrat_plus_def by simp
    show " vrat_plus  "
    proof(intro vsubsetI)
      fix y assume "y   vrat_plus"
      then obtain ab where "ab   ^× 2" and y_def: "y = vrat_plusab" 
        unfolding dom[symmetric] by force
      then obtain a b 
        where ab_def: "ab = [a, b]" and a: "a  " and b: "b  "
        by blast
      then show "y  " by (simp add: vrat_plus_closed y_def)
    qed
  qed
  interpret binop  vrat_plus by (rule binop)
  show "binop_onto  vrat_plus"
  proof(intro binop_ontoI')
    show "binop  vrat_plus" by (rule binop_axioms)
    show "   vrat_plus"
    proof(intro vsubsetI)
      fix y assume prems: "y  "
      moreover from vrat_zero vrat_zero_closed have 0: "0  " 
        by auto
      ultimately have "y + 0   vrat_plus" by auto
      moreover from prems vrat_identity_law_addition have "y = y + 0" 
        by (simp add: vrat_zero)
      ultimately show "y   vrat_plus" by simp
    qed
  qed
qed


text‹Unary minus.›

global_interpretation vrat_uminus: v11 vrat_uminus
  rewrites vrat_uminus_vdomain[simp]: "𝒟 vrat_uminus = "
    and vrat_uminus_vrange[simp]: " vrat_uminus = "
proof-
  show v11: "v11 vrat_uminus" 
  proof(intro v11I)
    show vsv: "vsv vrat_uminus" unfolding vrat_uminus_def by simp
    interpret vsv vrat_uminus by (rule vsv)
    show "vsv (vrat_uminus¯)"
    proof(intro vsvI)
      show "vbrelation (vrat_uminus¯)" by clarsimp
      fix a b c
      assume prems: "a, b  vrat_uminus¯" "a, c  vrat_uminus¯"
      then have ba: "b, a  vrat_uminus" and ca: "c, a  vrat_uminus" 
        by auto
      then have b: "b  " and c: "c  " 
        by (simp_all add: VLambda_iff2 vrat_uminus_def)
      from ba ca have "a = - b" "a = - c" by simp_all
      with ba ca b c show "b = c"  by (metis vrat_uminus_uminus)
    qed
  qed
  interpret v11 vrat_uminus by (rule v11)
  show dom: "𝒟 vrat_uminus = " unfolding vrat_uminus_def by simp
  have " vrat_uminus  "
  proof(intro vsubsetI)
    fix y assume "y   vrat_uminus"
    then obtain x where "x  " and y_def: "y = - x" 
      unfolding dom[symmetric] by force
    then show "y  " by (simp add: vrat_uminus_closed)
  qed
  moreover have "   vrat_uminus"
    by (intro vsubsetI) 
      (metis dom vdomain_atD vrat_uminus_closed vrat_uminus_uminus)
  ultimately show " vrat_uminus = " by simp
qed


text‹Multiplication.›

global_interpretation vrat_mult: binop_onto  vrat_mult
proof-
  have binop: "binop  vrat_mult"
  proof(intro binopI nopI)
    show vsv: "vsv vrat_mult" unfolding vrat_mult_def by auto
    interpret vsv vrat_mult by (rule vsv)
    show "2  ω" by simp
    show dom: "𝒟 vrat_mult =  ^× 2" unfolding vrat_mult_def by simp
    show " vrat_mult  "
    proof(intro vsubsetI)
      fix y assume "y   vrat_mult"
      then obtain ab where "ab   ^× 2" and y_def: "y = vrat_multab" 
        unfolding dom[symmetric] by force
      then obtain a b 
        where ab_def: "ab = [a, b]" and a: "a  " and b: "b  "
        by blast
      then show "y  " by (simp add: vrat_mult_closed y_def)
    qed
  qed
  interpret binop  vrat_mult by (rule binop)
  show "binop_onto  vrat_mult"
  proof(intro binop_ontoI')
    show "binop  vrat_mult" by (rule binop_axioms)
    show "   vrat_mult"
    proof(intro vsubsetI)
      fix y assume prems: "y  "
      moreover from vrat_one vrat_one_closed have "1  " by auto
      ultimately have "y * 1   vrat_mult" by auto
      moreover from prems vrat_identity_law_multiplication have "y = y * 1" 
        by (simp add: vrat_one)
      ultimately show "y   vrat_mult" by simp
    qed
  qed
qed


text‹Multiplicative inverse.›

global_interpretation vrat_inverse: v11 vrat_inverse
  rewrites vrat_inverse_vdomain[simp]: "𝒟 vrat_inverse = "
    and vrat_inverse_vrange[simp]: " vrat_inverse = "
proof-
  show v11: "v11 vrat_inverse" 
  proof(intro v11I)
    show vsv: "vsv vrat_inverse" unfolding vrat_inverse_def by simp
    interpret vsv vrat_inverse by (rule vsv)
    show "vsv (vrat_inverse¯)"
    proof(intro vsvI)
      show "vbrelation (vrat_inverse¯)" by clarsimp
      fix a b c
      assume prems: "a, b  vrat_inverse¯" "a, c  vrat_inverse¯"
      then have ba: "b, a  vrat_inverse" and ca: "c, a  vrat_inverse" 
        by auto
      then have b: "b  " and c: "c  " 
        by (simp_all add: VLambda_iff2 vrat_inverse_def)
      from ba ca have "a = b¯" "a = c¯" by simp_all
      with ba ca b c show "b = c"  by (metis vrat_inverse_inverse)
    qed
  qed
  interpret v11 vrat_inverse by (rule v11)
  show dom: "𝒟 vrat_inverse = " unfolding vrat_inverse_def by simp
  have " vrat_inverse  "
  proof(intro vsubsetI)
    fix y assume "y   vrat_inverse"
    then obtain x where "x  " and y_def: "y = x¯" 
      unfolding dom[symmetric] by force
    then show "y  " by (simp add: vrat_inverse_closed)
  qed
  moreover have "   vrat_inverse"
    by (intro vsubsetI) 
      (metis dom vdomain_atD vrat_inverse_closed vrat_inverse_inverse)
  ultimately show " vrat_inverse = " by simp
qed


text‹Misc.›

lemma (in 𝒵) vrat_in_Vset[intro]: "  Vset α"
  using vrat_in_Vset_ω2 vsubsetD by (auto intro!: 𝒵_Vset_ω2_vsubset_Vset)



subsection‹Upper bound on the cardinality of the continuum for typV

lemma inj_on_inv_vreal_of_real: "inj_on (inv vreal_of_real) (elts )"
  by (intro inj_onI) (fastforce intro: inv_into_injective)

lemma vreal_vlepoll_VPow_omega: "  VPow ω"
proof-
  have "elts   (UNIV::real set)"
    unfolding lepoll_def by (auto intro: inj_on_inv_vreal_of_real)
  from vlepoll_VPow_omega_if_vreal_lepoll_real[OF this] show ?thesis by simp
qed

lemma (in 𝒵) vreal_in_Vset[intro]: "  Vset α"
  using vreal_in_Vset_ω2 vsubsetD by (auto intro!: 𝒵_Vset_ω2_vsubset_Vset)

text‹\newpage›

end