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