(* Title: HOL/Examples/Sqrt.thy Author: Makarius Author: Tobias Nipkow, TU Muenchen *) section ‹Square roots of primes are irrational› theory Sqrt imports Complex_Main "HOL-Computational_Algebra.Primes" begin text ‹ The square root of any prime number (including 2) is irrational. › theorem sqrt_prime_irrational: fixes p :: nat assumes "prime p" shows "sqrt p ∉ ℚ" proof from ‹prime p› have p: "p > 1" by (rule prime_gt_1_nat) assume "sqrt p ∈ ℚ" then obtain m n :: nat where n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n" and "coprime m n" by (rule Rats_abs_nat_div_natE) have eq: "m⇧^{2}= p * n⇧^{2}" proof - from n and sqrt_rat have "m = ¦sqrt p¦ * n" by simp then have "m⇧^{2}= (sqrt p)⇧^{2}* n⇧^{2}" by (simp add: power_mult_distrib) also have "(sqrt p)⇧^{2}= p" by simp also have "… * n⇧^{2}= p * n⇧^{2}" by simp finally show ?thesis by linarith qed have "p dvd m ∧ p dvd n" proof from eq have "p dvd m⇧^{2}" .. with ‹prime p› show "p dvd m" by (rule prime_dvd_power) then obtain k where "m = p * k" .. with eq have "p * n⇧^{2}= p⇧^{2}* k⇧^{2}" by algebra with p have "n⇧^{2}= p * k⇧^{2}" by (simp add: power2_eq_square) then have "p dvd n⇧^{2}" .. with ‹prime p› show "p dvd n" by (rule prime_dvd_power) qed then have "p dvd gcd m n" by simp with ‹coprime m n› have "p = 1" by simp with p show False by simp qed corollary sqrt_2_not_rat: "sqrt 2 ∉ ℚ" using sqrt_prime_irrational [of 2] by simp text ‹ Here is an alternative version of the main proof, using mostly linear forward-reasoning. While this results in less top-down structure, it is probably closer to proofs seen in mathematics. › theorem fixes p :: nat assumes "prime p" shows "sqrt p ∉ ℚ" proof from ‹prime p› have p: "p > 1" by (rule prime_gt_1_nat) assume "sqrt p ∈ ℚ" then obtain m n :: nat where n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n" and "coprime m n" by (rule Rats_abs_nat_div_natE) from n and sqrt_rat have "m = ¦sqrt p¦ * n" by simp then have "m⇧^{2}= (sqrt p)⇧^{2}* n⇧^{2}" by (auto simp add: power2_eq_square) also have "(sqrt p)⇧^{2}= p" by simp also have "… * n⇧^{2}= p * n⇧^{2}" by simp finally have eq: "m⇧^{2}= p * n⇧^{2}" by linarith then have "p dvd m⇧^{2}" .. with ‹prime p› have dvd_m: "p dvd m" by (rule prime_dvd_power) then obtain k where "m = p * k" .. with eq have "p * n⇧^{2}= p⇧^{2}* k⇧^{2}" by algebra with p have "n⇧^{2}= p * k⇧^{2}" by (simp add: power2_eq_square) then have "p dvd n⇧^{2}" .. with ‹prime p› have "p dvd n" by (rule prime_dvd_power) with dvd_m have "p dvd gcd m n" by (rule gcd_greatest) with ‹coprime m n› have "p = 1" by simp with p show False by simp qed text ‹ Another old chestnut, which is a consequence of the irrationality of \<^term>‹sqrt 2›. › lemma "∃a b::real. a ∉ ℚ ∧ b ∉ ℚ ∧ a powr b ∈ ℚ" (is "∃a b. ?P a b") proof (cases "sqrt 2 powr sqrt 2 ∈ ℚ") case True with sqrt_2_not_rat have "?P (sqrt 2) (sqrt 2)" by simp then show ?thesis by blast next case False with sqrt_2_not_rat powr_powr have "?P (sqrt 2 powr sqrt 2) (sqrt 2)" by simp then show ?thesis by blast qed end