author wenzelm Tue, 10 Mar 2009 16:48:27 +0100 changeset 30411 9c9b6511ad1b parent 30410 ef670320e281 child 30412 7f5b0a020ccd
tuned proofs; tuned document;
 src/HOL/ex/Sqrt.thy file | annotate | diff | comparison | revisions
```--- 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>)"
by (auto simp add: power2_eq_square)```