# Theory Sqrt

Up to index of Isabelle/HOL/HOL-Complex/ex

theory Sqrt
imports Primes Complex_Main
begin

    (*  Title:      HOL/Hyperreal/ex/Sqrt.thy
        ID:         $Id: Sqrt.thy,v 1.7 2005/07/01 15:41:15 nipkow Exp $
        Author:     Markus Wenzel, TU Muenchen

    *)

    header {*  Square roots of primes are irrational *}

    theory Sqrt
    imports Primes Complex_Main
    begin

    subsection {* Preliminaries *}

    text {*
      The set of rational numbers, including the key representation
      theorem.
    *}

    constdefs
      rationals :: "real set"    ("\<rat>")
      "\<rat> ≡ {x. ∃m n. n ≠ 0 ∧ ¦x¦ = real (m::nat) / real (n::nat)}"

    theorem rationals_rep: "x ∈ \<rat> ==>
      ∃m n. n ≠ 0 ∧ ¦x¦ = real m / real n ∧ gcd (m, n) = 1"
    proof -
      assume "x ∈ \<rat>"
      then obtain m n :: nat where
          n: "n ≠ 0" and x_rat: "¦x¦ = real m / real n"
        by (unfold rationals_def) blast
      let ?gcd = "gcd (m, n)"
      from n have gcd: "?gcd ≠ 0" by (simp add: gcd_zero)
      let ?k = "m div ?gcd"
      let ?l = "n div ?gcd"
      let ?gcd' = "gcd (?k, ?l)"
      have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
        by (rule dvd_mult_div_cancel)
      have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
        by (rule dvd_mult_div_cancel)

      from n and gcd_l have "?l ≠ 0"
        by (auto iff del: neq0_conv)
      moreover
      have "¦x¦ = real ?k / real ?l"
      proof -
        from gcd have "real ?k / real ?l =
            real (?gcd * ?k) / real (?gcd * ?l)"
          by (simp add: mult_divide_cancel_left)
        also from gcd_k and gcd_l have "… = real m / real n" by simp
        also from x_rat have "… = ¦x¦" ..
        finally show ?thesis ..
      qed
      moreover
      have "?gcd' = 1"
      proof -
        have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)"
          by (rule gcd_mult_distrib2)
        with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
        with gcd show ?thesis by simp
      qed
      ultimately show ?thesis by blast
    qed

    lemma [elim?]: "r ∈ \<rat> ==>
      (!!m n. n ≠ 0 ==> ¦r¦ = real m / real n ==> gcd (m, n) = 1 ==> C)
        ==> C"
      using rationals_rep by blast

    subsection {* Main theorem *}

    text {*
      The square root of any prime number (including @{text 2}) is
      irrational.
    *}

    theorem sqrt_prime_irrational: "prime p ==> sqrt (real p) ∉ \<rat>"
    proof
      assume p_prime: "prime p"
      then have p: "1 < p" by (simp add: prime_def)
      assume "sqrt (real p) ∈ \<rat>"
      then obtain m n where
          n: "n ≠ 0" and sqrt_rat: "¦sqrt (real p)¦ = real m / real n"
        and gcd: "gcd (m, n) = 1" ..
      have eq: "m² = p * n²"
      proof -
        from n and sqrt_rat have "real m = ¦sqrt (real p)¦ * real n" by simp
        then have "real (m²) = (sqrt (real p))² * real (n²)"
          by (auto simp add: power2_eq_square)
        also have "(sqrt (real p))² = real p" by simp
        also have "… * real (n²) = real (p * n²)" by simp
        finally show ?thesis ..
      qed
      have "p dvd m ∧ p dvd n"
      proof
        from eq have "p dvd m²" ..
        with p_prime show "p dvd m" by (rule prime_dvd_power_two)
        then obtain k where "m = p * k" ..
        with eq have "p * n² = p² * k²" by (auto simp add: power2_eq_square mult_ac)
        with p have "n² = p * k²" by (simp add: power2_eq_square)
        then have "p dvd n²" ..
        with p_prime show "p dvd n" by (rule prime_dvd_power_two)
      qed
      then have "p dvd gcd (m, n)" ..
      with gcd have "p dvd 1" by simp
      then have "p ≤ 1" by (simp add: dvd_imp_le)
      with p show False by simp
    qed

    corollary "sqrt (real (2::nat)) ∉ \<rat>"
      by (rule sqrt_prime_irrational) (rule two_is_prime)

    subsection {* Variations *}

    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 "prime p ==> sqrt (real p) ∉ \<rat>"
    proof
      assume p_prime: "prime p"
      then have p: "1 < p" by (simp add: prime_def)
      assume "sqrt (real p) ∈ \<rat>"
      then obtain m n where
          n: "n ≠ 0" and sqrt_rat: "¦sqrt (real p)¦ = real m / real n"
        and gcd: "gcd (m, n) = 1" ..
      from n and sqrt_rat have "real m = ¦sqrt (real p)¦ * real n" by simp
      then have "real (m²) = (sqrt (real p))² * real (n²)"
        by (auto simp add: power2_eq_square)
      also have "(sqrt (real p))² = real p" by simp
      also have "… * real (n²) = real (p * n²)" by simp
      finally have eq: "m² = p * n²" ..
      then have "p dvd m²" ..
      with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
      then obtain k where "m = p * k" ..
      with eq have "p * n² = p² * k²" by (auto simp add: power2_eq_square mult_ac)
      with p have "n² = p * k²" by (simp add: power2_eq_square)
      then have "p dvd n²" ..
      with p_prime have "p dvd n" by (rule prime_dvd_power_two)
      with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
      with gcd have "p dvd 1" by simp
      then have "p ≤ 1" by (simp add: dvd_imp_le)
      with p show False by simp
    qed

    end

### Preliminaries

theorem rationals_rep:

      x ∈ \<rat> ==> ∃m n. n ≠ 0 ∧ ¦x¦ = real m / real n ∧ gcd (m, n) = 1

lemma

      [| r ∈ \<rat>;
         !!m n. [| n ≠ 0; ¦r¦ = real m / real n; gcd (m, n) = 1 |] ==> C |]
      ==> C

### Main theorem

theorem sqrt_prime_irrational:

      prime p ==> sqrt (real p) ∉ \<rat>

corollary

      sqrt (real 2) ∉ \<rat>

### Variations

theorem

      prime p ==> sqrt (real p) ∉ \<rat>