author | wenzelm |
Sat, 22 Nov 2014 14:57:04 +0100 | |
changeset 59031 | 4c3bb56b8ce7 |
parent 58889 | 5b7a9633cfa8 |
child 60690 | a9e45c9588c3 |
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 |
45917 | 2 |
Author: Markus Wenzel, Tobias Nipkow, TU Muenchen |
13957 | 3 |
*) |
4 |
||
59031 | 5 |
section \<open>Square roots of primes are irrational\<close> |
13957 | 6 |
|
15149 | 7 |
theory Sqrt |
32479 | 8 |
imports Complex_Main "~~/src/HOL/Number_Theory/Primes" |
15149 | 9 |
begin |
13957 | 10 |
|
59031 | 11 |
text \<open>The square root of any prime number (including 2) is irrational.\<close> |
13957 | 12 |
|
19086 | 13 |
theorem sqrt_prime_irrational: |
31712 | 14 |
assumes "prime (p::nat)" |
51708 | 15 |
shows "sqrt p \<notin> \<rat>" |
13957 | 16 |
proof |
59031 | 17 |
from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def) |
51708 | 18 |
assume "sqrt p \<in> \<rat>" |
31712 | 19 |
then obtain m n :: nat where |
51708 | 20 |
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n" |
30411 | 21 |
and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
22 |
have eq: "m\<^sup>2 = p * n\<^sup>2" |
13957 | 23 |
proof - |
51708 | 24 |
from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
25 |
then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
26 |
by (auto simp add: power2_eq_square) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
27 |
also have "(sqrt p)\<^sup>2 = p" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
28 |
also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp |
13957 | 29 |
finally show ?thesis .. |
30 |
qed |
|
31 |
have "p dvd m \<and> p dvd n" |
|
32 |
proof |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
33 |
from eq have "p dvd m\<^sup>2" .. |
59031 | 34 |
with \<open>prime p\<close> show "p dvd m" by (rule prime_dvd_power_nat) |
13957 | 35 |
then obtain k where "m = p * k" .. |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
53598
diff
changeset
|
36 |
with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
37 |
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
38 |
then have "p dvd n\<^sup>2" .. |
59031 | 39 |
with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat) |
13957 | 40 |
qed |
27556 | 41 |
then have "p dvd gcd m n" .. |
13957 | 42 |
with gcd have "p dvd 1" by simp |
43 |
then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
44 |
with p show False by simp |
|
45 |
qed |
|
46 |
||
51708 | 47 |
corollary sqrt_2_not_rat: "sqrt 2 \<notin> \<rat>" |
48 |
using sqrt_prime_irrational[of 2] by simp |
|
13957 | 49 |
|
50 |
||
59031 | 51 |
subsection \<open>Variations\<close> |
52 |
||
53 |
text \<open> |
|
13957 | 54 |
Here is an alternative version of the main proof, using mostly |
55 |
linear forward-reasoning. While this results in less top-down |
|
56 |
structure, it is probably closer to proofs seen in mathematics. |
|
59031 | 57 |
\<close> |
13957 | 58 |
|
19086 | 59 |
theorem |
31712 | 60 |
assumes "prime (p::nat)" |
51708 | 61 |
shows "sqrt p \<notin> \<rat>" |
13957 | 62 |
proof |
59031 | 63 |
from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def) |
51708 | 64 |
assume "sqrt p \<in> \<rat>" |
31712 | 65 |
then obtain m n :: nat where |
51708 | 66 |
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n" |
30411 | 67 |
and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) |
51708 | 68 |
from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
69 |
then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14305
diff
changeset
|
70 |
by (auto simp add: power2_eq_square) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
71 |
also have "(sqrt p)\<^sup>2 = p" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
72 |
also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
73 |
finally have eq: "m\<^sup>2 = p * n\<^sup>2" .. |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
74 |
then have "p dvd m\<^sup>2" .. |
59031 | 75 |
with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) |
13957 | 76 |
then obtain k where "m = p * k" .. |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
53598
diff
changeset
|
77 |
with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
78 |
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51708
diff
changeset
|
79 |
then have "p dvd n\<^sup>2" .. |
59031 | 80 |
with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31712
diff
changeset
|
81 |
with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat) |
13957 | 82 |
with gcd have "p dvd 1" by simp |
83 |
then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
84 |
with p show False by simp |
|
85 |
qed |
|
86 |
||
45917 | 87 |
|
59031 | 88 |
text \<open>Another old chestnut, which is a consequence of the irrationality of 2.\<close> |
45917 | 89 |
|
59031 | 90 |
lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "\<exists>a b. ?P a b") |
45917 | 91 |
proof cases |
92 |
assume "sqrt 2 powr sqrt 2 \<in> \<rat>" |
|
46495 | 93 |
then have "?P (sqrt 2) (sqrt 2)" |
51708 | 94 |
by (metis sqrt_2_not_rat) |
46495 | 95 |
then show ?thesis by blast |
45917 | 96 |
next |
97 |
assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>" |
|
98 |
have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" |
|
46495 | 99 |
using powr_realpow [of _ 2] |
100 |
by (simp add: powr_powr power2_eq_square [symmetric]) |
|
101 |
then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" |
|
51708 | 102 |
by (metis 1 Rats_number_of sqrt_2_not_rat) |
46495 | 103 |
then show ?thesis by blast |
45917 | 104 |
qed |
105 |
||
13957 | 106 |
end |