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;
 haftmann@28952 ` 1` ```(* Title: HOL/ex/Sqrt.thy ``` nipkow@45917 ` 2` ``` Author: Markus Wenzel, Tobias Nipkow, 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` wenzelm@46495 ` 11` ```text {* The square root of any prime number (including 2) is irrational. *} ``` paulson@13957 ` 12` wenzelm@19086 ` 13` ```theorem sqrt_prime_irrational: ``` huffman@31712 ` 14` ``` assumes "prime (p::nat)" ``` hoelzl@51708 ` 15` ``` shows "sqrt p \ \" ``` paulson@13957 ` 16` ```proof ``` huffman@31712 ` 17` ``` from `prime p` have p: "1 < p" by (simp add: prime_nat_def) ``` hoelzl@51708 ` 18` ``` assume "sqrt p \ \" ``` huffman@31712 ` 19` ``` then obtain m n :: nat where ``` hoelzl@51708 ` 20` ``` n: "n \ 0" and sqrt_rat: "\sqrt p\ = m / n" ``` wenzelm@30411 ` 21` ``` and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) ``` wenzelm@53015 ` 22` ``` have eq: "m\<^sup>2 = p * n\<^sup>2" ``` paulson@13957 ` 23` ``` proof - ``` hoelzl@51708 ` 24` ``` from n and sqrt_rat have "m = \sqrt p\ * n" by simp ``` wenzelm@53015 ` 25` ``` then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" ``` paulson@14353 ` 26` ``` by (auto simp add: power2_eq_square) ``` wenzelm@53015 ` 27` ``` also have "(sqrt p)\<^sup>2 = p" by simp ``` wenzelm@53015 ` 28` ``` also have "\ * n\<^sup>2 = p * n\<^sup>2" by simp ``` paulson@13957 ` 29` ``` finally show ?thesis .. ``` paulson@13957 ` 30` ``` qed ``` paulson@13957 ` 31` ``` have "p dvd m \ p dvd n" ``` paulson@13957 ` 32` ``` proof ``` wenzelm@53015 ` 33` ``` from eq have "p dvd m\<^sup>2" .. ``` nipkow@31952 ` 34` ``` with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 35` ``` then obtain k where "m = p * k" .. ``` wenzelm@53015 ` 36` ``` with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac) ``` wenzelm@53015 ` 37` ``` with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) ``` wenzelm@53015 ` 38` ``` then have "p dvd n\<^sup>2" .. ``` nipkow@31952 ` 39` ``` with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 40` ``` qed ``` haftmann@27556 ` 41` ``` then have "p dvd gcd m n" .. ``` paulson@13957 ` 42` ``` with gcd have "p dvd 1" by simp ``` paulson@13957 ` 43` ``` then have "p \ 1" by (simp add: dvd_imp_le) ``` paulson@13957 ` 44` ``` with p show False by simp ``` paulson@13957 ` 45` ```qed ``` paulson@13957 ` 46` hoelzl@51708 ` 47` ```corollary sqrt_2_not_rat: "sqrt 2 \ \" ``` hoelzl@51708 ` 48` ``` using sqrt_prime_irrational[of 2] by simp ``` paulson@13957 ` 49` paulson@13957 ` 50` ```subsection {* Variations *} ``` paulson@13957 ` 51` paulson@13957 ` 52` ```text {* ``` paulson@13957 ` 53` ``` Here is an alternative version of the main proof, using mostly ``` paulson@13957 ` 54` ``` linear forward-reasoning. While this results in less top-down ``` paulson@13957 ` 55` ``` structure, it is probably closer to proofs seen in mathematics. ``` paulson@13957 ` 56` ```*} ``` paulson@13957 ` 57` wenzelm@19086 ` 58` ```theorem ``` huffman@31712 ` 59` ``` assumes "prime (p::nat)" ``` hoelzl@51708 ` 60` ``` shows "sqrt p \ \" ``` paulson@13957 ` 61` ```proof ``` huffman@31712 ` 62` ``` from `prime p` have p: "1 < p" by (simp add: prime_nat_def) ``` hoelzl@51708 ` 63` ``` assume "sqrt p \ \" ``` huffman@31712 ` 64` ``` then obtain m n :: nat where ``` hoelzl@51708 ` 65` ``` n: "n \ 0" and sqrt_rat: "\sqrt p\ = m / n" ``` wenzelm@30411 ` 66` ``` and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE) ``` hoelzl@51708 ` 67` ``` from n and sqrt_rat have "m = \sqrt p\ * n" by simp ``` wenzelm@53015 ` 68` ``` then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2" ``` paulson@14353 ` 69` ``` by (auto simp add: power2_eq_square) ``` wenzelm@53015 ` 70` ``` also have "(sqrt p)\<^sup>2 = p" by simp ``` wenzelm@53015 ` 71` ``` also have "\ * n\<^sup>2 = p * n\<^sup>2" by simp ``` wenzelm@53015 ` 72` ``` finally have eq: "m\<^sup>2 = p * n\<^sup>2" .. ``` wenzelm@53015 ` 73` ``` then have "p dvd m\<^sup>2" .. ``` nipkow@31952 ` 74` ``` with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 75` ``` then obtain k where "m = p * k" .. ``` wenzelm@53015 ` 76` ``` with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac) ``` wenzelm@53015 ` 77` ``` with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square) ``` wenzelm@53015 ` 78` ``` then have "p dvd n\<^sup>2" .. ``` nipkow@31952 ` 79` ``` with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat) ``` nipkow@31952 ` 80` ``` with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat) ``` paulson@13957 ` 81` ``` with gcd have "p dvd 1" by simp ``` paulson@13957 ` 82` ``` then have "p \ 1" by (simp add: dvd_imp_le) ``` paulson@13957 ` 83` ``` with p show False by simp ``` paulson@13957 ` 84` ```qed ``` paulson@13957 ` 85` nipkow@45917 ` 86` wenzelm@46495 ` 87` ```text {* Another old chestnut, which is a consequence of the irrationality of 2. *} ``` nipkow@45917 ` 88` nipkow@45917 ` 89` ```lemma "\a b::real. a \ \ \ b \ \ \ a powr b \ \" (is "EX a b. ?P a b") ``` nipkow@45917 ` 90` ```proof cases ``` nipkow@45917 ` 91` ``` assume "sqrt 2 powr sqrt 2 \ \" ``` wenzelm@46495 ` 92` ``` then have "?P (sqrt 2) (sqrt 2)" ``` hoelzl@51708 ` 93` ``` by (metis sqrt_2_not_rat) ``` wenzelm@46495 ` 94` ``` then show ?thesis by blast ``` nipkow@45917 ` 95` ```next ``` nipkow@45917 ` 96` ``` assume 1: "sqrt 2 powr sqrt 2 \ \" ``` nipkow@45917 ` 97` ``` have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" ``` wenzelm@46495 ` 98` ``` using powr_realpow [of _ 2] ``` wenzelm@46495 ` 99` ``` by (simp add: powr_powr power2_eq_square [symmetric]) ``` wenzelm@46495 ` 100` ``` then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" ``` hoelzl@51708 ` 101` ``` by (metis 1 Rats_number_of sqrt_2_not_rat) ``` wenzelm@46495 ` 102` ``` then show ?thesis by blast ``` nipkow@45917 ` 103` ```qed ``` nipkow@45917 ` 104` paulson@13957 ` 105` ```end ``` hoelzl@51708 ` 106`