|
(* The rational numbers as subset of the real type.
by Stefan Richter, TUM 2002.
This theory should really be subsumed by the construction of the
rational numbers as part of the development of the reals in
Real/Rational.thy. Any volunteers? (TN) *)
header {*The Rational Numbers*}
theory Rats
imports Complex_Main
begin
text{*A dense and countable subset of the @{text real} type was needed for
some measurability proofs. That is why I developed this
theory. Apparently, something similar exists in Isabelle2004 by now,
but I have not checked it for applicability yet.
To begin with, an injective function from $\mathbb{N}^2$ to
$\mathbb{N}$ is defined\footnote{The function as well as the proofs
are derived from a german recursion theory textbook
\cite[p.~85f]{Oberschelp1993}. Surjectivity is not needed here but
Larry Paulson suggested to prove it for completeness.}. Its inverse is
then a surjective
mapping into $\mathbb{N}^2$. Another iteration yields three natural
numbers, one for enumerator, denominator, and sign respectively. The
rationals are now exactly the range of the resulting function on
$\mathbb{N}$, which already proves
them countable, without even defining this concept. Much to my
delight, these functions could be reused for the simple
function integral properties.*}
definition
n2_to_n:: "(nat * nat) => nat" where
"n2_to_n pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
definition
n_to_n2:: "nat => (nat * nat)" where
"n_to_n2 = inv n2_to_n"
definition
n3_to_rat:: "nat => nat => nat => real" where
"n3_to_rat a b c = (if 2 dvd a then real b / real c else - real b /real c)"
definition
n_to_rat:: "nat => real" where
"n_to_rat n = (let (a,x) = n_to_n2 n ; (b,c) = n_to_n2 x in
n3_to_rat a b c)"
definition
Rats:: "real set" ("\") where
"\ = range n_to_rat"
lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
(*<*)proof (cases "2 dvd a")
case True
thus ?thesis by (rule dvd_mult2)
next
case False
hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
thus ?thesis by (rule dvd_mult)
qed(*>*)
lemma assumes eq: "n2_to_n (u,v) = n2_to_n (x,y)"
shows n2_to_n_help: "u+v ? x+y"
proof (rule classical)
assume "¬ ?thesis"
hence contrapos: "x+y < u+v"
by simp
have "n2_to_n (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
by (unfold n2_to_n_def) (simp add: Let_def)
also have "
= (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
by (simp only: div_mult_self1_is_m)
also have "
= (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
+ ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
proof -
have "2 dvd (x+y)*Suc(x+y)"
by (rule dvd2_a_x_suc_a)
hence "(x+y)*Suc(x+y) mod 2 = 0"
by (simp only: dvd_eq_mod_eq_0)
also
have "2 * Suc(x+y) mod 2 = 0"
by (rule mod_mult_self1_is_0)
ultimately have
"((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
by simp
thus ?thesis
by simp
qed
also have "
= ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
by (rule div_add1_eq[THEN sym])
also have "
= ((x+y+2)*Suc(x+y)) div 2"
by (simp only: add_mult_distrib[THEN sym])
also from contrapos have "
? ((Suc(u+v))*(u+v)) div 2"
by (simp only: mult_le_mono div_le_mono)
also have "
? n2_to_n (u,v)"
by (unfold n2_to_n_def) (simp add: Let_def)
finally show ?thesis
by (simp only: eq)
qed
lemma n2_to_n_inj: "inj n2_to_n"
proof -
{fix u v x y assume "n2_to_n (u,v) = n2_to_n (x,y)"
hence "u+v ? x+y" by (rule n2_to_n_help)
also from prems[THEN sym] have "x+y ? u+v"
by (rule n2_to_n_help)
finally have eq: "u+v = x+y" .
with prems have ux: "u=x"
by (simp add: n2_to_n_def Let_def)
with eq have vy: "v=y"
by simp
with ux have "(u,v) = (x,y)"
by simp
}
hence "!!x y. n2_to_n x = n2_to_n y ==> x=y"
by fast
thus ?thesis
by (unfold inj_on_def) simp
qed
lemma n_to_n2_surj: "surj n_to_n2"
by (simp only: n_to_n2_def n2_to_n_inj inj_imp_surj_inv)
theorem nat_nat_rats: "real (a::nat)/real (b::nat) ? \"
proof -
from n_to_n2_surj obtain x where "(a,b) = n_to_n2 x"
by (auto simp only: surj_def)
also from n_to_n2_surj obtain n where "(0,x) = n_to_n2 n"
by (auto simp only: surj_def)
moreover have "n3_to_rat 0 a b = real a/real b"
by (simp add: n3_to_rat_def)
ultimately have "real a/real b = n_to_rat n"
by (auto simp add: n_to_rat_def Let_def split: split_split)
hence "real a/real b ? range n_to_rat"
by (auto simp add: image_def)
thus ?thesis
by (simp add: Rats_def)
qed
(*<*)
theorem sum_of_naturals: (*Stolen from Isar_examples/Summation.thy by Markus Wenzel*)
"2 * (?i < Suc n. i) = n * (n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by (simp add: lessThan_Suc)
next
fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by (simp add: lessThan_Suc)
also assume "?S n = n * (n + 1)"
also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
finally show "?P (Suc n)" by simp
qed(*>*)
lemma n2_to_n_surj: "surj n2_to_n"(*<*)
proof (unfold surj_def)
{
fix z::nat
def r ? "Max {r. (?i < Suc r. i) ? z}"
def x ? "z - (?i < Suc r. i)"
have "?r. r ? (?i < Suc r. i)"
by (simp add: lessThan_Suc)
hence "finite {r. (?i < Suc r. i) ? z}"
by (rule NSLIMSEQ_finite_set)
also have "0 ? {r. (?i < Suc r. i) ? z}"
by (simp add: lessThan_Suc)
hence "{r. (?i < Suc r. i) ? z} ? {}"
by fast
ultimately have a: "r ? {r. (?i < Suc r. i) ? z} ? (?s ? {r. (?i < Suc r. i) ? z}. s ? r)"
by (simp add: r_def del:mem_Collect_eq)
{
assume "r
hence "r+1?x"
by simp
hence "(?i < Suc r. i)+(r+1)?z"
using x_def by arith
hence "(r+1) ? {r. (?i < Suc r. i) ? z}"
by (simp add: lessThan_Suc)
with a have "(r+1)?r"
by simp
}
hence b: "x?r"
by force
def y ? "r-x"
have "2*z=2*(?i < r + 1. i)+2*x"
using x_def a by simp arith
also have "
= r * (r+1) + 2*x"
using sum_of_naturals by simp
also have "
= (x+y)*(x+y+1)+2*x"
using y_def b by simp
also { have "2 dvd ((x+y)*(x+y+1))"
using dvd2_a_x_suc_a by simp }
hence "
= 2 * n2_to_n(x,y)"
using n2_to_n_def by (simp add: Let_def dvd_mult_div_cancel)
finally have "z=n2_to_n (x, y)"
by simp
}
thus "?y. ?x. y = n2_to_n x"
by fast
qed(*>*)
theorem minus_nat_nat_rats: "- real (a::nat)/real (b::nat) ? \"
proof -
from n_to_n2_surj obtain x where "(a,b) = n_to_n2 x"
by (auto simp only: surj_def)
also from n_to_n2_surj obtain n where "(1,x) = n_to_n2 n"
by (auto simp only: surj_def)
moreover have "n3_to_rat 1 a b = - real a/real b"
by (simp add: n3_to_rat_def)
ultimately have "- real a/real b = n_to_rat n"
by (auto simp add: n_to_rat_def Let_def split: split_split)
hence "- real a/real b ? range n_to_rat"
by (auto simp add: image_def)
thus ?thesis
by (simp add: Rats_def)
qed
text{*The following lemmata do not seem to exist in the @{text
Real} theory,
but I think they should. The proof is of unexpected complexity, since there are a
number of theorems on @{text abs}, conversion from @{text int} to @{text real}, etc.~missing. *}(*<*)
theorem int_int_rats: "real (a::int)/real (b::int) ? \"
proof (cases "real a/real b < 0")
case False
hence "(real a/real b) = ¦real a/real b¦"
by arith
also have "
= real ¦a¦/real ¦b¦"
by simp
also have "
= real (nat ¦a¦)/real (nat ¦b¦)" by simp
finally show ?thesis
by (simp only: nat_nat_rats)
next
case True
hence "(real a/real b) = -¦real a/real b¦"
by arith
also have "
= - real (nat ¦a¦)/real (nat ¦b¦)"
by (simp add: real_of_int_abs)
finally show ?thesis txt{*\nopagebreak*}
by (simp only: minus_nat_nat_rats)
qed
theorem assumes a: "z ? \"
shows rats_int_int: "? x y. z = real (x::int)/real (y::int)"
(*<*)proof -
from a obtain n where "z=n_to_rat n"
by (auto simp only: Rats_def)
also have " = (let (a,x) = n_to_n2 n ; (b,c) = n_to_n2 x in n3_to_rat a b c)" by (simp only: n_to_rat_def)
also have "
= n3_to_rat (fst (n_to_n2 n)) (fst (n_to_n2 (snd (n_to_n2 n)))) (snd (n_to_n2 (snd (n_to_n2 n))))"
by (simp add: Let_def split: split_split)
also obtain a b c where "
= n3_to_rat a b c" by blast
also have "? x y.
= real (x::int)/real (y::int)"
proof (cases "2 dvd a")
case True
hence "n3_to_rat a b c = real (int b)/real (int c)" by (simp add: n3_to_rat_def real_of_int_real_of_nat)
thus ?thesis by fast
next
case False
hence "n3_to_rat a b c = real (-int b)/real (int c)" by (simp add: n3_to_rat_def real_of_int_real_of_nat)
thus ?thesis by fast
qed
finally show ?thesis .
qed(*>*)
theorem assumes a: "z ? \"
shows rats_int_intnot0: "? x y. z = real (x::int)/real (y::int) ? y?0"
(*<*)proof -
from a have "? x y. z = real (x::int)/real (y::int)" by (rule rats_int_int)
then obtain x y where xy: "z = real (x::int) / real (y::int)" by fast
thus ?thesis
proof (cases "0=z")
case False
with xy have "y?0"
by simp
with xy show ?thesis by fast
next
case True
hence "z = real (0::int) / real (1::int) ? (1::int)?(0::int)" by simp
thus ?thesis by fast
qed
qed(*>*)
theorem assumes a: "a ? \" and b: "b ? \"
shows rats_plus_rats: "a+b ? \"
proof -
from a obtain x y where "a = real (x::int)/real (y::int) ? y?0"
by (force simp add: rats_int_intnot0)
also from b obtain xb yb where "b = real (xb::int)/real (yb::int) ? yb?0"
by (force simp add: rats_int_intnot0)
ultimately have yn0: "y?0" and ybn0: "yb?0"
and eq: "a+b = real x/real y + real xb/real yb"
by auto
note eq also from yn0 ybn0
have "
= real yb * real x / (real yb * real y) +
real y * real xb / (real yb * real y)" (is "_ = ?X/?Z + ?Y/?Z")
by (simp add: real_mult_commute)
also have "
= (?X + ?Y)/?Z"
by (rule add_divide_distrib[THEN sym])
also have "
= real (yb*x + y*xb) / real (yb*y)"
by (simp only: real_of_int_mult real_of_int_add)
finally show ?thesis by (simp only: int_int_rats)
qed
text {*The density proof was first to be adapted from a Mizar document
\cite{basrat}.
Alas, it depends on a
Gauss bracket (or floor function) that could not be found
anywhere in Isabelle/HOL; and
it turned out many lemmata are missing about the relation between
integers and reals. Fortunately, a much more
elementary proof was discovered in ``Real Analysis'' by H.L. Royden
(\cite{Royden1968} p. 32 ff).
It directly employs
the axiom of Archimedes, which is already in the \mbox{@{text RComplete}} theory.*}
lemma assumes nn: "0?x" and ord: "x
shows rats_dense_in_nn_real: "?r ? \. x
proof -
from ord have "0 < y-x" by simp
with reals_Archimedean obtain q::nat
where q: "inverse (real q) < y-x" and qpos: "0 < real q"
by auto
def p ? "LEAST n. y ? real (Suc n)/real q"
from reals_Archimedean2 obtain n::nat where "y * real q < real n"
by auto
with qpos have ex: "y ? real n/real q" (is "?P n")
by (simp add: pos_less_divide_eq[THEN sym])
also from nn ord have "¬ y ? real (0::nat) / real q"
by simp
ultimately have main: "(LEAST n. y ? real n/real q) = Suc p"
by (unfold p_def) (rule Least_Suc)
also from ex have "?P (LEAST x. ?P x)"
by (rule LeastI)
ultimately have suc: "y ? real (Suc p) / real q"
by simp
def r ? "real p/real q"
have "x=y-(y-x)"
by simp
also from suc q have "
< real (Suc p)/real q - inverse (real q)"
by arith
also have "
= real p / real q"
by (simp only: inverse_eq_divide real_diff_def real_of_nat_Suc
minus_divide_left add_divide_distrib[THEN sym]) simp
finally have 1: "x
by (unfold r_def)
have "p .. also note main[THEN sym]
finally have "¬ ?P p"
by (rule not_less_Least)
hence 2: "r
by (simp add: r_def)
from r_def have "r ? \"
by (simp only: nat_nat_rats)
txt{*\nopagebreak*}
with 1 2 show ?thesis by fast
qed
theorem assumes ord: "x
shows rats_dense_in_real: "?r ? \. x
proof -
from reals_Archimedean2 obtain n::nat where "-x < real n"
by auto
hence "0 ? x + real n"
by arith
also from ord have "x + real n < y + real n"
by arith
ultimately have "?r ? \. x + real n < r ? r < y + real n"
by (rule rats_dense_in_nn_real)
then obtain r where r1: "r ? \" and r2: "x + real n < r"
and r3: "r < y + real n"
by blast
have "r - real n = r + real (int n)/real (-1::int)"
by (simp add: real_of_int_real_of_nat)
also from r1 have "r + real (int n)/real (-1::int) ? \"
by (simp only: int_int_rats rats_plus_rats)
also from r2 have "x < r - real n"
by arith
moreover from r3 have "r - real n < y"
by arith
ultimately show ?thesis
by fast
qed
(*This wraps up the most essential properties of the rational numbers,
though there are many more to establish, of course *)
end
lemma dvd2_a_x_suc_a:
2 dvd a * Suc a
lemma n2_to_n_help:
n2_to_n (u, v) = n2_to_n (x, y) ==> u + v ? x + y
lemma n2_to_n_inj:
inj n2_to_n
lemma n_to_n2_surj:
surj n_to_n2
theorem nat_nat_rats:
real a / real b ? \<rat>
theorem sum_of_naturals:
2 * ?{..<Suc n} = n * (n + 1)
lemma n2_to_n_surj:
surj n2_to_n
theorem minus_nat_nat_rats:
- real a / real b ? \<rat>
theorem int_int_rats:
real a / real b ? \<rat>
theorem rats_int_int:
z ? \<rat> ==> ?x y. z = real x / real y
theorem rats_int_intnot0:
z ? \<rat> ==> ?x y. z = real x / real y ? y ? 0
theorem rats_plus_rats:
[| a ? \<rat>; b ? \<rat> |] ==> a + b ? \<rat>
lemma rats_dense_in_nn_real:
[| 0 ? x; x < y |] ==> ?r?\<rat>. x < r ? r < y
theorem rats_dense_in_real:
x < y ==> ?r?\<rat>. x < r ? r < y
[ zur Elbe Produktseite wechseln0.31Quellennavigators
Analyse erneut starten
]
|
