summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/Sqrt.thy

author | nipkow |

Mon Dec 19 17:10:45 2011 +0100 (2011-12-19) | |

changeset 45917 | 1ce1bc9ff64a |

parent 32479 | 521cc9bf2958 |

child 46495 | 8e8a339e176f |

permissions | -rw-r--r-- |

added old chestnut

1 (* Title: HOL/ex/Sqrt.thy

2 Author: Markus Wenzel, Tobias Nipkow, TU Muenchen

3 *)

5 header {* Square roots of primes are irrational *}

7 theory Sqrt

8 imports Complex_Main "~~/src/HOL/Number_Theory/Primes"

9 begin

11 text {*

12 The square root of any prime number (including @{text 2}) is

13 irrational.

14 *}

16 theorem sqrt_prime_irrational:

17 assumes "prime (p::nat)"

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

19 proof

20 from `prime p` have p: "1 < p" by (simp add: prime_nat_def)

21 assume "sqrt (real p) \<in> \<rat>"

22 then obtain m n :: nat where

23 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"

24 and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)

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

29 by (auto simp add: power2_eq_square)

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

37 with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat)

38 then obtain k where "m = p * k" ..

39 with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)

40 with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)

41 then have "p dvd n\<twosuperior>" ..

42 with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat)

43 qed

44 then have "p dvd gcd m n" ..

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

50 corollary sqrt_real_2_not_rat: "sqrt (real (2::nat)) \<notin> \<rat>"

51 by (rule sqrt_prime_irrational) (rule two_is_prime_nat)

54 subsection {* Variations *}

56 text {*

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

58 linear forward-reasoning. While this results in less top-down

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

60 *}

62 theorem

63 assumes "prime (p::nat)"

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

65 proof

66 from `prime p` have p: "1 < p" by (simp add: prime_nat_def)

67 assume "sqrt (real p) \<in> \<rat>"

68 then obtain m n :: nat where

69 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"

70 and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)

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

73 by (auto simp add: power2_eq_square)

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

78 with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)

79 then obtain k where "m = p * k" ..

80 with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)

81 with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)

82 then have "p dvd n\<twosuperior>" ..

83 with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat)

84 with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)

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

91 text{* Another old chestnut, which is a consequence of the irrationality of 2. *}

93 lemma "\<exists>a b::real. a \<notin> \<rat> \<and> b \<notin> \<rat> \<and> a powr b \<in> \<rat>" (is "EX a b. ?P a b")

94 proof cases

95 assume "sqrt 2 powr sqrt 2 \<in> \<rat>"

96 hence "?P (sqrt 2) (sqrt 2)" by(metis sqrt_real_2_not_rat[simplified])

97 thus ?thesis by blast

98 next

99 assume 1: "sqrt 2 powr sqrt 2 \<notin> \<rat>"

100 have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2"

101 using powr_realpow[of _ 2]

102 by (simp add: powr_powr power2_eq_square[symmetric])

103 hence "?P (sqrt 2 powr sqrt 2) (sqrt 2)"

104 by (metis 1 Rats_number_of sqrt_real_2_not_rat[simplified])

105 thus ?thesis by blast

106 qed

108 end