src/HOL/ex/Sqrt.thy
 author haftmann Wed Feb 17 21:51:57 2016 +0100 (2016-02-17) changeset 62348 9a5f43dac883 parent 61762 d50b993b4fb9 child 63534 523b488b15c9 permissions -rw-r--r--
dropped various legacy fact bindings
 haftmann@28952 ` 1` ```(* Title: HOL/ex/Sqrt.thy ``` nipkow@45917 ` 2` ``` Author: Markus Wenzel, Tobias Nipkow, TU Muenchen ``` paulson@13957 ` 3` ```*) ``` paulson@13957 ` 4` wenzelm@59031 ` 5` ```section \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@59031 ` 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 ``` lp15@61762 ` 17` ``` from \prime p\ have p: "1 < p" by (simp add: prime_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" ``` haftmann@60690 ` 21` ``` and "coprime m n" 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 ``` lp15@61649 ` 29` ``` finally show ?thesis using of_nat_eq_iff by blast ``` 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" .. ``` wenzelm@59031 ` 34` ``` with \prime p\ show "p dvd m" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 35` ``` then obtain k where "m = p * k" .. ``` haftmann@57514 ` 36` ``` with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps) ``` 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" .. ``` wenzelm@59031 ` 39` ``` with \prime p\ show "p dvd n" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 40` ``` qed ``` haftmann@60690 ` 41` ``` then have "p dvd gcd m n" by simp ``` haftmann@60690 ` 42` ``` with \coprime m n\ have "p = 1" by simp ``` paulson@13957 ` 43` ``` with p show False by simp ``` paulson@13957 ` 44` ```qed ``` paulson@13957 ` 45` hoelzl@51708 ` 46` ```corollary sqrt_2_not_rat: "sqrt 2 \ \" ``` hoelzl@51708 ` 47` ``` using sqrt_prime_irrational[of 2] by simp ``` paulson@13957 ` 48` paulson@13957 ` 49` wenzelm@59031 ` 50` ```subsection \Variations\ ``` wenzelm@59031 ` 51` wenzelm@59031 ` 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. ``` wenzelm@59031 ` 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 ``` lp15@61762 ` 62` ``` from \prime p\ have p: "1 < p" by (simp add: prime_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" ``` haftmann@60690 ` 66` ``` and "coprime m n" 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 ``` lp15@61649 ` 72` ``` finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast ``` wenzelm@53015 ` 73` ``` then have "p dvd m\<^sup>2" .. ``` wenzelm@59031 ` 74` ``` with \prime p\ have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) ``` paulson@13957 ` 75` ``` then obtain k where "m = p * k" .. ``` haftmann@57514 ` 76` ``` with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps) ``` 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" .. ``` wenzelm@59031 ` 79` ``` with \prime p\ have "p dvd n" by (rule prime_dvd_power_nat) ``` haftmann@62348 ` 80` ``` with dvd_m have "p dvd gcd m n" by (rule gcd_greatest) ``` haftmann@60690 ` 81` ``` with \coprime m n\ have "p = 1" by simp ``` paulson@13957 ` 82` ``` with p show False by simp ``` paulson@13957 ` 83` ```qed ``` paulson@13957 ` 84` nipkow@45917 ` 85` wenzelm@59031 ` 86` ```text \Another old chestnut, which is a consequence of the irrationality of 2.\ ``` nipkow@45917 ` 87` wenzelm@59031 ` 88` ```lemma "\a b::real. a \ \ \ b \ \ \ a powr b \ \" (is "\a b. ?P a b") ``` nipkow@45917 ` 89` ```proof cases ``` nipkow@45917 ` 90` ``` assume "sqrt 2 powr sqrt 2 \ \" ``` wenzelm@46495 ` 91` ``` then have "?P (sqrt 2) (sqrt 2)" ``` hoelzl@51708 ` 92` ``` by (metis sqrt_2_not_rat) ``` wenzelm@46495 ` 93` ``` then show ?thesis by blast ``` nipkow@45917 ` 94` ```next ``` nipkow@45917 ` 95` ``` assume 1: "sqrt 2 powr sqrt 2 \ \" ``` nipkow@45917 ` 96` ``` have "(sqrt 2 powr sqrt 2) powr sqrt 2 = 2" ``` wenzelm@46495 ` 97` ``` using powr_realpow [of _ 2] ``` wenzelm@46495 ` 98` ``` by (simp add: powr_powr power2_eq_square [symmetric]) ``` wenzelm@46495 ` 99` ``` then have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" ``` hoelzl@51708 ` 100` ``` by (metis 1 Rats_number_of sqrt_2_not_rat) ``` wenzelm@46495 ` 101` ``` then show ?thesis by blast ``` nipkow@45917 ` 102` ```qed ``` nipkow@45917 ` 103` paulson@13957 ` 104` ```end ```