1.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Tue Aug 26 11:42:46 2008 +0200
     1.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Tue Aug 26 12:07:06 2008 +0200
     1.3 @@ -10,56 +10,10 @@
     1.4  imports Primes Complex_Main
     1.5  begin
     1.6  
     1.7 -subsection {* Preliminaries *}
     1.8 +text {* The definition and the key representation theorem for the set of
     1.9 +rational numbers has been moved to a core theory.  *}
    1.10  
    1.11 -text {*
    1.12 -  The set of rational numbers, including the key representation
    1.13 -  theorem.
    1.14 -*}
    1.15 -
    1.16 -definition
    1.17 -  rationals  ("\<rat>") where
    1.18 -  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
    1.19 -
    1.20 -theorem rationals_rep [elim?]:
    1.21 -  assumes "x \<in> \<rat>"
    1.22 -  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
    1.23 -proof -
    1.24 -  from `x \<in> \<rat>` obtain m n :: nat where
    1.25 -      n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
    1.26 -    unfolding rationals_def by blast
    1.27 -  let ?gcd = "gcd m n"
    1.28 -  from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
    1.29 -  let ?k = "m div ?gcd"
    1.30 -  let ?l = "n div ?gcd"
    1.31 -  let ?gcd' = "gcd ?k ?l"
    1.32 -  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
    1.33 -    by (rule dvd_mult_div_cancel)
    1.34 -  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
    1.35 -    by (rule dvd_mult_div_cancel)
    1.36 -
    1.37 -  from n and gcd_l have "?l \<noteq> 0"
    1.38 -    by (auto iff del: neq0_conv)
    1.39 -  moreover
    1.40 -  have "\<bar>x\<bar> = real ?k / real ?l"
    1.41 -  proof -
    1.42 -    from gcd have "real ?k / real ?l =
    1.43 -        real (?gcd * ?k) / real (?gcd * ?l)" by simp
    1.44 -    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
    1.45 -    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
    1.46 -    finally show ?thesis ..
    1.47 -  qed
    1.48 -  moreover
    1.49 -  have "?gcd' = 1"
    1.50 -  proof -
    1.51 -    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
    1.52 -      by (rule gcd_mult_distrib2)
    1.53 -    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    1.54 -    with gcd show ?thesis by simp
    1.55 -  qed
    1.56 -  ultimately show ?thesis ..
    1.57 -qed
    1.58 -
    1.59 +declare Rats_abs_nat_div_natE[elim?]
    1.60  
    1.61  subsection {* Main theorem *}
    1.62  

     2.1 --- a/src/HOL/Complex/ex/Sqrt_Script.thy	Tue Aug 26 11:42:46 2008 +0200
     2.2 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Tue Aug 26 12:07:06 2008 +0200
     2.3 @@ -50,13 +50,6 @@
     2.4    done
     2.5  
     2.6  
     2.7 -subsection {* The set of rational numbers *}
     2.8 -
     2.9 -definition
    2.10 -  rationals :: "real set"    ("\<rat>") where
    2.11 -  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
    2.12 -
    2.13 -
    2.14  subsection {* Main theorem *}
    2.15  
    2.16  text {*
    2.17 @@ -66,11 +59,10 @@
    2.18  
    2.19  theorem prime_sqrt_irrational:
    2.20      "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
    2.21 -  apply (simp add: rationals_def real_abs_def)
    2.22 -  apply clarify
    2.23 -  apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
    2.24 +  apply (rule notI)
    2.25 +  apply (erule Rats_abs_nat_div_natE)
    2.26    apply (simp del: real_of_nat_mult
    2.27 -              add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
    2.28 +              add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
    2.29    done
    2.30  
    2.31  lemmas two_sqrt_irrational =

     3.1 --- a/src/HOL/Real/Rational.thy	Tue Aug 26 11:42:46 2008 +0200
     3.2 +++ b/src/HOL/Real/Rational.thy	Tue Aug 26 12:07:06 2008 +0200
     3.3 @@ -674,6 +674,19 @@
     3.4    "rat_of_int \<equiv> of_int"
     3.5  
     3.6  
     3.7 +context field_char_0
     3.8 +begin
     3.9 +
    3.10 +definition
    3.11 +  Rats  :: "'a set" where
    3.12 +  [code func del]: "Rats = range of_rat"
    3.13 +
    3.14 +notation (xsymbols)
    3.15 +  Rats  ("\<rat>")
    3.16 +
    3.17 +end
    3.18 +
    3.19 +
    3.20  subsection {* Implementation of rational numbers as pairs of integers *}
    3.21  
    3.22  lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"

     4.1 --- a/src/HOL/Real/RealDef.thy	Tue Aug 26 11:42:46 2008 +0200
     4.2 +++ b/src/HOL/Real/RealDef.thy	Tue Aug 26 12:07:06 2008 +0200
     4.3 @@ -558,8 +558,6 @@
     4.4  where
     4.5    "real_of_rat \<equiv> of_rat"
     4.6  
     4.7 -definition [code func del]: "Rational = range of_rat"
     4.8 -
     4.9  consts
    4.10    (*overloaded constant for injecting other types into "real"*)
    4.11    real :: "'a => real"
    4.12 @@ -705,52 +703,6 @@
    4.13  by (insert real_of_int_div2 [of n x], simp)
    4.14  
    4.15  
    4.16 -lemma Rational_eq_int_div_int:
    4.17 -  "Rational = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
    4.18 -proof
    4.19 -  show "Rational \<subseteq> ?S"
    4.20 -  proof
    4.21 -    fix x::real assume "x : Rational"
    4.22 -    then obtain r where "x = of_rat r" unfolding Rational_def ..
    4.23 -    have "of_rat r : ?S"
    4.24 -      by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
    4.25 -    thus "x : ?S" using `x = of_rat r` by simp
    4.26 -  qed
    4.27 -next
    4.28 -  show "?S \<subseteq> Rational"
    4.29 -  proof(auto simp:Rational_def)
    4.30 -    fix i j :: int assume "j \<noteq> 0"
    4.31 -    hence "real i / real j = of_rat(Fract i j)"
    4.32 -      by (simp add:of_rat_rat real_eq_of_int)
    4.33 -    thus "real i / real j \<in> range of_rat" by blast
    4.34 -  qed
    4.35 -qed
    4.36 -
    4.37 -lemma Rational_eq_int_div_nat:
    4.38 -  "Rational = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    4.39 -proof(auto simp:Rational_eq_int_div_int)
    4.40 -  fix i j::int assume "j \<noteq> 0"
    4.41 -  show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
    4.42 -  proof cases
    4.43 -    assume "j>0"
    4.44 -    hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
    4.45 -      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
    4.46 -    thus ?thesis by blast
    4.47 -  next
    4.48 -    assume "~ j>0"
    4.49 -    hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
    4.50 -      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
    4.51 -    thus ?thesis by blast
    4.52 -  qed
    4.53 -next
    4.54 -  fix i::int and n::nat assume "0 < n"
    4.55 -  moreover have "real n = real(int n)"
    4.56 -    by (simp add: real_eq_of_int real_eq_of_nat)
    4.57 -  ultimately show "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0"
    4.58 -    by (fastsimp)
    4.59 -qed
    4.60 -
    4.61 -
    4.62  subsection{*Embedding the Naturals into the Reals*}
    4.63  
    4.64  lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
    4.65 @@ -892,6 +844,91 @@
    4.66    apply (simp only: real_of_int_real_of_nat)
    4.67  done
    4.68  
    4.69 +
    4.70 +subsection{* Rationals *}
    4.71 +
    4.72 +lemma Rats_eq_int_div_int:
    4.73 +  "Rats = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
    4.74 +proof
    4.75 +  show "Rats \<subseteq> ?S"
    4.76 +  proof
    4.77 +    fix x::real assume "x : Rats"
    4.78 +    then obtain r where "x = of_rat r" unfolding Rats_def ..
    4.79 +    have "of_rat r : ?S"
    4.80 +      by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
    4.81 +    thus "x : ?S" using `x = of_rat r` by simp
    4.82 +  qed
    4.83 +next
    4.84 +  show "?S \<subseteq> Rats"
    4.85 +  proof(auto simp:Rats_def)
    4.86 +    fix i j :: int assume "j \<noteq> 0"
    4.87 +    hence "real i / real j = of_rat(Fract i j)"
    4.88 +      by (simp add:of_rat_rat real_eq_of_int)
    4.89 +    thus "real i / real j \<in> range of_rat" by blast
    4.90 +  qed
    4.91 +qed
    4.92 +
    4.93 +lemma Rats_eq_int_div_nat:
    4.94 +  "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    4.95 +proof(auto simp:Rats_eq_int_div_int)
    4.96 +  fix i j::int assume "j \<noteq> 0"
    4.97 +  show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
    4.98 +  proof cases
    4.99 +    assume "j>0"
   4.100 +    hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
   4.101 +      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
   4.102 +    thus ?thesis by blast
   4.103 +  next
   4.104 +    assume "~ j>0"
   4.105 +    hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
   4.106 +      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
   4.107 +    thus ?thesis by blast
   4.108 +  qed
   4.109 +next
   4.110 +  fix i::int and n::nat assume "0 < n"
   4.111 +  hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp
   4.112 +  thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast
   4.113 +qed
   4.114 +
   4.115 +lemma Rats_abs_nat_div_natE:
   4.116 +  assumes "x \<in> \<rat>"
   4.117 +  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
   4.118 +proof -
   4.119 +  from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
   4.120 +    by(auto simp add: Rats_eq_int_div_nat)
   4.121 +  hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
   4.122 +  then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
   4.123 +  let ?gcd = "gcd m n"
   4.124 +  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
   4.125 +  let ?k = "m div ?gcd"
   4.126 +  let ?l = "n div ?gcd"
   4.127 +  let ?gcd' = "gcd ?k ?l"
   4.128 +  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
   4.129 +    by (rule dvd_mult_div_cancel)
   4.130 +  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
   4.131 +    by (rule dvd_mult_div_cancel)
   4.132 +  from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
   4.133 +  moreover
   4.134 +  have "\<bar>x\<bar> = real ?k / real ?l"
   4.135 +  proof -
   4.136 +    from gcd have "real ?k / real ?l =
   4.137 +        real (?gcd * ?k) / real (?gcd * ?l)" by simp
   4.138 +    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
   4.139 +    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
   4.140 +    finally show ?thesis ..
   4.141 +  qed
   4.142 +  moreover
   4.143 +  have "?gcd' = 1"
   4.144 +  proof -
   4.145 +    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
   4.146 +      by (rule gcd_mult_distrib2)
   4.147 +    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
   4.148 +    with gcd show ?thesis by simp
   4.149 +  qed
   4.150 +  ultimately show ?thesis ..
   4.151 +qed
   4.152 +
   4.153 +
   4.154  subsection{*Numerals and Arithmetic*}
   4.155  
   4.156  instantiation real :: number_ring

     5.1 --- a/src/HOL/ex/Puzzle.thy	Tue Aug 26 11:42:46 2008 +0200
     5.2 +++ b/src/HOL/ex/Puzzle.thy	Tue Aug 26 12:07:06 2008 +0200
     5.3 @@ -106,11 +106,9 @@
     5.4  
     5.5  text{* One more from Tao's booklet. If @{text f} is also assumed to be
     5.6  continuous, @{term"f(x::real) = x+1"} holds for all reals, not only
     5.7 -rationals. Extend the proof!
     5.8 +rationals. Extend the proof! *}
     5.9  
    5.10 -The definition of @{text Rats} should go somewhere else. *}
    5.11 -
    5.12 -definition "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    5.13 +ML{*ResAtp.set_prover "vampire"*}
    5.14  
    5.15  theorem plus1:
    5.16  fixes f :: "real \<Rightarrow> real"
    5.17 @@ -150,23 +148,23 @@
    5.18        finally show ?case by(simp add:real_of_nat_Suc ring_simps)
    5.19      qed }
    5.20    note 1 = this
    5.21 -  { fix n::nat and r assume "n>0"
    5.22 +  { fix n::nat and r assume "n\<noteq>0"
    5.23      have "f(real(n)*r + real(n - 1)) = real(n) * f r"
    5.24      proof(cases n)
    5.25 -      case 0 thus ?thesis using `n>0` by simp
    5.26 +      case 0 thus ?thesis using `n\<noteq>0` by simp
    5.27      next
    5.28 -      case Suc thus ?thesis using `n>0` by (simp add:1)
    5.29 +      case Suc thus ?thesis using `n\<noteq>0` by (simp add:1)
    5.30      qed }
    5.31    note f_mult = this
    5.32 -  from `r:Rats` obtain i::int and n::nat where r: "r = real i/real n" and "n>0"
    5.33 -    by(fastsimp simp:Rats_def)
    5.34 +  from `r:Rats` obtain i::int and n::nat where r: "r = real i/real n" and "n\<noteq>0"
    5.35 +    by(fastsimp simp:Rats_eq_int_div_nat)
    5.36    have "real(n)*f(real i/real n) = f(real i + real(n - 1))"
    5.37 -    using `n>0` by(simp add:f_mult[symmetric])
    5.38 -  also have "\<dots> = f(real(i + int n - 1))" using `n>0`
    5.39 +    using `n\<noteq>0` by(simp add:f_mult[symmetric])
    5.40 +  also have "\<dots> = f(real(i + int n - 1))" using `n\<noteq>0`[simplified]
    5.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)
    5.42    also have "\<dots> = real(i + int n - 1) + 1" by(rule f_int)
    5.43    also have "\<dots> = real i + real n" by arith
    5.44 -  finally show ?thesis using `n>0` unfolding r by (simp add:field_simps)
    5.45 +  finally show ?thesis using `n\<noteq>0` unfolding r by (simp add:field_simps)
    5.46  qed
    5.47  
    5.48