# HG changeset patch
# User nipkow
# Date 1219518392 -7200
# Node ID 1e0303048c0b28187067864a8062289335ca06d4
# Parent  c9ea824441894c4d746c47a53115d9e980d9acbd
added const Rational
added more function puzzles

diff -r c9ea82444189 -r 1e0303048c0b src/HOL/Real/Real.thy
--- 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
diff -r c9ea82444189 -r 1e0303048c0b src/HOL/Real/RealDef.thy
--- 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*}
 
diff -r c9ea82444189 -r 1e0303048c0b src/HOL/ex/Puzzle.thy
--- 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: *}