1.1 --- a/src/HOL/ex/Puzzle.thy	Tue Aug 26 11:42:46 2008 +0200
     1.2 +++ b/src/HOL/ex/Puzzle.thy	Tue Aug 26 12:07:06 2008 +0200
     1.3 @@ -106,11 +106,9 @@
     1.4  
     1.5  text{* One more from Tao's booklet. If @{text f} is also assumed to be
     1.6  continuous, @{term"f(x::real) = x+1"} holds for all reals, not only
     1.7 -rationals. Extend the proof!
     1.8 +rationals. Extend the proof! *}
     1.9  
    1.10 -The definition of @{text Rats} should go somewhere else. *}
    1.11 -
    1.12 -definition "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    1.13 +ML{*ResAtp.set_prover "vampire"*}
    1.14  
    1.15  theorem plus1:
    1.16  fixes f :: "real \<Rightarrow> real"
    1.17 @@ -150,23 +148,23 @@
    1.18        finally show ?case by(simp add:real_of_nat_Suc ring_simps)
    1.19      qed }
    1.20    note 1 = this
    1.21 -  { fix n::nat and r assume "n>0"
    1.22 +  { fix n::nat and r assume "n\<noteq>0"
    1.23      have "f(real(n)*r + real(n - 1)) = real(n) * f r"
    1.24      proof(cases n)
    1.25 -      case 0 thus ?thesis using `n>0` by simp
    1.26 +      case 0 thus ?thesis using `n\<noteq>0` by simp
    1.27      next
    1.28 -      case Suc thus ?thesis using `n>0` by (simp add:1)
    1.29 +      case Suc thus ?thesis using `n\<noteq>0` by (simp add:1)
    1.30      qed }
    1.31    note f_mult = this
    1.32 -  from `r:Rats` obtain i::int and n::nat where r: "r = real i/real n" and "n>0"
    1.33 -    by(fastsimp simp:Rats_def)
    1.34 +  from `r:Rats` obtain i::int and n::nat where r: "r = real i/real n" and "n\<noteq>0"
    1.35 +    by(fastsimp simp:Rats_eq_int_div_nat)
    1.36    have "real(n)*f(real i/real n) = f(real i + real(n - 1))"
    1.37 -    using `n>0` by(simp add:f_mult[symmetric])
    1.38 -  also have "\<dots> = f(real(i + int n - 1))" using `n>0`
    1.39 +    using `n\<noteq>0` by(simp add:f_mult[symmetric])
    1.40 +  also have "\<dots> = f(real(i + int n - 1))" using `n\<noteq>0`[simplified]
    1.41      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)
    1.42    also have "\<dots> = real(i + int n - 1) + 1" by(rule f_int)
    1.43    also have "\<dots> = real i + real n" by arith
    1.44 -  finally show ?thesis using `n>0` unfolding r by (simp add:field_simps)
    1.45 +  finally show ?thesis using `n\<noteq>0` unfolding r by (simp add:field_simps)
    1.46  qed
    1.47  
    1.48