src/HOL/ex/Sqrt.thy
 changeset 30411 9c9b6511ad1b parent 28952 15a4b2cf8c34 child 31712 6f8aa9aea693
equal inserted replaced
`     1 (*  Title:      HOL/ex/Sqrt.thy`
`     1 (*  Title:      HOL/ex/Sqrt.thy`
`     2     Author:     Markus Wenzel, TU Muenchen`
`     2     Author:     Markus Wenzel, TU Muenchen`
`     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`
`    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`