author | wenzelm |
Thu, 16 Feb 2006 21:12:00 +0100 | |
changeset 19086 | 1b3780be6cc2 |
parent 16663 | 13e9c402308b |
child 21404 | eb85850d3eb7 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: HOL/Hyperreal/ex/Sqrt.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
14981 | 4 |
|
13957 | 5 |
*) |
6 |
||
7 |
header {* Square roots of primes are irrational *} |
|
8 |
||
15149 | 9 |
theory Sqrt |
10 |
imports Primes Complex_Main |
|
11 |
begin |
|
13957 | 12 |
|
13 |
subsection {* Preliminaries *} |
|
14 |
||
15 |
text {* |
|
16 |
The set of rational numbers, including the key representation |
|
17 |
theorem. |
|
18 |
*} |
|
19 |
||
19086 | 20 |
definition |
21 |
rationals ("\<rat>") |
|
22 |
"\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
|
13957 | 23 |
|
19086 | 24 |
theorem rationals_rep [elim?]: |
25 |
assumes "x \<in> \<rat>" |
|
26 |
obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1" |
|
13957 | 27 |
proof - |
19086 | 28 |
from `x \<in> \<rat>` obtain m n :: nat where |
13957 | 29 |
n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" |
19086 | 30 |
unfolding rationals_def by blast |
13957 | 31 |
let ?gcd = "gcd (m, n)" |
32 |
from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero) |
|
33 |
let ?k = "m div ?gcd" |
|
34 |
let ?l = "n div ?gcd" |
|
35 |
let ?gcd' = "gcd (?k, ?l)" |
|
36 |
have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m" |
|
37 |
by (rule dvd_mult_div_cancel) |
|
38 |
have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n" |
|
39 |
by (rule dvd_mult_div_cancel) |
|
40 |
||
41 |
from n and gcd_l have "?l \<noteq> 0" |
|
42 |
by (auto iff del: neq0_conv) |
|
43 |
moreover |
|
44 |
have "\<bar>x\<bar> = real ?k / real ?l" |
|
45 |
proof - |
|
46 |
from gcd have "real ?k / real ?l = |
|
47 |
real (?gcd * ?k) / real (?gcd * ?l)" |
|
14305
f17ca9f6dc8c
tidying first part of HyperArith0.ML, using generic lemmas
paulson
parents:
14051
diff
changeset
|
48 |
by (simp add: mult_divide_cancel_left) |
13957 | 49 |
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp |
50 |
also from x_rat have "\<dots> = \<bar>x\<bar>" .. |
|
51 |
finally show ?thesis .. |
|
52 |
qed |
|
53 |
moreover |
|
54 |
have "?gcd' = 1" |
|
55 |
proof - |
|
56 |
have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)" |
|
57 |
by (rule gcd_mult_distrib2) |
|
58 |
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp |
|
59 |
with gcd show ?thesis by simp |
|
60 |
qed |
|
19086 | 61 |
ultimately show ?thesis .. |
13957 | 62 |
qed |
63 |
||
64 |
||
65 |
subsection {* Main theorem *} |
|
66 |
||
67 |
text {* |
|
68 |
The square root of any prime number (including @{text 2}) is |
|
69 |
irrational. |
|
70 |
*} |
|
71 |
||
19086 | 72 |
theorem sqrt_prime_irrational: |
73 |
assumes "prime p" |
|
74 |
shows "sqrt (real p) \<notin> \<rat>" |
|
13957 | 75 |
proof |
19086 | 76 |
from `prime p` have p: "1 < p" by (simp add: prime_def) |
13957 | 77 |
assume "sqrt (real p) \<in> \<rat>" |
78 |
then obtain m n where |
|
79 |
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" |
|
80 |
and gcd: "gcd (m, n) = 1" .. |
|
81 |
have eq: "m\<twosuperior> = p * n\<twosuperior>" |
|
82 |
proof - |
|
83 |
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp |
|
84 |
then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
85 |
by (auto simp add: power2_eq_square) |
13957 | 86 |
also have "(sqrt (real p))\<twosuperior> = real p" by simp |
87 |
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp |
|
88 |
finally show ?thesis .. |
|
89 |
qed |
|
90 |
have "p dvd m \<and> p dvd n" |
|
91 |
proof |
|
92 |
from eq have "p dvd m\<twosuperior>" .. |
|
19086 | 93 |
with `prime p` show "p dvd m" by (rule prime_dvd_power_two) |
13957 | 94 |
then obtain k where "m = p * k" .. |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
95 |
with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
96 |
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) |
13957 | 97 |
then have "p dvd n\<twosuperior>" .. |
19086 | 98 |
with `prime p` show "p dvd n" by (rule prime_dvd_power_two) |
13957 | 99 |
qed |
100 |
then have "p dvd gcd (m, n)" .. |
|
101 |
with gcd have "p dvd 1" by simp |
|
102 |
then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
103 |
with p show False by simp |
|
104 |
qed |
|
105 |
||
106 |
corollary "sqrt (real (2::nat)) \<notin> \<rat>" |
|
107 |
by (rule sqrt_prime_irrational) (rule two_is_prime) |
|
108 |
||
109 |
||
110 |
subsection {* Variations *} |
|
111 |
||
112 |
text {* |
|
113 |
Here is an alternative version of the main proof, using mostly |
|
114 |
linear forward-reasoning. While this results in less top-down |
|
115 |
structure, it is probably closer to proofs seen in mathematics. |
|
116 |
*} |
|
117 |
||
19086 | 118 |
theorem |
119 |
assumes "prime p" |
|
120 |
shows "sqrt (real p) \<notin> \<rat>" |
|
13957 | 121 |
proof |
19086 | 122 |
from `prime p` have p: "1 < p" by (simp add: prime_def) |
13957 | 123 |
assume "sqrt (real p) \<in> \<rat>" |
124 |
then obtain m n where |
|
125 |
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" |
|
126 |
and gcd: "gcd (m, n) = 1" .. |
|
127 |
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp |
|
128 |
then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
129 |
by (auto simp add: power2_eq_square) |
13957 | 130 |
also have "(sqrt (real p))\<twosuperior> = real p" by simp |
131 |
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp |
|
132 |
finally have eq: "m\<twosuperior> = p * n\<twosuperior>" .. |
|
133 |
then have "p dvd m\<twosuperior>" .. |
|
19086 | 134 |
with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two) |
13957 | 135 |
then obtain k where "m = p * k" .. |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
136 |
with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
137 |
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) |
13957 | 138 |
then have "p dvd n\<twosuperior>" .. |
19086 | 139 |
with `prime p` have "p dvd n" by (rule prime_dvd_power_two) |
13957 | 140 |
with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest) |
141 |
with gcd have "p dvd 1" by simp |
|
142 |
then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
143 |
with p show False by simp |
|
144 |
qed |
|
145 |
||
146 |
end |