Theory CZH_Sets_ZQR
section‹
Construction of integer numbers, rational numbers and real numbers
›
theory CZH_Sets_ZQR
imports
"HOL-Library.Rewrite"
CZH_Sets_NOP
CZH_Sets_VNHS
HOL_CContinuum
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 \<^term>‹Vset (ω + ω)›.\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 \<^typ>‹int› and \<^typ>‹rat›, 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 x = assms
also from real_lepoll_natnat have "… ≲ (UNIV::nat set set)"
unfolding Pow_UNIV by simp
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::real⇒V. 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 (x⦇0⇩ℕ⦈) + real_of_vreal (x⦇1⇩ℕ⦈))⇩ℝ)"
abbreviation vreal_plus_app :: "V ⇒ V ⇒ V" (infixl "+⇩ℝ" 65)
where "vreal_plus_app a b ≡ vreal_plus⦇a, 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 (x⦇0⇩ℕ⦈) * real_of_vreal (x⦇1⇩ℕ⦈))⇩ℝ)"
abbreviation vreal_mult_app (infixl "*⇩ℝ" 70)
where "vreal_mult_app a b ≡ vreal_mult⦇a, 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_uminus⦇a⦈"
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_inverse⦇a⦈"
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 (x⦇0⇩ℕ⦈) - real_of_vreal (x⦇1⇩ℕ⦈))⇩ℝ)"
abbreviation vreal_minus_app (infixl "-⇩ℝ" 65)
where "vreal_minus_app a b ≡ vreal_minus⦇a, 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 ∈⇩∘ ℝ⇩∘ ∧ (∀x∈⇩∘S. 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∈⇩∘ℝ⇩∘. ∀y∈⇩∘A. 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.›