# HG changeset patch
# User nipkow
# Date 1219745226 -7200
# Node ID 4642317e0deb78ace43cb6d9e2cf67f31e04d49b
# Parent  ca56bbb9960767daf5fd60ca674c8c928e771c80
Defined rationals (Rats) globally in Rational.
Chractarized them with a few lemmas in RealDef, one of them from Sqrt.

diff -r ca56bbb99607 -r 4642317e0deb src/HOL/Complex/ex/Sqrt.thy
--- a/src/HOL/Complex/ex/Sqrt.thy	Tue Aug 26 11:42:46 2008 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy	Tue Aug 26 12:07:06 2008 +0200
@@ -10,56 +10,10 @@
 imports Primes Complex_Main
 begin
 
-subsection {* Preliminaries *}
-
-text {*
-  The set of rational numbers, including the key representation
-  theorem.
-*}
-
-definition
-  rationals  ("\<rat>") where
-  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
+text {* The definition and the key representation theorem for the set of
+rational numbers has been moved to a core theory.  *}
 
-theorem rationals_rep [elim?]:
-  assumes "x \<in> \<rat>"
-  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
-proof -
-  from `x \<in> \<rat>` obtain m n :: nat where
-      n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
-    unfolding rationals_def by blast
-  let ?gcd = "gcd m n"
-  from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
-  let ?k = "m div ?gcd"
-  let ?l = "n div ?gcd"
-  let ?gcd' = "gcd ?k ?l"
-  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
-    by (rule dvd_mult_div_cancel)
-  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
-    by (rule dvd_mult_div_cancel)
-
-  from n and gcd_l have "?l \<noteq> 0"
-    by (auto iff del: neq0_conv)
-  moreover
-  have "\<bar>x\<bar> = real ?k / real ?l"
-  proof -
-    from gcd have "real ?k / real ?l =
-        real (?gcd * ?k) / real (?gcd * ?l)" by simp
-    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
-    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
-    finally show ?thesis ..
-  qed
-  moreover
-  have "?gcd' = 1"
-  proof -
-    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
-      by (rule gcd_mult_distrib2)
-    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
-    with gcd show ?thesis by simp
-  qed
-  ultimately show ?thesis ..
-qed
-
+declare Rats_abs_nat_div_natE[elim?]
 
 subsection {* Main theorem *}
 
diff -r ca56bbb99607 -r 4642317e0deb src/HOL/Complex/ex/Sqrt_Script.thy
--- a/src/HOL/Complex/ex/Sqrt_Script.thy	Tue Aug 26 11:42:46 2008 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Tue Aug 26 12:07:06 2008 +0200
@@ -50,13 +50,6 @@
   done
 
 
-subsection {* The set of rational numbers *}
-
-definition
-  rationals :: "real set"    ("\<rat>") where
-  "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
-
-
 subsection {* Main theorem *}
 
 text {*
@@ -66,11 +59,10 @@
 
 theorem prime_sqrt_irrational:
     "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
-  apply (simp add: rationals_def real_abs_def)
-  apply clarify
-  apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
+  apply (rule notI)
+  apply (erule Rats_abs_nat_div_natE)
   apply (simp del: real_of_nat_mult
-              add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
+              add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
   done
 
 lemmas two_sqrt_irrational =
diff -r ca56bbb99607 -r 4642317e0deb src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Tue Aug 26 11:42:46 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Tue Aug 26 12:07:06 2008 +0200
@@ -674,6 +674,19 @@
   "rat_of_int \<equiv> of_int"
 
 
+context field_char_0
+begin
+
+definition
+  Rats  :: "'a set" where
+  [code func del]: "Rats = range of_rat"
+
+notation (xsymbols)
+  Rats  ("\<rat>")
+
+end
+
+
 subsection {* Implementation of rational numbers as pairs of integers *}
 
 lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"
diff -r ca56bbb99607 -r 4642317e0deb src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Aug 26 11:42:46 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Aug 26 12:07:06 2008 +0200
@@ -558,8 +558,6 @@
 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"
@@ -705,52 +703,6 @@
 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*}
 
 lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
@@ -892,6 +844,91 @@
   apply (simp only: real_of_int_real_of_nat)
 done
 
+
+subsection{* Rationals *}
+
+lemma Rats_eq_int_div_int:
+  "Rats = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
+proof
+  show "Rats \<subseteq> ?S"
+  proof
+    fix x::real assume "x : Rats"
+    then obtain r where "x = of_rat r" unfolding Rats_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> Rats"
+  proof(auto simp:Rats_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 Rats_eq_int_div_nat:
+  "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
+proof(auto simp:Rats_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"
+  hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp
+  thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast
+qed
+
+lemma Rats_abs_nat_div_natE:
+  assumes "x \<in> \<rat>"
+  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
+proof -
+  from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
+    by(auto simp add: Rats_eq_int_div_nat)
+  hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
+  then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
+  let ?gcd = "gcd m n"
+  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
+  let ?k = "m div ?gcd"
+  let ?l = "n div ?gcd"
+  let ?gcd' = "gcd ?k ?l"
+  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
+    by (rule dvd_mult_div_cancel)
+  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
+    by (rule dvd_mult_div_cancel)
+  from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
+  moreover
+  have "\<bar>x\<bar> = real ?k / real ?l"
+  proof -
+    from gcd have "real ?k / real ?l =
+        real (?gcd * ?k) / real (?gcd * ?l)" by simp
+    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
+    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
+    finally show ?thesis ..
+  qed
+  moreover
+  have "?gcd' = 1"
+  proof -
+    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
+      by (rule gcd_mult_distrib2)
+    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
+    with gcd show ?thesis by simp
+  qed
+  ultimately show ?thesis ..
+qed
+
+
 subsection{*Numerals and Arithmetic*}
 
 instantiation real :: number_ring
diff -r ca56bbb99607 -r 4642317e0deb src/HOL/ex/Puzzle.thy
--- a/src/HOL/ex/Puzzle.thy	Tue Aug 26 11:42:46 2008 +0200
+++ b/src/HOL/ex/Puzzle.thy	Tue Aug 26 12:07:06 2008 +0200
@@ -106,11 +106,9 @@
 
 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!
+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}"
+ML{*ResAtp.set_prover "vampire"*}
 
 theorem plus1:
 fixes f :: "real \<Rightarrow> real"
@@ -150,23 +148,23 @@
       finally show ?case by(simp add:real_of_nat_Suc ring_simps)
     qed }
   note 1 = this
-  { fix n::nat and r assume "n>0"
+  { fix n::nat and r assume "n\<noteq>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
+      case 0 thus ?thesis using `n\<noteq>0` by simp
     next
-      case Suc thus ?thesis using `n>0` by (simp add:1)
+      case Suc thus ?thesis using `n\<noteq>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)
+  from `r:Rats` obtain i::int and n::nat where r: "r = real i/real n" and "n\<noteq>0"
+    by(fastsimp simp:Rats_eq_int_div_nat)
   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`
+    using `n\<noteq>0` by(simp add:f_mult[symmetric])
+  also have "\<dots> = f(real(i + int n - 1))" using `n\<noteq>0`[simplified]
     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)
+  finally show ?thesis using `n\<noteq>0` unfolding r by (simp add:field_simps)
 qed