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

src/HOL/ex/Sqrt.thy

author | paulson <lp15@cam.ac.uk> |

Fri Nov 13 12:27:13 2015 +0000 (2015-11-13) | |

changeset 61649 | 268d88ec9087 |

parent 60690 | a9e45c9588c3 |

child 61762 | d50b993b4fb9 |

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

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

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

2 Author: Markus Wenzel, Tobias Nipkow, TU Muenchen

3 *)

5 section \<open>Square roots of primes are irrational\<close>

7 theory Sqrt

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

9 begin

11 text \<open>The square root of any prime number (including 2) is irrational.\<close>

13 theorem sqrt_prime_irrational:

14 assumes "prime (p::nat)"

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

16 proof

17 from \<open>prime p\<close> 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 "coprime m n" 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 using of_nat_eq_iff by blast

30 qed

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

32 proof

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

34 with \<open>prime p\<close> 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 ac_simps)

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 \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)

40 qed

41 then have "p dvd gcd m n" by simp

42 with \<open>coprime m n\<close> have "p = 1" by simp

43 with p show False by simp

44 qed

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

47 using sqrt_prime_irrational[of 2] by simp

50 subsection \<open>Variations\<close>

52 text \<open>

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 \<close>

58 theorem

59 assumes "prime (p::nat)"

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

61 proof

62 from \<open>prime p\<close> 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 "coprime m n" 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" using of_nat_eq_iff by blast

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

74 with \<open>prime p\<close> 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 ac_simps)

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 \<open>prime p\<close> 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 \<open>coprime m n\<close> have "p = 1" by simp

82 with p show False by simp

83 qed

86 text \<open>Another old chestnut, which is a consequence of the irrationality of 2.\<close>

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

89 proof cases

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

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

92 by (metis sqrt_2_not_rat)

93 then show ?thesis by blast

94 next

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

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

97 using powr_realpow [of _ 2]

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

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

100 by (metis 1 Rats_number_of sqrt_2_not_rat)

101 then show ?thesis by blast

102 qed

104 end