src/HOL/Library/Diagonalize.thy
 author haftmann Wed Apr 22 19:09:21 2009 +0200 (2009-04-22) changeset 30960 fec1a04b7220 parent 30326 a01b2de0e3e1 child 37388 793618618f78 permissions -rw-r--r--
power operation defined generic
 haftmann@30326 1 (* Author: Florian Haftmann, TU Muenchen *) haftmann@30326 2 haftmann@30326 3 header {* A constructive version of Cantor's first diagonalization argument. *} haftmann@30326 4 haftmann@30326 5 theory Diagonalize haftmann@30326 6 imports Main haftmann@30326 7 begin haftmann@30326 8 haftmann@30326 9 subsection {* Summation from @{text "0"} to @{text "n"} *} haftmann@30326 10 haftmann@30326 11 definition sum :: "nat \ nat" where haftmann@30326 12 "sum n = n * Suc n div 2" haftmann@30326 13 haftmann@30326 14 lemma sum_0: haftmann@30326 15 "sum 0 = 0" haftmann@30326 16 unfolding sum_def by simp haftmann@30326 17 haftmann@30326 18 lemma sum_Suc: haftmann@30326 19 "sum (Suc n) = Suc n + sum n" haftmann@30326 20 unfolding sum_def by simp haftmann@30326 21 haftmann@30326 22 lemma sum2: haftmann@30326 23 "2 * sum n = n * Suc n" haftmann@30326 24 proof - haftmann@30326 25 have "2 dvd n * Suc n" haftmann@30326 26 proof (cases "2 dvd n") haftmann@30326 27 case True then show ?thesis by simp haftmann@30326 28 next haftmann@30326 29 case False then have "2 dvd Suc n" by arith haftmann@30326 30 then show ?thesis by (simp del: mult_Suc_right) haftmann@30326 31 qed haftmann@30326 32 then have "n * Suc n div 2 * 2 = n * Suc n" haftmann@30326 33 by (rule dvd_div_mult_self [of "2::nat"]) haftmann@30326 34 then show ?thesis by (simp add: sum_def) haftmann@30326 35 qed haftmann@30326 36 haftmann@30326 37 lemma sum_strict_mono: haftmann@30326 38 "strict_mono sum" haftmann@30326 39 proof (rule strict_monoI) haftmann@30326 40 fix m n :: nat haftmann@30326 41 assume "m < n" haftmann@30326 42 then have "m * Suc m < n * Suc n" by (intro mult_strict_mono) simp_all haftmann@30326 43 then have "2 * sum m < 2 * sum n" by (simp add: sum2) haftmann@30326 44 then show "sum m < sum n" by auto haftmann@30326 45 qed haftmann@30326 46 haftmann@30326 47 lemma sum_not_less_self: haftmann@30326 48 "n \ sum n" haftmann@30326 49 proof - haftmann@30326 50 have "2 * n \ n * Suc n" by auto haftmann@30326 51 with sum2 have "2 * n \ 2 * sum n" by simp haftmann@30326 52 then show ?thesis by simp haftmann@30326 53 qed haftmann@30326 54 haftmann@30326 55 lemma sum_rest_aux: haftmann@30326 56 assumes "q \ n" haftmann@30326 57 assumes "sum m \ sum n + q" haftmann@30326 58 shows "m \ n" haftmann@30326 59 proof (rule ccontr) haftmann@30326 60 assume "\ m \ n" haftmann@30326 61 then have "n < m" by simp haftmann@30326 62 then have "m \ Suc n" by simp haftmann@30326 63 then have "m = m - Suc n + Suc n" by simp haftmann@30326 64 then have "m = Suc (n + (m - Suc n))" by simp haftmann@30326 65 then obtain r where "m = Suc (n + r)" by auto haftmann@30326 66 with `sum m \ sum n + q` have "sum (Suc (n + r)) \ sum n + q" by simp haftmann@30326 67 then have "sum (n + r) + Suc (n + r) \ sum n + q" unfolding sum_Suc by simp haftmann@30326 68 with `m = Suc (n + r)` have "sum (n + r) + m \ sum n + q" by simp haftmann@30326 69 have "sum n \ sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp haftmann@30326 70 moreover from `q \ n` `n < m` have "q < m" by simp haftmann@30326 71 ultimately have "sum n + q < sum (n + r) + m" by auto haftmann@30326 72 with `sum (n + r) + m \ sum n + q` show False haftmann@30326 73 by auto haftmann@30326 74 qed haftmann@30326 75 haftmann@30326 76 lemma sum_rest: haftmann@30326 77 assumes "q \ n" haftmann@30326 78 shows "sum m \ sum n + q \ m \ n" haftmann@30326 79 using assms apply (auto intro: sum_rest_aux) haftmann@30326 80 apply (simp add: strict_mono_less_eq [OF sum_strict_mono, symmetric, of m n]) haftmann@30326 81 done haftmann@30326 82 haftmann@30326 83 haftmann@30326 84 subsection {* Diagonalization: an injective embedding of two @{typ "nat"}s to one @{typ "nat"} *} haftmann@30326 85 haftmann@30326 86 definition diagonalize :: "nat \ nat \ nat" where haftmann@30326 87 "diagonalize m n = sum (m + n) + m" haftmann@30326 88 haftmann@30326 89 lemma diagonalize_inject: haftmann@30326 90 assumes "diagonalize a b = diagonalize c d" haftmann@30326 91 shows "a = c" and "b = d" haftmann@30326 92 proof - haftmann@30326 93 from assms have diageq: "sum (a + b) + a = sum (c + d) + c" haftmann@30326 94 by (simp add: diagonalize_def) haftmann@30326 95 have "a + b = c + d \ a + b \ Suc (c + d) \ c + d \ Suc (a + b)" by arith haftmann@30326 96 then have "a = c \ b = d" haftmann@30326 97 proof (elim disjE) haftmann@30326 98 assume sumeq: "a + b = c + d" haftmann@30326 99 then have "a = c" using diageq by auto haftmann@30326 100 moreover from sumeq this have "b = d" by auto haftmann@30326 101 ultimately show ?thesis .. haftmann@30326 102 next haftmann@30326 103 assume "a + b \ Suc (c + d)" haftmann@30326 104 with strict_mono_less_eq [OF sum_strict_mono] haftmann@30326 105 have "sum (a + b) \ sum (Suc (c + d))" by simp haftmann@30326 106 with diageq show ?thesis by (simp add: sum_Suc) haftmann@30326 107 next haftmann@30326 108 assume "c + d \ Suc (a + b)" haftmann@30326 109 with strict_mono_less_eq [OF sum_strict_mono] haftmann@30326 110 have "sum (c + d) \ sum (Suc (a + b))" by simp haftmann@30326 111 with diageq show ?thesis by (simp add: sum_Suc) haftmann@30326 112 qed haftmann@30326 113 then show "a = c" and "b = d" by auto haftmann@30326 114 qed haftmann@30326 115 haftmann@30326 116 haftmann@30326 117 subsection {* The reverse diagonalization: reconstruction a pair of @{typ nat}s from one @{typ nat} *} haftmann@30326 118 haftmann@30326 119 text {* The inverse of the @{const sum} function *} haftmann@30326 120 haftmann@30326 121 definition tupelize :: "nat \ nat \ nat" where haftmann@30326 122 "tupelize q = (let d = Max {d. sum d \ q}; m = q - sum d haftmann@30326 123 in (m, d - m))" haftmann@30326 124 haftmann@30326 125 lemma tupelize_diagonalize: haftmann@30326 126 "tupelize (diagonalize m n) = (m, n)" haftmann@30326 127 proof - haftmann@30326 128 from sum_rest haftmann@30326 129 have "\r. sum r \ sum (m + n) + m \ r \ m + n" by simp haftmann@30326 130 then have "Max {d. sum d \ (sum (m + n) + m)} = m + n" haftmann@30326 131 by (auto intro: Max_eqI) haftmann@30326 132 then show ?thesis haftmann@30326 133 by (simp add: tupelize_def diagonalize_def) haftmann@30326 134 qed haftmann@30326 135 haftmann@30326 136 lemma snd_tupelize: haftmann@30326 137 "snd (tupelize n) \ n" haftmann@30326 138 proof - haftmann@30326 139 have "sum 0 \ n" by (simp add: sum_0) haftmann@30326 140 then have "Max {m \ nat. sum m \ n} \ Max {m \ nat. m \ n}" haftmann@30326 141 by (intro Max_mono [of "{m. sum m \ n}" "{m. m \ n}"]) haftmann@30326 142 (auto intro: Max_mono order_trans sum_not_less_self) haftmann@30326 143 also have "Max {m \ nat. m \ n} \ n" haftmann@30326 144 by (subst Max_le_iff) auto haftmann@30326 145 finally have "Max {m. sum m \ n} \ n" . haftmann@30326 146 then show ?thesis by (simp add: tupelize_def Let_def) haftmann@30326 147 qed haftmann@30326 148 haftmann@30326 149 end