src/HOL/ex/Sqrt.thy
changeset 30411 9c9b6511ad1b
parent 28952 15a4b2cf8c34
child 31712 6f8aa9aea693
equal deleted inserted replaced
30410:ef670320e281 30411:9c9b6511ad1b
     1 (*  Title:      HOL/ex/Sqrt.thy
     1 (*  Title:      HOL/ex/Sqrt.thy
     2     Author:     Markus Wenzel, TU Muenchen
     2     Author:     Markus Wenzel, TU Muenchen
     3 
       
     4 *)
     3 *)
     5 
     4 
     6 header {*  Square roots of primes are irrational *}
     5 header {*  Square roots of primes are irrational *}
     7 
     6 
     8 theory Sqrt
     7 theory Sqrt
     9 imports Complex_Main Primes
     8 imports Complex_Main Primes
    10 begin
     9 begin
    11 
       
    12 text {* The definition and the key representation theorem for the set of
       
    13 rational numbers has been moved to a core theory.  *}
       
    14 
       
    15 declare Rats_abs_nat_div_natE[elim?]
       
    16 
       
    17 subsection {* Main theorem *}
       
    18 
    10 
    19 text {*
    11 text {*
    20   The square root of any prime number (including @{text 2}) is
    12   The square root of any prime number (including @{text 2}) is
    21   irrational.
    13   irrational.
    22 *}
    14 *}
    27 proof
    19 proof
    28   from `prime p` have p: "1 < p" by (simp add: prime_def)
    20   from `prime p` have p: "1 < p" by (simp add: prime_def)
    29   assume "sqrt (real p) \<in> \<rat>"
    21   assume "sqrt (real p) \<in> \<rat>"
    30   then obtain m n where
    22   then obtain m n where
    31       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    23       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    32     and gcd: "gcd m n = 1" ..
    24     and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
    33   have eq: "m\<twosuperior> = p * n\<twosuperior>"
    25   have eq: "m\<twosuperior> = p * n\<twosuperior>"
    34   proof -
    26   proof -
    35     from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    27     from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    36     then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
    28     then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
    37       by (auto simp add: power2_eq_square)
    29       by (auto simp add: power2_eq_square)
    73 proof
    65 proof
    74   from `prime p` have p: "1 < p" by (simp add: prime_def)
    66   from `prime p` have p: "1 < p" by (simp add: prime_def)
    75   assume "sqrt (real p) \<in> \<rat>"
    67   assume "sqrt (real p) \<in> \<rat>"
    76   then obtain m n where
    68   then obtain m n where
    77       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    69       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    78     and gcd: "gcd m n = 1" ..
    70     and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
    79   from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    71   from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
    80   then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
    72   then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
    81     by (auto simp add: power2_eq_square)
    73     by (auto simp add: power2_eq_square)
    82   also have "(sqrt (real p))\<twosuperior> = real p" by simp
    74   also have "(sqrt (real p))\<twosuperior> = real p" by simp
    83   also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
    75   also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp