src/HOL/ex/Sqrt.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28952 15a4b2cf8c34
child 30411 9c9b6511ad1b
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Sqrt.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 *)
     5 
     6 header {*  Square roots of primes are irrational *}
     7 
     8 theory Sqrt
     9 imports Complex_Main Primes
    10 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 
    19 text {*
    20   The square root of any prime number (including @{text 2}) is
    21   irrational.
    22 *}
    23 
    24 theorem sqrt_prime_irrational:
    25   assumes "prime p"
    26   shows "sqrt (real p) \<notin> \<rat>"
    27 proof
    28   from `prime p` have p: "1 < p" by (simp add: prime_def)
    29   assume "sqrt (real p) \<in> \<rat>"
    30   then obtain m n where
    31       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    32     and gcd: "gcd m n = 1" ..
    33   have eq: "m\<twosuperior> = p * n\<twosuperior>"
    34   proof -
    35     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>)"
    37       by (auto simp add: power2_eq_square)
    38     also have "(sqrt (real p))\<twosuperior> = real p" by simp
    39     also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
    40     finally show ?thesis ..
    41   qed
    42   have "p dvd m \<and> p dvd n"
    43   proof
    44     from eq have "p dvd m\<twosuperior>" ..
    45     with `prime p` show "p dvd m" by (rule prime_dvd_power_two)
    46     then obtain k where "m = p * k" ..
    47     with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
    48     with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
    49     then have "p dvd n\<twosuperior>" ..
    50     with `prime p` show "p dvd n" by (rule prime_dvd_power_two)
    51   qed
    52   then have "p dvd gcd m n" ..
    53   with gcd have "p dvd 1" by simp
    54   then have "p \<le> 1" by (simp add: dvd_imp_le)
    55   with p show False by simp
    56 qed
    57 
    58 corollary "sqrt (real (2::nat)) \<notin> \<rat>"
    59   by (rule sqrt_prime_irrational) (rule two_is_prime)
    60 
    61 
    62 subsection {* Variations *}
    63 
    64 text {*
    65   Here is an alternative version of the main proof, using mostly
    66   linear forward-reasoning.  While this results in less top-down
    67   structure, it is probably closer to proofs seen in mathematics.
    68 *}
    69 
    70 theorem
    71   assumes "prime p"
    72   shows "sqrt (real p) \<notin> \<rat>"
    73 proof
    74   from `prime p` have p: "1 < p" by (simp add: prime_def)
    75   assume "sqrt (real p) \<in> \<rat>"
    76   then obtain m n where
    77       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
    78     and gcd: "gcd m n = 1" ..
    79   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>)"
    81     by (auto simp add: power2_eq_square)
    82   also have "(sqrt (real p))\<twosuperior> = real p" by simp
    83   also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
    84   finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
    85   then have "p dvd m\<twosuperior>" ..
    86   with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
    87   then obtain k where "m = p * k" ..
    88   with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
    89   with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
    90   then have "p dvd n\<twosuperior>" ..
    91   with `prime p` have "p dvd n" by (rule prime_dvd_power_two)
    92   with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)
    93   with gcd have "p dvd 1" by simp
    94   then have "p \<le> 1" by (simp add: dvd_imp_le)
    95   with p show False by simp
    96 qed
    97 
    98 end