author  wenzelm 
Tue, 10 Mar 2009 16:48:27 +0100  
changeset 30411  9c9b6511ad1b 
parent 28952  15a4b2cf8c34 
child 31712  6f8aa9aea693 
permissions  rwrr 
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 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28001
diff
changeset

8 
imports Complex_Main 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: 
17 
assumes "prime p" 

18 
shows "sqrt (real p) \<notin> \<rat>" 

13957  19 
proof 
19086  20 
from `prime p` have p: "1 < p" by (simp add: prime_def) 
13957  21 
assume "sqrt (real p) \<in> \<rat>" 
22 
then obtain m n where 

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>" .. 

19086  37 
with `prime p` show "p dvd m" by (rule prime_dvd_power_two) 
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>" .. 
19086  42 
with `prime p` show "p dvd n" by (rule prime_dvd_power_two) 
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>" 

51 
by (rule sqrt_prime_irrational) (rule two_is_prime) 

52 

53 

54 
subsection {* Variations *} 

55 

56 
text {* 

57 
Here is an alternative version of the main proof, using mostly 

58 
linear forwardreasoning. While this results in less topdown 

59 
structure, it is probably closer to proofs seen in mathematics. 

60 
*} 

61 

19086  62 
theorem 
63 
assumes "prime p" 

64 
shows "sqrt (real p) \<notin> \<rat>" 

13957  65 
proof 
19086  66 
from `prime p` have p: "1 < p" by (simp add: prime_def) 
13957  67 
assume "sqrt (real p) \<in> \<rat>" 
68 
then obtain m n where 

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>" .. 

19086  78 
with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two) 
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>" .. 
19086  83 
with `prime p` have "p dvd n" by (rule prime_dvd_power_two) 
27556  84 
with dvd_m have "p dvd gcd m n" by (rule gcd_greatest) 
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 