src/HOL/Library/Diagonalize.thy
author haftmann
Tue Jun 08 16:37:22 2010 +0200 (2010-06-08)
changeset 37388 793618618f78
parent 30326 a01b2de0e3e1
permissions -rw-r--r--
tuned quotes, antiquotations and whitespace
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 \<Rightarrow> 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 \<le> sum n"
haftmann@30326
    49
proof -
haftmann@30326
    50
  have "2 * n \<le> n * Suc n" by auto
haftmann@30326
    51
  with sum2 have "2 * n \<le> 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 \<le> n"
haftmann@30326
    57
  assumes "sum m \<le> sum n + q"
haftmann@30326
    58
  shows "m \<le> n"
haftmann@30326
    59
proof (rule ccontr)
haftmann@30326
    60
  assume "\<not> m \<le> n"
haftmann@30326
    61
  then have "n < m" by simp
haftmann@30326
    62
  then have "m \<ge> 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 \<le> sum n + q` have "sum (Suc (n + r)) \<le> sum n + q" by simp
haftmann@30326
    67
  then have "sum (n + r) + Suc (n + r) \<le> sum n + q" unfolding sum_Suc by simp
haftmann@30326
    68
  with `m = Suc (n + r)` have "sum (n + r) + m \<le> sum n + q" by simp
haftmann@30326
    69
  have "sum n \<le> sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp
haftmann@30326
    70
  moreover from `q \<le> 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 \<le> 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 \<le> n"
haftmann@30326
    78
  shows "sum m \<le> sum n + q \<longleftrightarrow> m \<le> 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@37388
    84
subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *}
haftmann@30326
    85
haftmann@30326
    86
definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> 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 \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
haftmann@30326
    96
  then have "a = c \<and> 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 \<ge> Suc (c + d)"
haftmann@30326
   104
    with strict_mono_less_eq [OF sum_strict_mono]
haftmann@30326
   105
      have "sum (a + b) \<ge> 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 \<ge> Suc (a + b)"
haftmann@30326
   109
    with strict_mono_less_eq [OF sum_strict_mono]
haftmann@30326
   110
      have "sum (c + d) \<ge> 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 \<Rightarrow> nat \<times> nat" where
haftmann@30326
   122
  "tupelize q = (let d = Max {d. sum d \<le> 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 "\<And>r. sum r \<le> sum (m + n) + m \<longleftrightarrow> r \<le> m + n" by simp
haftmann@30326
   130
  then have "Max {d. sum d \<le> (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) \<le> n"
haftmann@30326
   138
proof -
haftmann@30326
   139
  have "sum 0 \<le> n" by (simp add: sum_0)
haftmann@30326
   140
  then have "Max {m \<Colon> nat. sum m \<le> n} \<le> Max {m \<Colon> nat. m \<le> n}"
haftmann@30326
   141
    by (intro Max_mono [of "{m. sum m \<le> n}" "{m. m \<le> n}"])
haftmann@30326
   142
      (auto intro: Max_mono order_trans sum_not_less_self)
haftmann@30326
   143
  also have "Max {m \<Colon> nat. m \<le> n} \<le> n"
haftmann@30326
   144
    by (subst Max_le_iff) auto
haftmann@30326
   145
  finally have "Max {m. sum m \<le> n} \<le> 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