author | haftmann |
Wed, 10 Feb 2010 08:49:26 +0100 | |
changeset 35084 | e25eedfc15ce |
parent 32479 | 521cc9bf2958 |
child 45917 | 1ce1bc9ff64a |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28001
diff
changeset
|
1 |
(* Title: HOL/ex/Sqrt.thy |
13957 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Square roots of primes are irrational *} |
|
6 |
||
15149 | 7 |
theory Sqrt |
32479 | 8 |
imports Complex_Main "~~/src/HOL/Number_Theory/Primes" |
15149 | 9 |
begin |
13957 | 10 |
|
11 |
text {* |
|
12 |
The square root of any prime number (including @{text 2}) is |
|
13 |
irrational. |
|
14 |
*} |
|
15 |
||
19086 | 16 |
theorem sqrt_prime_irrational: |
31712 | 17 |
assumes "prime (p::nat)" |
19086 | 18 |
shows "sqrt (real p) \<notin> \<rat>" |
13957 | 19 |
proof |
31712 | 20 |
from `prime p` have p: "1 < p" by (simp add: prime_nat_def) |
13957 | 21 |
assume "sqrt (real p) \<in> \<rat>" |
31712 | 22 |
then obtain m n :: nat where |
13957 | 23 |
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" |
30411 | 24 |
and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) |
13957 | 25 |
have eq: "m\<twosuperior> = p * n\<twosuperior>" |
26 |
proof - |
|
27 |
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp |
|
28 |
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
|
29 |
by (auto simp add: power2_eq_square) |
13957 | 30 |
also have "(sqrt (real p))\<twosuperior> = real p" by simp |
31 |
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp |
|
32 |
finally show ?thesis .. |
|
33 |
qed |
|
34 |
have "p dvd m \<and> p dvd n" |
|
35 |
proof |
|
36 |
from eq have "p dvd m\<twosuperior>" .. |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
37 |
with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat) |
13957 | 38 |
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
|
39 |
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
|
40 |
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) |
13957 | 41 |
then have "p dvd n\<twosuperior>" .. |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
42 |
with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat) |
13957 | 43 |
qed |
27556 | 44 |
then have "p dvd gcd m n" .. |
13957 | 45 |
with gcd have "p dvd 1" by simp |
46 |
then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
47 |
with p show False by simp |
|
48 |
qed |
|
49 |
||
50 |
corollary "sqrt (real (2::nat)) \<notin> \<rat>" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
51 |
by (rule sqrt_prime_irrational) (rule two_is_prime_nat) |
13957 | 52 |
|
53 |
||
54 |
subsection {* Variations *} |
|
55 |
||
56 |
text {* |
|
57 |
Here is an alternative version of the main proof, using mostly |
|
58 |
linear forward-reasoning. While this results in less top-down |
|
59 |
structure, it is probably closer to proofs seen in mathematics. |
|
60 |
*} |
|
61 |
||
19086 | 62 |
theorem |
31712 | 63 |
assumes "prime (p::nat)" |
19086 | 64 |
shows "sqrt (real p) \<notin> \<rat>" |
13957 | 65 |
proof |
31712 | 66 |
from `prime p` have p: "1 < p" by (simp add: prime_nat_def) |
13957 | 67 |
assume "sqrt (real p) \<in> \<rat>" |
31712 | 68 |
then obtain m n :: nat where |
13957 | 69 |
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" |
30411 | 70 |
and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) |
13957 | 71 |
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp |
72 |
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
|
73 |
by (auto simp add: power2_eq_square) |
13957 | 74 |
also have "(sqrt (real p))\<twosuperior> = real p" by simp |
75 |
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp |
|
76 |
finally have eq: "m\<twosuperior> = p * n\<twosuperior>" .. |
|
77 |
then have "p dvd m\<twosuperior>" .. |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
78 |
with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) |
13957 | 79 |
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
|
80 |
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
|
81 |
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) |
13957 | 82 |
then have "p dvd n\<twosuperior>" .. |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
83 |
with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
84 |
with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat) |
13957 | 85 |
with gcd have "p dvd 1" by simp |
86 |
then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
87 |
with p show False by simp |
|
88 |
qed |
|
89 |
||
90 |
end |