1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/ex/Sqrt_Irrational.thy	Thu Sep 27 18:43:40 2001 +0200
     1.3 @@ -0,0 +1,159 @@
     1.4 +(*  Title:      HOL/Real/ex/Sqrt_Irrational.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +*)
     1.9 +
    1.10 +header {*  Square roots of primes are irrational *}
    1.11 +
    1.12 +theory Sqrt_Irrational = Real + Primes:
    1.13 +
    1.14 +syntax (xsymbols)                        (* FIXME move to main HOL (!?) *)
    1.15 +  "_square" :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999)
    1.16 +syntax (HTML output)
    1.17 +  "_square" :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999)
    1.18 +syntax (output)
    1.19 +  "_square" :: "'a \<Rightarrow> 'a"  ("(_^2)" [1000] 999)
    1.20 +translations
    1.21 +  "x\<twosuperior>" \<rightleftharpoons> "x^2"
    1.22 +
    1.23 +
    1.24 +subsection {* The set of rational numbers *}
    1.25 +
    1.26 +constdefs
    1.27 +  rationals :: "real set"    ("\<rat>")
    1.28 +  "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
    1.29 +
    1.30 +theorem rationals_rep: "x \<in> \<rat> \<Longrightarrow>
    1.31 +  \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
    1.32 +proof -
    1.33 +  assume "x \<in> \<rat>"
    1.34 +  then obtain m n :: nat where n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
    1.35 +    by (unfold rationals_def) blast
    1.36 +  let ?gcd = "gcd (m, n)"
    1.37 +  from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
    1.38 +  let ?k = "m div ?gcd"
    1.39 +  let ?l = "n div ?gcd"
    1.40 +  let ?gcd' = "gcd (?k, ?l)"
    1.41 +  have "?gcd dvd m" .. hence gcd_k: "?gcd * ?k = m"
    1.42 +    by (rule dvd_mult_div_cancel)
    1.43 +  have "?gcd dvd n" .. hence gcd_l: "?gcd * ?l = n"
    1.44 +    by (rule dvd_mult_div_cancel)
    1.45 +
    1.46 +  from n gcd_l have "?l \<noteq> 0"
    1.47 +    by (auto iff del: neq0_conv)
    1.48 +  moreover
    1.49 +  have "\<bar>x\<bar> = real ?k / real ?l"
    1.50 +  proof -
    1.51 +    from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)"
    1.52 +      by (simp add: real_mult_div_cancel1)
    1.53 +    also from gcd_k gcd_l have "\<dots> = real m / real n" by simp
    1.54 +    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
    1.55 +    finally show ?thesis ..
    1.56 +  qed
    1.57 +  moreover
    1.58 +  have "?gcd' = 1"
    1.59 +  proof -
    1.60 +    have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)"
    1.61 +      by (rule gcd_mult_distrib2)
    1.62 +    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
    1.63 +    with gcd show ?thesis by simp
    1.64 +  qed
    1.65 +  ultimately show ?thesis by blast
    1.66 +qed
    1.67 +
    1.68 +lemma [elim?]: "r \<in> \<rat> \<Longrightarrow>
    1.69 +    (\<And>m n. n \<noteq> 0 \<Longrightarrow> \<bar>r\<bar> = real m / real n \<Longrightarrow> gcd (m, n) = 1 \<Longrightarrow> C) \<Longrightarrow> C"
    1.70 +  by (insert rationals_rep) blast
    1.71 +
    1.72 +
    1.73 +subsection {* Main theorem *}
    1.74 +
    1.75 +text {*
    1.76 +  The square root of any prime number (including @{text 2}) is
    1.77 +  irrational.
    1.78 +*}
    1.79 +
    1.80 +theorem sqrt_prime_irrational: "x\<twosuperior> = real p \<Longrightarrow> p \<in> prime \<Longrightarrow> x \<notin> \<rat>"
    1.81 +proof
    1.82 +  assume x_sqrt: "x\<twosuperior> = real p"
    1.83 +  assume p_prime: "p \<in> prime"
    1.84 +  hence p: "1 < p" by (simp add: prime_def)
    1.85 +  assume "x \<in> \<rat>"
    1.86 +  then obtain m n where
    1.87 +    n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" and gcd: "gcd (m, n) = 1" ..
    1.88 +  have eq: "m\<twosuperior> = p * n\<twosuperior>"
    1.89 +  proof -
    1.90 +    from n x_rat have "real m = \<bar>x\<bar> * real n" by simp
    1.91 +    hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)" by (simp split: abs_split)
    1.92 +    also from x_sqrt have "\<dots> = real (p * n\<twosuperior>)" by simp
    1.93 +    finally show ?thesis ..
    1.94 +  qed
    1.95 +  have "p dvd m \<and> p dvd n"
    1.96 +  proof
    1.97 +    from eq have "p dvd m\<twosuperior>" ..
    1.98 +    with p_prime show "p dvd m" by (rule prime_dvd_square)
    1.99 +    then obtain k where "m = p * k" ..
   1.100 +    with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: mult_ac)
   1.101 +    with p have "n\<twosuperior> = p * k\<twosuperior>" by simp
   1.102 +    hence "p dvd n\<twosuperior>" ..
   1.103 +    with p_prime show "p dvd n" by (rule prime_dvd_square)
   1.104 +  qed
   1.105 +  hence "p dvd gcd (m, n)" ..
   1.106 +  with gcd have "p dvd 1" by simp
   1.107 +  hence "p \<le> 1" by (simp add: dvd_imp_le)
   1.108 +  with p show False by simp
   1.109 +qed
   1.110 +
   1.111 +
   1.112 +subsection {* Variations *}
   1.113 +
   1.114 +text {*
   1.115 +  Just for the record: we instantiate the main theorem for the
   1.116 +  specific prime number @{text 2} (real mathematicians would never do
   1.117 +  this formally :-).
   1.118 +*}
   1.119 +
   1.120 +theorem "x\<twosuperior> = real 2 \<Longrightarrow> x \<notin> \<rat>"
   1.121 +proof (rule sqrt_prime_irrational)
   1.122 +  {
   1.123 +    fix m assume dvd: "m dvd 2"
   1.124 +    hence "m \<le> 2" by (simp add: dvd_imp_le)
   1.125 +    moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
   1.126 +    ultimately have "m = 1 \<or> m = 2" by arith
   1.127 +  }
   1.128 +  thus "2 \<in> prime" by (simp add: prime_def)
   1.129 +qed
   1.130 +
   1.131 +text {*
   1.132 +  \medskip An alternative version of the main proof, using mostly
   1.133 +  linear forward-reasoning.  While this results in less top-down
   1.134 +  structure, it is probably closer to proofs seen in mathematics.
   1.135 +*}
   1.136 +
   1.137 +theorem "x\<twosuperior> = real p \<Longrightarrow> p \<in> prime \<Longrightarrow> x \<notin> \<rat>"
   1.138 +proof
   1.139 +  assume x_sqrt: "x\<twosuperior> = real p"
   1.140 +  assume p_prime: "p \<in> prime"
   1.141 +  hence p: "1 < p" by (simp add: prime_def)
   1.142 +  assume "x \<in> \<rat>"
   1.143 +  then obtain m n where
   1.144 +    n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n" and gcd: "gcd (m, n) = 1" ..
   1.145 +  from n x_rat have "real m = \<bar>x\<bar> * real n" by simp
   1.146 +  hence "real (m\<twosuperior>) = x\<twosuperior> * real (n\<twosuperior>)" by (simp split: abs_split)
   1.147 +  also from x_sqrt have "\<dots> = real (p * n\<twosuperior>)" by simp
   1.148 +  finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
   1.149 +  hence "p dvd m\<twosuperior>" ..
   1.150 +  with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_square)
   1.151 +  then obtain k where "m = p * k" ..
   1.152 +  with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: mult_ac)
   1.153 +  with p have "n\<twosuperior> = p * k\<twosuperior>" by simp
   1.154 +  hence "p dvd n\<twosuperior>" ..
   1.155 +  with p_prime have "p dvd n" by (rule prime_dvd_square)
   1.156 +  with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
   1.157 +  with gcd have "p dvd 1" by simp
   1.158 +  hence "p \<le> 1" by (simp add: dvd_imp_le)
   1.159 +  with p show False by simp
   1.160 +qed
   1.161 +
   1.162 +end