|
1 (* Title: HOL/Real/ex/Sqrt.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 *) |
|
6 |
|
7 header {* Square roots of primes are irrational *} |
|
8 |
|
9 theory Sqrt = Primes + Real: |
|
10 |
|
11 syntax (xsymbols) (* FIXME move to main HOL (!?) *) |
|
12 "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999) |
|
13 syntax (HTML output) |
|
14 "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999) |
|
15 syntax (output) |
|
16 "_square" :: "'a => 'a" ("(_^2)" [1000] 999) |
|
17 translations |
|
18 "x\<twosuperior>" == "x^Suc (Suc 0)" |
|
19 |
|
20 |
|
21 subsection {* The set of rational numbers *} |
|
22 |
|
23 constdefs |
|
24 rationals :: "real set" ("\<rat>") |
|
25 "\<rat> == {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
|
26 |
|
27 theorem rationals_rep: "x \<in> \<rat> ==> |
|
28 \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1" |
|
29 proof - |
|
30 assume "x \<in> \<rat>" |
|
31 then obtain m n :: nat where n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" |
|
32 by (unfold rationals_def) blast |
|
33 let ?gcd = "gcd (m, n)" |
|
34 from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero) |
|
35 let ?k = "m div ?gcd" |
|
36 let ?l = "n div ?gcd" |
|
37 let ?gcd' = "gcd (?k, ?l)" |
|
38 have "?gcd dvd m" .. hence gcd_k: "?gcd * ?k = m" |
|
39 by (rule dvd_mult_div_cancel) |
|
40 have "?gcd dvd n" .. hence gcd_l: "?gcd * ?l = n" |
|
41 by (rule dvd_mult_div_cancel) |
|
42 |
|
43 from n gcd_l have "?l \<noteq> 0" |
|
44 by (auto iff del: neq0_conv) |
|
45 moreover |
|
46 have "\<bar>x\<bar> = real ?k / real ?l" |
|
47 proof - |
|
48 from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" |
|
49 by (simp add: real_mult_div_cancel1) |
|
50 also from gcd_k gcd_l have "... = real m / real n" by simp |
|
51 also from x_rat have "... = \<bar>x\<bar>" .. |
|
52 finally show ?thesis .. |
|
53 qed |
|
54 moreover |
|
55 have "?gcd' = 1" |
|
56 proof - |
|
57 have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)" |
|
58 by (rule gcd_mult_distrib2) |
|
59 with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp |
|
60 with gcd show ?thesis by simp |
|
61 qed |
|
62 ultimately show ?thesis by blast |
|
63 qed |
|
64 |
|
65 lemma [elim?]: "r \<in> \<rat> ==> |
|
66 (!!m n. n \<noteq> 0 ==> \<bar>r\<bar> = real m / real n ==> gcd (m, n) = 1 ==> C) |
|
67 ==> C" |
|
68 by (insert rationals_rep) blast |
|
69 |
|
70 |
|
71 subsection {* Main theorem *} |
|
72 |
|
73 text {* |
|
74 The square root of any prime number (including @{text 2}) is |
|
75 irrational. |
|
76 *} |
|
77 |
|
78 theorem sqrt_prime_irrational: "x\<twosuperior> = real p ==> p \<in> prime ==> x \<notin> \<rat>" |
|
79 proof |
|
80 assume x_sqrt: "x\<twosuperior> = real p" |
|
81 assume p_prime: "p \<in> prime" |
|
82 hence p: "1 < p" by (simp add: prime_def) |
|
83 assume "x \<in> \<rat>" |
|
84 then obtain m n where |
|
85 n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" and gcd: "gcd (m, n) = 1" .. |
|
86 have eq: "m\<twosuperior> = p * n\<twosuperior>" |
|
87 proof - |
|
88 from n x_rat have "real m = \<bar>x\<bar> * real n" by simp |
|
89 hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)" by (simp split: abs_split) |
|
90 also from x_sqrt have "... = real (p * n\<twosuperior>)" by simp |
|
91 finally show ?thesis .. |
|
92 qed |
|
93 have "p dvd m \<and> p dvd n" |
|
94 proof |
|
95 from eq have "p dvd m\<twosuperior>" .. |
|
96 with p_prime show "p dvd m" by (rule prime_dvd_square) |
|
97 then obtain k where "m = p * k" .. |
|
98 with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: mult_ac) |
|
99 with p have "n\<twosuperior> = p * k\<twosuperior>" by simp |
|
100 hence "p dvd n\<twosuperior>" .. |
|
101 with p_prime show "p dvd n" by (rule prime_dvd_square) |
|
102 qed |
|
103 hence "p dvd gcd (m, n)" .. |
|
104 with gcd have "p dvd 1" by simp |
|
105 hence "p \<le> 1" by (simp add: dvd_imp_le) |
|
106 with p show False by simp |
|
107 qed |
|
108 |
|
109 |
|
110 subsection {* Variations *} |
|
111 |
|
112 text {* |
|
113 Just for the record: we instantiate the main theorem for the |
|
114 specific prime number @{text 2} (real mathematicians would never do |
|
115 this formally :-). |
|
116 *} |
|
117 |
|
118 theorem "x\<twosuperior> = real (2::nat) ==> x \<notin> \<rat>" |
|
119 proof (rule sqrt_prime_irrational) |
|
120 { |
|
121 fix m :: nat assume dvd: "m dvd 2" |
|
122 hence "m \<le> 2" by (simp add: dvd_imp_le) |
|
123 moreover from dvd have "m \<noteq> 0" by (auto iff del: neq0_conv) |
|
124 ultimately have "m = 1 \<or> m = 2" by arith |
|
125 } |
|
126 thus "2 \<in> prime" by (simp add: prime_def) |
|
127 qed |
|
128 |
|
129 text {* |
|
130 \medskip An alternative version of the main proof, using mostly |
|
131 linear forward-reasoning. While this results in less top-down |
|
132 structure, it is probably closer to proofs seen in mathematics. |
|
133 *} |
|
134 |
|
135 theorem "x\<twosuperior> = real p ==> p \<in> prime ==> x \<notin> \<rat>" |
|
136 proof |
|
137 assume x_sqrt: "x\<twosuperior> = real p" |
|
138 assume p_prime: "p \<in> prime" |
|
139 hence p: "1 < p" by (simp add: prime_def) |
|
140 assume "x \<in> \<rat>" |
|
141 then obtain m n where |
|
142 n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" and gcd: "gcd (m, n) = 1" .. |
|
143 from n x_rat have "real m = \<bar>x\<bar> * real n" by simp |
|
144 hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)" by (simp split: abs_split) |
|
145 also from x_sqrt have "... = real (p * n\<twosuperior>)" by simp |
|
146 finally have eq: "m\<twosuperior> = p * n\<twosuperior>" .. |
|
147 hence "p dvd m\<twosuperior>" .. |
|
148 with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_square) |
|
149 then obtain k where "m = p * k" .. |
|
150 with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: mult_ac) |
|
151 with p have "n\<twosuperior> = p * k\<twosuperior>" by simp |
|
152 hence "p dvd n\<twosuperior>" .. |
|
153 with p_prime have "p dvd n" by (rule prime_dvd_square) |
|
154 with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest) |
|
155 with gcd have "p dvd 1" by simp |
|
156 hence "p \<le> 1" by (simp add: dvd_imp_le) |
|
157 with p show False by simp |
|
158 qed |
|
159 |
|
160 end |