src/HOL/ex/Sqrt.thy
 changeset 30411 9c9b6511ad1b parent 28952 15a4b2cf8c34 child 31712 6f8aa9aea693
```--- a/src/HOL/ex/Sqrt.thy	Tue Mar 10 16:44:20 2009 +0100
+++ b/src/HOL/ex/Sqrt.thy	Tue Mar 10 16:48:27 2009 +0100
@@ -1,6 +1,5 @@
(*  Title:      HOL/ex/Sqrt.thy
Author:     Markus Wenzel, TU Muenchen
-
*)

header {*  Square roots of primes are irrational *}
@@ -9,13 +8,6 @@
imports Complex_Main Primes
begin

-text {* The definition and the key representation theorem for the set of
-rational numbers has been moved to a core theory.  *}
-
-declare Rats_abs_nat_div_natE[elim?]
-
-subsection {* Main theorem *}
-
text {*
The square root of any prime number (including @{text 2}) is
irrational.
@@ -29,7 +21,7 @@
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
-    and gcd: "gcd m n = 1" ..
+    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
have eq: "m\<twosuperior> = p * n\<twosuperior>"
proof -
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
@@ -75,7 +67,7 @@
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
-    and gcd: "gcd m n = 1" ..
+    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"