1 (* Title: HOL/Hyperreal/ex/Sqrt.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 *) |
|
6 |
|
7 header {* Square roots of primes are irrational *} |
|
8 |
|
9 theory Sqrt |
|
10 imports Primes Complex_Main |
|
11 begin |
|
12 |
|
13 text {* The definition and the key representation theorem for the set of |
|
14 rational numbers has been moved to a core theory. *} |
|
15 |
|
16 declare Rats_abs_nat_div_natE[elim?] |
|
17 |
|
18 subsection {* Main theorem *} |
|
19 |
|
20 text {* |
|
21 The square root of any prime number (including @{text 2}) is |
|
22 irrational. |
|
23 *} |
|
24 |
|
25 theorem sqrt_prime_irrational: |
|
26 assumes "prime p" |
|
27 shows "sqrt (real p) \<notin> \<rat>" |
|
28 proof |
|
29 from `prime p` have p: "1 < p" by (simp add: prime_def) |
|
30 assume "sqrt (real p) \<in> \<rat>" |
|
31 then obtain m n where |
|
32 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" |
|
33 and gcd: "gcd m n = 1" .. |
|
34 have eq: "m\<twosuperior> = p * n\<twosuperior>" |
|
35 proof - |
|
36 from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp |
|
37 then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" |
|
38 by (auto simp add: power2_eq_square) |
|
39 also have "(sqrt (real p))\<twosuperior> = real p" by simp |
|
40 also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp |
|
41 finally show ?thesis .. |
|
42 qed |
|
43 have "p dvd m \<and> p dvd n" |
|
44 proof |
|
45 from eq have "p dvd m\<twosuperior>" .. |
|
46 with `prime p` show "p dvd m" by (rule prime_dvd_power_two) |
|
47 then obtain k where "m = p * k" .. |
|
48 with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac) |
|
49 with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) |
|
50 then have "p dvd n\<twosuperior>" .. |
|
51 with `prime p` show "p dvd n" by (rule prime_dvd_power_two) |
|
52 qed |
|
53 then have "p dvd gcd m n" .. |
|
54 with gcd have "p dvd 1" by simp |
|
55 then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
56 with p show False by simp |
|
57 qed |
|
58 |
|
59 corollary "sqrt (real (2::nat)) \<notin> \<rat>" |
|
60 by (rule sqrt_prime_irrational) (rule two_is_prime) |
|
61 |
|
62 |
|
63 subsection {* Variations *} |
|
64 |
|
65 text {* |
|
66 Here is an alternative version of the main proof, using mostly |
|
67 linear forward-reasoning. While this results in less top-down |
|
68 structure, it is probably closer to proofs seen in mathematics. |
|
69 *} |
|
70 |
|
71 theorem |
|
72 assumes "prime p" |
|
73 shows "sqrt (real p) \<notin> \<rat>" |
|
74 proof |
|
75 from `prime p` have p: "1 < p" by (simp add: prime_def) |
|
76 assume "sqrt (real p) \<in> \<rat>" |
|
77 then obtain m n where |
|
78 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" |
|
79 and gcd: "gcd m n = 1" .. |
|
80 from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp |
|
81 then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" |
|
82 by (auto simp add: power2_eq_square) |
|
83 also have "(sqrt (real p))\<twosuperior> = real p" by simp |
|
84 also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp |
|
85 finally have eq: "m\<twosuperior> = p * n\<twosuperior>" .. |
|
86 then have "p dvd m\<twosuperior>" .. |
|
87 with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two) |
|
88 then obtain k where "m = p * k" .. |
|
89 with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac) |
|
90 with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) |
|
91 then have "p dvd n\<twosuperior>" .. |
|
92 with `prime p` have "p dvd n" by (rule prime_dvd_power_two) |
|
93 with dvd_m have "p dvd gcd m n" by (rule gcd_greatest) |
|
94 with gcd have "p dvd 1" by simp |
|
95 then have "p \<le> 1" by (simp add: dvd_imp_le) |
|
96 with p show False by simp |
|
97 qed |
|
98 |
|
99 end |
|