author wenzelm Wed, 06 Mar 2002 18:16:48 +0100 changeset 13035 d3be9be2b307 parent 13034 d7bb6e4f5f82 child 13036 dca23533bdfb
tuned;
 src/HOL/Hyperreal/ex/Sqrt.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/ex/Sqrt_Script.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/ex/Sqrt.thy	Wed Mar 06 17:56:02 2002 +0100
+++ b/src/HOL/Hyperreal/ex/Sqrt.thy	Wed Mar 06 18:16:48 2002 +0100
@@ -23,7 +23,8 @@
\<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
proof -
assume "x \<in> \<rat>"
-  then obtain m n :: nat where n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
+  then obtain m n :: nat where
+      n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
by (unfold rationals_def) blast
let ?gcd = "gcd (m, n)"
from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
@@ -40,7 +41,8 @@
moreover
have "\<bar>x\<bar> = real ?k / real ?l"
proof -
-    from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)"
+    from gcd have "real ?k / real ?l =
+        real (?gcd * ?k) / real (?gcd * ?l)"
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
also from x_rat have "\<dots> = \<bar>x\<bar>" ..
@@ -103,12 +105,6 @@
with p show False by simp
qed

-text {*
-  Just for the record: we instantiate the main theorem for the
-  specific prime number @{text 2} (real mathematicians would never do
-  this formally :-).
-*}
-
corollary "sqrt (real (2::nat)) \<notin> \<rat>"
by (rule sqrt_prime_irrational) (rule two_is_prime)
```
```--- a/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 17:56:02 2002 +0100
+++ b/src/HOL/Hyperreal/ex/Sqrt_Script.thy	Wed Mar 06 18:16:48 2002 +0100
@@ -23,8 +23,8 @@
apply (rule_tac j = "k * k" in dvd_mult_left, simp)
done

-lemma reduction:
-    "p \<in> prime \<Longrightarrow> 0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
+lemma reduction: "p \<in> prime \<Longrightarrow>
+    0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
apply (rule ccontr)