src/HOL/ex/Sqrt.thy
 author haftmann Tue Sep 01 15:39:33 2009 +0200 (2009-09-01) changeset 32479 521cc9bf2958 parent 31952 40501bb2d57c child 45917 1ce1bc9ff64a permissions -rw-r--r--
some reorganization of number theory
 haftmann@28952 ` 1` ```(* Title: HOL/ex/Sqrt.thy ``` paulson@13957 ` 2` ``` Author: Markus Wenzel, TU Muenchen ``` paulson@13957 ` 3` ```*) ``` paulson@13957 ` 4` paulson@13957 ` 5` ```header {* Square roots of primes are irrational *} ``` paulson@13957 ` 6` nipkow@15149 ` 7` ```theory Sqrt ``` haftmann@32479 ` 8` ```imports Complex_Main "~~/src/HOL/Number_Theory/Primes" ``` nipkow@15149 ` 9` ```begin ``` paulson@13957 ` 10` paulson@13957 ` 11` ```text {* ``` paulson@13957 ` 12` ``` The square root of any prime number (including @{text 2}) is ``` paulson@13957 ` 13` ``` irrational. ``` paulson@13957 ` 14` ```*} ``` paulson@13957 ` 15` wenzelm@19086 ` 16` ```theorem sqrt_prime_irrational: ``` huffman@31712 ` 17` ``` assumes "prime (p::nat)" ``` wenzelm@19086 ` 18` ``` shows "sqrt (real p) \ \" ``` paulson@13957 ` 19` ```proof ``` huffman@31712 ` 20` ``` from `prime p` have p: "1 < p" by (simp add: prime_nat_def) ``` paulson@13957 ` 21` ``` assume "sqrt (real p) \ \" ``` huffman@31712 ` 22` ``` then obtain m n :: nat where ``` paulson@13957 ` 23` ``` n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" ``` wenzelm@30411 ` 24` ``` and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) ``` paulson@13957 ` 25` ``` have eq: "m\ = p * n\" ``` paulson@13957 ` 26` ``` proof - ``` paulson@13957 ` 27` ``` from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp ``` paulson@13957 ` 28` ``` then have "real (m\) = (sqrt (real p))\ * real (n\)" ``` paulson@14353 ` 29` ``` by (auto simp add: power2_eq_square) ``` paulson@13957 ` 30` ``` also have "(sqrt (real p))\ = real p" by simp ``` paulson@13957 ` 31` ``` also have "\ * real (n\) = real (p * n\)" by simp ``` paulson@13957 ` 32` ``` finally show ?thesis .. ``` paulson@13957 ` 33` ``` qed ``` paulson@13957 ` 34` ``` have "p dvd m \ p dvd n" ``` paulson@13957 ` 35` ``` proof ``` paulson@13957 ` 36` ``` from eq have "p dvd m\" .. ``` nipkow@31952 ` 37` ``` with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 38` ``` then obtain k where "m = p * k" .. ``` paulson@14353 ` 39` ``` with eq have "p * n\ = p\ * k\" by (auto simp add: power2_eq_square mult_ac) ``` paulson@14353 ` 40` ``` with p have "n\ = p * k\" by (simp add: power2_eq_square) ``` paulson@13957 ` 41` ``` then have "p dvd n\" .. ``` nipkow@31952 ` 42` ``` with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 43` ``` qed ``` haftmann@27556 ` 44` ``` then have "p dvd gcd m n" .. ``` paulson@13957 ` 45` ``` with gcd have "p dvd 1" by simp ``` paulson@13957 ` 46` ``` then have "p \ 1" by (simp add: dvd_imp_le) ``` paulson@13957 ` 47` ``` with p show False by simp ``` paulson@13957 ` 48` ```qed ``` paulson@13957 ` 49` paulson@13957 ` 50` ```corollary "sqrt (real (2::nat)) \ \" ``` nipkow@31952 ` 51` ``` by (rule sqrt_prime_irrational) (rule two_is_prime_nat) ``` paulson@13957 ` 52` paulson@13957 ` 53` paulson@13957 ` 54` ```subsection {* Variations *} ``` paulson@13957 ` 55` paulson@13957 ` 56` ```text {* ``` paulson@13957 ` 57` ``` Here is an alternative version of the main proof, using mostly ``` paulson@13957 ` 58` ``` linear forward-reasoning. While this results in less top-down ``` paulson@13957 ` 59` ``` structure, it is probably closer to proofs seen in mathematics. ``` paulson@13957 ` 60` ```*} ``` paulson@13957 ` 61` wenzelm@19086 ` 62` ```theorem ``` huffman@31712 ` 63` ``` assumes "prime (p::nat)" ``` wenzelm@19086 ` 64` ``` shows "sqrt (real p) \ \" ``` paulson@13957 ` 65` ```proof ``` huffman@31712 ` 66` ``` from `prime p` have p: "1 < p" by (simp add: prime_nat_def) ``` paulson@13957 ` 67` ``` assume "sqrt (real p) \ \" ``` huffman@31712 ` 68` ``` then obtain m n :: nat where ``` paulson@13957 ` 69` ``` n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" ``` wenzelm@30411 ` 70` ``` and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) ``` paulson@13957 ` 71` ``` from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp ``` paulson@13957 ` 72` ``` then have "real (m\) = (sqrt (real p))\ * real (n\)" ``` paulson@14353 ` 73` ``` by (auto simp add: power2_eq_square) ``` paulson@13957 ` 74` ``` also have "(sqrt (real p))\ = real p" by simp ``` paulson@13957 ` 75` ``` also have "\ * real (n\) = real (p * n\)" by simp ``` paulson@13957 ` 76` ``` finally have eq: "m\ = p * n\" .. ``` paulson@13957 ` 77` ``` then have "p dvd m\" .. ``` nipkow@31952 ` 78` ``` with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 79` ``` then obtain k where "m = p * k" .. ``` paulson@14353 ` 80` ``` with eq have "p * n\ = p\ * k\" by (auto simp add: power2_eq_square mult_ac) ``` paulson@14353 ` 81` ``` with p have "n\ = p * k\" by (simp add: power2_eq_square) ``` paulson@13957 ` 82` ``` then have "p dvd n\" .. ``` nipkow@31952 ` 83` ``` with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat) ``` nipkow@31952 ` 84` ``` with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat) ``` paulson@13957 ` 85` ``` with gcd have "p dvd 1" by simp ``` paulson@13957 ` 86` ``` then have "p \ 1" by (simp add: dvd_imp_le) ``` paulson@13957 ` 87` ``` with p show False by simp ``` paulson@13957 ` 88` ```qed ``` paulson@13957 ` 89` paulson@13957 ` 90` ```end ```