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

src/HOL/ex/Sqrt.thy

changeset 28952 | 15a4b2cf8c34 |

parent 28001 | 4642317e0deb |

child 30411 | 9c9b6511ad1b |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/ex/Sqrt.thy Wed Dec 03 15:58:44 2008 +0100 1.3 @@ -0,0 +1,98 @@ 1.4 +(* Title: HOL/ex/Sqrt.thy 1.5 + Author: Markus Wenzel, TU Muenchen 1.6 + 1.7 +*) 1.8 + 1.9 +header {* Square roots of primes are irrational *} 1.10 + 1.11 +theory Sqrt 1.12 +imports Complex_Main Primes 1.13 +begin 1.14 + 1.15 +text {* The definition and the key representation theorem for the set of 1.16 +rational numbers has been moved to a core theory. *} 1.17 + 1.18 +declare Rats_abs_nat_div_natE[elim?] 1.19 + 1.20 +subsection {* Main theorem *} 1.21 + 1.22 +text {* 1.23 + The square root of any prime number (including @{text 2}) is 1.24 + irrational. 1.25 +*} 1.26 + 1.27 +theorem sqrt_prime_irrational: 1.28 + assumes "prime p" 1.29 + shows "sqrt (real p) \<notin> \<rat>" 1.30 +proof 1.31 + from `prime p` have p: "1 < p" by (simp add: prime_def) 1.32 + assume "sqrt (real p) \<in> \<rat>" 1.33 + then obtain m n where 1.34 + n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" 1.35 + and gcd: "gcd m n = 1" .. 1.36 + have eq: "m\<twosuperior> = p * n\<twosuperior>" 1.37 + proof - 1.38 + from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp 1.39 + then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" 1.40 + by (auto simp add: power2_eq_square) 1.41 + also have "(sqrt (real p))\<twosuperior> = real p" by simp 1.42 + also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp 1.43 + finally show ?thesis .. 1.44 + qed 1.45 + have "p dvd m \<and> p dvd n" 1.46 + proof 1.47 + from eq have "p dvd m\<twosuperior>" .. 1.48 + with `prime p` show "p dvd m" by (rule prime_dvd_power_two) 1.49 + then obtain k where "m = p * k" .. 1.50 + with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac) 1.51 + with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) 1.52 + then have "p dvd n\<twosuperior>" .. 1.53 + with `prime p` show "p dvd n" by (rule prime_dvd_power_two) 1.54 + qed 1.55 + then have "p dvd gcd m n" .. 1.56 + with gcd have "p dvd 1" by simp 1.57 + then have "p \<le> 1" by (simp add: dvd_imp_le) 1.58 + with p show False by simp 1.59 +qed 1.60 + 1.61 +corollary "sqrt (real (2::nat)) \<notin> \<rat>" 1.62 + by (rule sqrt_prime_irrational) (rule two_is_prime) 1.63 + 1.64 + 1.65 +subsection {* Variations *} 1.66 + 1.67 +text {* 1.68 + Here is an alternative version of the main proof, using mostly 1.69 + linear forward-reasoning. While this results in less top-down 1.70 + structure, it is probably closer to proofs seen in mathematics. 1.71 +*} 1.72 + 1.73 +theorem 1.74 + assumes "prime p" 1.75 + shows "sqrt (real p) \<notin> \<rat>" 1.76 +proof 1.77 + from `prime p` have p: "1 < p" by (simp add: prime_def) 1.78 + assume "sqrt (real p) \<in> \<rat>" 1.79 + then obtain m n where 1.80 + n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n" 1.81 + and gcd: "gcd m n = 1" .. 1.82 + from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp 1.83 + then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)" 1.84 + by (auto simp add: power2_eq_square) 1.85 + also have "(sqrt (real p))\<twosuperior> = real p" by simp 1.86 + also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp 1.87 + finally have eq: "m\<twosuperior> = p * n\<twosuperior>" .. 1.88 + then have "p dvd m\<twosuperior>" .. 1.89 + with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two) 1.90 + then obtain k where "m = p * k" .. 1.91 + with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac) 1.92 + with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square) 1.93 + then have "p dvd n\<twosuperior>" .. 1.94 + with `prime p` have "p dvd n" by (rule prime_dvd_power_two) 1.95 + with dvd_m have "p dvd gcd m n" by (rule gcd_greatest) 1.96 + with gcd have "p dvd 1" by simp 1.97 + then have "p \<le> 1" by (simp add: dvd_imp_le) 1.98 + with p show False by simp 1.99 +qed 1.100 + 1.101 +end