equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Sqrt.thy 
1 (* Title: HOL/ex/Sqrt.thy 
2 Author: Markus Wenzel, TU Muenchen 
2 Author: Markus Wenzel, TU Muenchen 
3 

4 *) 
3 *) 
5 
4 
6 header {* Square roots of primes are irrational *} 
5 header {* Square roots of primes are irrational *} 
7 
6 
8 theory Sqrt 
7 theory Sqrt 
9 imports Complex_Main Primes 
8 imports Complex_Main Primes 
10 begin 
9 begin 
11 

12 text {* The definition and the key representation theorem for the set of 

13 rational numbers has been moved to a core theory. *} 

14 

15 declare Rats_abs_nat_div_natE[elim?] 

16 

17 subsection {* Main theorem *} 

18 
10 
19 text {* 
11 text {* 
20 The square root of any prime number (including @{text 2}) is 
12 The square root of any prime number (including @{text 2}) is 
21 irrational. 
13 irrational. 
22 *} 
14 *} 
27 proof 
19 proof 
28 from `prime p` have p: "1 < p" by (simp add: prime_def) 
20 from `prime p` have p: "1 < p" by (simp add: prime_def) 
29 assume "sqrt (real p) \<in> \<rat>" 
21 assume "sqrt (real p) \<in> \<rat>" 
30 then obtain m n where 
22 then obtain m n where 
31 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" 
23 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" 
32 and gcd: "gcd m n = 1" .. 
24 and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) 
33 have eq: "m\<twosuperior> = p * n\<twosuperior>" 
25 have eq: "m\<twosuperior> = p * n\<twosuperior>" 
34 proof  
26 proof  
35 from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp 
27 from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp 
36 then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" 
28 then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" 
37 by (auto simp add: power2_eq_square) 
29 by (auto simp add: power2_eq_square) 
73 proof 
65 proof 
74 from `prime p` have p: "1 < p" by (simp add: prime_def) 
66 from `prime p` have p: "1 < p" by (simp add: prime_def) 
75 assume "sqrt (real p) \<in> \<rat>" 
67 assume "sqrt (real p) \<in> \<rat>" 
76 then obtain m n where 
68 then obtain m n where 
77 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" 
69 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" 
78 and gcd: "gcd m n = 1" .. 
70 and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) 
79 from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp 
71 from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp 
80 then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" 
72 then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" 
81 by (auto simp add: power2_eq_square) 
73 by (auto simp add: power2_eq_square) 
82 also have "(sqrt (real p))\<twosuperior> = real p" by simp 
74 also have "(sqrt (real p))\<twosuperior> = real p" by simp 
83 also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp 
75 also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp 