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

src/HOL/ex/Sqrt.thy

author | wenzelm |

Tue Aug 13 16:25:47 2013 +0200 (2013-08-13) | |

changeset 53015 | a1119cf551e8 |

parent 51708 | 5188a18c33b1 |

child 53598 | 2bd8d459ebae |

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

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

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 {* The square root of any prime number (including 2) is irrational. *}

13 theorem sqrt_prime_irrational:

14 assumes "prime (p::nat)"

15 shows "sqrt p \<notin> \<rat>"

16 proof

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

18 assume "sqrt p \<in> \<rat>"

19 then obtain m n :: nat where

20 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"

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

22 have eq: "m\<^sup>2 = p * n\<^sup>2"

23 proof -

24 from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp

25 then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"

26 by (auto simp add: power2_eq_square)

27 also have "(sqrt p)\<^sup>2 = p" by simp

28 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp

29 finally show ?thesis ..

30 qed

31 have "p dvd m \<and> p dvd n"

32 proof

33 from eq have "p dvd m\<^sup>2" ..

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

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

36 with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)

37 with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)

38 then have "p dvd n\<^sup>2" ..

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

40 qed

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

42 with gcd have "p dvd 1" by simp

43 then have "p \<le> 1" by (simp add: dvd_imp_le)

44 with p show False by simp

45 qed

47 corollary sqrt_2_not_rat: "sqrt 2 \<notin> \<rat>"

48 using sqrt_prime_irrational[of 2] by simp

50 subsection {* Variations *}

52 text {*

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

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

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

56 *}

58 theorem

59 assumes "prime (p::nat)"

60 shows "sqrt p \<notin> \<rat>"

61 proof

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

63 assume "sqrt p \<in> \<rat>"

64 then obtain m n :: nat where

65 n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"

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

67 from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp

68 then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"

69 by (auto simp add: power2_eq_square)

70 also have "(sqrt p)\<^sup>2 = p" by simp

71 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp

72 finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..

73 then have "p dvd m\<^sup>2" ..

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

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

76 with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)

77 with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)

78 then have "p dvd n\<^sup>2" ..

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

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

81 with gcd have "p dvd 1" by simp

82 then have "p \<le> 1" by (simp add: dvd_imp_le)

83 with p show False by simp

84 qed

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

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

90 proof cases

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

92 then have "?P (sqrt 2) (sqrt 2)"

93 by (metis sqrt_2_not_rat)

94 then show ?thesis by blast

95 next

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

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

98 using powr_realpow [of _ 2]

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

100 then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)"

101 by (metis 1 Rats_number_of sqrt_2_not_rat)

102 then show ?thesis by blast

103 qed

105 end