src/HOL/Library/Diagonalize.thy

implement Mapping.map_entry

(* Author: Florian Haftmann, TU Muenchen *)

header {* A constructive version of Cantor's first diagonalization argument. *}

theory Diagonalize
imports Main
begin

subsection {* Summation from @{text "0"} to @{text "n"} *}

definition sum :: "nat \<Rightarrow> nat" where
  "sum n = n * Suc n div 2"

lemma sum_0:
  "sum 0 = 0"
  unfolding sum_def by simp

lemma sum_Suc:
  "sum (Suc n) = Suc n + sum n"
  unfolding sum_def by simp

lemma sum2:
  "2 * sum n = n * Suc n"
proof -
  have "2 dvd n * Suc n"
  proof (cases "2 dvd n")
    case True then show ?thesis by simp
  next
    case False then have "2 dvd Suc n" by arith
    then show ?thesis by (simp del: mult_Suc_right)
  qed
  then have "n * Suc n div 2 * 2 = n * Suc n"
    by (rule dvd_div_mult_self [of "2::nat"])
  then show ?thesis by (simp add: sum_def)
qed

lemma sum_strict_mono:
  "strict_mono sum"
proof (rule strict_monoI)
  fix m n :: nat
  assume "m < n"
  then have "m * Suc m < n * Suc n" by (intro mult_strict_mono) simp_all
  then have "2 * sum m < 2 * sum n" by (simp add: sum2)
  then show "sum m < sum n" by auto
qed

lemma sum_not_less_self:
  "n \<le> sum n"
proof -
  have "2 * n \<le> n * Suc n" by auto
  with sum2 have "2 * n \<le> 2 * sum n" by simp
  then show ?thesis by simp
qed

lemma sum_rest_aux:
  assumes "q \<le> n"
  assumes "sum m \<le> sum n + q"
  shows "m \<le> n"
proof (rule ccontr)
  assume "\<not> m \<le> n"
  then have "n < m" by simp
  then have "m \<ge> Suc n" by simp
  then have "m = m - Suc n + Suc n" by simp
  then have "m = Suc (n + (m - Suc n))" by simp
  then obtain r where "m = Suc (n + r)" by auto
  with `sum m \<le> sum n + q` have "sum (Suc (n + r)) \<le> sum n + q" by simp
  then have "sum (n + r) + Suc (n + r) \<le> sum n + q" unfolding sum_Suc by simp
  with `m = Suc (n + r)` have "sum (n + r) + m \<le> sum n + q" by simp
  have "sum n \<le> sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp
  moreover from `q \<le> n` `n < m` have "q < m" by simp
  ultimately have "sum n + q < sum (n + r) + m" by auto
  with `sum (n + r) + m \<le> sum n + q` show False
    by auto
qed

lemma sum_rest:
  assumes "q \<le> n"
  shows "sum m \<le> sum n + q \<longleftrightarrow> m \<le> n"
using assms apply (auto intro: sum_rest_aux)
apply (simp add: strict_mono_less_eq [OF sum_strict_mono, symmetric, of m n])
done


subsection {* Diagonalization: an injective embedding of two @{typ "nat"}s to one @{typ "nat"} *}

definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "diagonalize m n = sum (m + n) + m"

lemma diagonalize_inject:
  assumes "diagonalize a b = diagonalize c d"
  shows "a = c" and "b = d"
proof -
  from assms have diageq: "sum (a + b) + a = sum (c + d) + c"
    by (simp add: diagonalize_def)
  have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
  then have "a = c \<and> b = d"
  proof (elim disjE)
    assume sumeq: "a + b = c + d"
    then have "a = c" using diageq by auto
    moreover from sumeq this have "b = d" by auto
    ultimately show ?thesis ..
  next
    assume "a + b \<ge> Suc (c + d)"
    with strict_mono_less_eq [OF sum_strict_mono]
      have "sum (a + b) \<ge> sum (Suc (c + d))" by simp
    with diageq show ?thesis by (simp add: sum_Suc)
  next
    assume "c + d \<ge> Suc (a + b)"
    with strict_mono_less_eq [OF sum_strict_mono]
      have "sum (c + d) \<ge> sum (Suc (a + b))" by simp
    with diageq show ?thesis by (simp add: sum_Suc)
  qed
  then show "a = c" and "b = d" by auto
qed


subsection {* The reverse diagonalization: reconstruction a pair of @{typ nat}s from one @{typ nat} *}

text {* The inverse of the @{const sum} function *}

definition tupelize :: "nat \<Rightarrow> nat \<times> nat" where
  "tupelize q = (let d = Max {d. sum d \<le> q}; m = q - sum d
     in (m, d - m))"
  
lemma tupelize_diagonalize:
  "tupelize (diagonalize m n) = (m, n)"
proof -
  from sum_rest
    have "\<And>r. sum r \<le> sum (m + n) + m \<longleftrightarrow> r \<le> m + n" by simp
  then have "Max {d. sum d \<le> (sum (m + n) + m)} = m + n"
    by (auto intro: Max_eqI)
  then show ?thesis
    by (simp add: tupelize_def diagonalize_def)
qed

lemma snd_tupelize:
  "snd (tupelize n) \<le> n"
proof -
  have "sum 0 \<le> n" by (simp add: sum_0)
  then have "Max {m \<Colon> nat. sum m \<le> n} \<le> Max {m \<Colon> nat. m \<le> n}"
    by (intro Max_mono [of "{m. sum m \<le> n}" "{m. m \<le> n}"])
      (auto intro: Max_mono order_trans sum_not_less_self)
  also have "Max {m \<Colon> nat. m \<le> n} \<le> n"
    by (subst Max_le_iff) auto
  finally have "Max {m. sum m \<le> n} \<le> n" .
  then show ?thesis by (simp add: tupelize_def Let_def)
qed

end