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

src/HOL/ex/Sqrt.thy

author | nipkow |

Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) | |

changeset 30313 | b2441b0c8d38 |

parent 28952 | 15a4b2cf8c34 |

child 30411 | 9c9b6511ad1b |

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

added lemmas

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

2 Author: Markus Wenzel, TU Muenchen

4 *)

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

8 theory Sqrt

9 imports Complex_Main Primes

10 begin

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

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

15 declare Rats_abs_nat_div_natE[elim?]

17 subsection {* Main theorem *}

19 text {*

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

21 irrational.

22 *}

24 theorem sqrt_prime_irrational:

25 assumes "prime p"

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

27 proof

28 from `prime p` have p: "1 < p" by (simp add: prime_def)

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

30 then obtain m n where

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

32 and gcd: "gcd m n = 1" ..

33 have eq: "m\<twosuperior> = p * n\<twosuperior>"

34 proof -

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

37 by (auto simp add: power2_eq_square)

38 also have "(sqrt (real p))\<twosuperior> = real p" by simp

39 also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp

40 finally show ?thesis ..

41 qed

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

43 proof

44 from eq have "p dvd m\<twosuperior>" ..

45 with `prime p` show "p dvd m" by (rule prime_dvd_power_two)

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

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

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

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

50 with `prime p` show "p dvd n" by (rule prime_dvd_power_two)

51 qed

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

53 with gcd have "p dvd 1" by simp

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

55 with p show False by simp

56 qed

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

59 by (rule sqrt_prime_irrational) (rule two_is_prime)

62 subsection {* Variations *}

64 text {*

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

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

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

68 *}

70 theorem

71 assumes "prime p"

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

73 proof

74 from `prime p` have p: "1 < p" by (simp add: prime_def)

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

76 then obtain m n where

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

78 and gcd: "gcd m n = 1" ..

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

81 by (auto simp add: power2_eq_square)

82 also have "(sqrt (real p))\<twosuperior> = real p" by simp

83 also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp

84 finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..

85 then have "p dvd m\<twosuperior>" ..

86 with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two)

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

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

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

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

91 with `prime p` have "p dvd n" by (rule prime_dvd_power_two)

92 with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)

93 with gcd have "p dvd 1" by simp

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

95 with p show False by simp

96 qed

98 end