(*  Title:      HOL/Hyperreal/ex/Sqrt.thy

     ID:         $Id$

     Author:     Markus Wenzel, TU Muenchen

 *)

 header {*  Square roots of primes are irrational *}

 theory Sqrt

 imports Primes Complex_Main

 begin

 text {* The definition and the key representation theorem for the set of

 rational numbers has been moved to a core theory.  *}

 declare Rats_abs_nat_div_natE[elim?]

 subsection {* Main theorem *}

 text {*

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

   irrational.

 *}

 theorem sqrt_prime_irrational:

   assumes "prime p"

   shows "sqrt (real p) \<notin> \<rat>"

 proof

   from `prime p` have p: "1 < p" by (simp add: prime_def)

   assume "sqrt (real p) \<in> \<rat>"

   then obtain m n where

       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"

     and gcd: "gcd m n = 1" ..

   have eq: "m\<twosuperior> = p * n\<twosuperior>"

   proof -

     from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp

     then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"

       by (auto simp add: power2_eq_square)

     also have "(sqrt (real p))\<twosuperior> = real p" by simp

     also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp

     finally show ?thesis ..

   qed

   have "p dvd m \<and> p dvd n"

   proof

     from eq have "p dvd m\<twosuperior>" ..

     with `prime p` show "p dvd m" by (rule prime_dvd_power_two)

     then obtain k where "m = p * k" ..

     with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)

     with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)

     then have "p dvd n\<twosuperior>" ..

     with `prime p` 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 \<le> 1" by (simp add: dvd_imp_le)

   with p show False by simp

 qed

 corollary "sqrt (real (2::nat)) \<notin> \<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

   assumes "prime p"

   shows "sqrt (real p) \<notin> \<rat>"

 proof

   from `prime p` have p: "1 < p" by (simp add: prime_def)

   assume "sqrt (real p) \<in> \<rat>"

   then obtain m n where

       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"

     and gcd: "gcd m n = 1" ..

   from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp

   then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"

     by (auto simp add: power2_eq_square)

   also have "(sqrt (real p))\<twosuperior> = real p" by simp

   also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp

   finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..

   then have "p dvd m\<twosuperior>" ..

   with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two)

   then obtain k where "m = p * k" ..

   with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)

   with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)

   then have "p dvd n\<twosuperior>" ..

   with `prime p` 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 \<le> 1" by (simp add: dvd_imp_le)

   with p show False by simp

 qed

 end