--- a/src/HOL/Real/Real.thy Sat Aug 23 19:42:17 2008 +0200
+++ b/src/HOL/Real/Real.thy Sat Aug 23 21:06:32 2008 +0200
@@ -1,4 +1,3 @@
-
(* $Id$ *)
theory Real
--- a/src/HOL/Real/RealDef.thy Sat Aug 23 19:42:17 2008 +0200
+++ b/src/HOL/Real/RealDef.thy Sat Aug 23 21:06:32 2008 +0200
@@ -37,7 +37,7 @@
definition
real_add_def [code func del]: "z + w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
- { Abs_Real(realrel``{(x+u, y+v)}) })"
+ { Abs_Real(realrel``{(x+u, y+v)}) })"
definition
real_minus_def [code func del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
@@ -49,7 +49,7 @@
real_mult_def [code func del]:
"z * w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
- { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
+ { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
definition
real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
@@ -558,6 +558,8 @@
where
"real_of_rat \<equiv> of_rat"
+definition [code func del]: "Rational = range of_rat"
+
consts
(*overloaded constant for injecting other types into "real"*)
real :: "'a => real"
@@ -700,7 +702,54 @@
done
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
- by (insert real_of_int_div2 [of n x], simp)
+by (insert real_of_int_div2 [of n x], simp)
+
+
+lemma Rational_eq_int_div_int:
+ "Rational = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
+proof
+ show "Rational \<subseteq> ?S"
+ proof
+ fix x::real assume "x : Rational"
+ then obtain r where "x = of_rat r" unfolding Rational_def ..
+ have "of_rat r : ?S"
+ by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
+ thus "x : ?S" using `x = of_rat r` by simp
+ qed
+next
+ show "?S \<subseteq> Rational"
+ proof(auto simp:Rational_def)
+ fix i j :: int assume "j \<noteq> 0"
+ hence "real i / real j = of_rat(Fract i j)"
+ by (simp add:of_rat_rat real_eq_of_int)
+ thus "real i / real j \<in> range of_rat" by blast
+ qed
+qed
+
+lemma Rational_eq_int_div_nat:
+ "Rational = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
+proof(auto simp:Rational_eq_int_div_int)
+ fix i j::int assume "j \<noteq> 0"
+ show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
+ proof cases
+ assume "j>0"
+ hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
+ by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
+ thus ?thesis by blast
+ next
+ assume "~ j>0"
+ hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
+ by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
+ thus ?thesis by blast
+ qed
+next
+ fix i::int and n::nat assume "0 < n"
+ moreover have "real n = real(int n)"
+ by (simp add: real_eq_of_int real_eq_of_nat)
+ ultimately show "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0"
+ by (fastsimp)
+qed
+
subsection{*Embedding the Naturals into the Reals*}
--- a/src/HOL/ex/Puzzle.thy Sat Aug 23 19:42:17 2008 +0200
+++ b/src/HOL/ex/Puzzle.thy Sat Aug 23 21:06:32 2008 +0200
@@ -5,7 +5,7 @@
header {* Fun with Functions *}
-theory Puzzle imports Main begin
+theory Puzzle imports Complex begin
text{* From \emph{Solving Mathematical Problems} by Terence Tao. He quotes
Greitzer's \emph{Interational Mathematical Olympiads 1959--1977} as the
@@ -104,6 +104,72 @@
qed
+text{* One more from Tao's booklet. If @{text f} is also assumed to be
+continuous, @{term"f(x::real) = x+1"} holds for all reals, not only
+rationals. Extend the proof!
+
+The definition of @{text Rats} should go somewhere else. *}
+
+definition "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
+
+theorem plus1:
+fixes f :: "real \<Rightarrow> real"
+assumes 0: "f 0 = 1" and f_add: "!!x y. f(x+y+1) = f x + f y"
+
+assumes "r : Rats"
+shows "f(r) = r + 1"
+proof -
+ { fix i :: int have "f(real i) = real i + 1"
+ proof (induct i rule: Presburger.int_induct[where k=0])
+ case base show ?case using 0 by simp
+ next
+ case (step1 i)
+ have "f(real(i+1)) = f(real i + 0 + 1)" by simp
+ also have "\<dots> = f(real i) + f 0" by(rule f_add)
+ also have "\<dots> = real(i+1) + 1" using step1 0 by simp
+ finally show ?case .
+ next
+ case (step2 i)
+ have "f(real i) = f(real(i - 1) + 0 + 1)" by simp
+ also have "\<dots> = f(real(i - 1)) + f 0" by(rule f_add)
+ also have "\<dots> = f(real(i - 1)) + 1 " using 0 by simp
+ finally show ?case using step2 by simp
+ qed }
+ note f_int = this
+ { fix n r have "f(real(Suc n)*r + real n) = real(Suc n) * f r"
+ proof(induct n)
+ case 0 show ?case by simp
+ next
+ case (Suc n)
+ have "real(Suc(Suc n))*r + real(Suc n) =
+ r + (real(Suc n)*r + real n) + 1" (is "?a = ?b")
+ by(simp add:real_of_nat_Suc ring_simps)
+ hence "f ?a = f ?b" by simp
+ also have "\<dots> = f r + f(real(Suc n)*r + real n)" by(rule f_add)
+ also have "\<dots> = f r + real(Suc n) * f r" by(simp only:Suc)
+ finally show ?case by(simp add:real_of_nat_Suc ring_simps)
+ qed }
+ note 1 = this
+ { fix n::nat and r assume "n>0"
+ have "f(real(n)*r + real(n - 1)) = real(n) * f r"
+ proof(cases n)
+ case 0 thus ?thesis using `n>0` by simp
+ next
+ case Suc thus ?thesis using `n>0` by (simp add:1)
+ qed }
+ note f_mult = this
+ from `r:Rats` obtain i::int and n::nat where r: "r = real i/real n" and "n>0"
+ by(fastsimp simp:Rats_def)
+ have "real(n)*f(real i/real n) = f(real i + real(n - 1))"
+ using `n>0` by(simp add:f_mult[symmetric])
+ also have "\<dots> = f(real(i + int n - 1))" using `n>0`
+ by (metis One_nat_def Suc_leI int_1 real_of_int_add real_of_int_of_nat_eq ring_class.ring_simps(4) zdiff_int)
+ also have "\<dots> = real(i + int n - 1) + 1" by(rule f_int)
+ also have "\<dots> = real i + real n" by arith
+ finally show ?thesis using `n>0` unfolding r by (simp add:field_simps)
+qed
+
+
text{* The only total model of a naive recursion equation of factorial on
integers is 0 for all negative arguments: *}