src/HOL/Library/Diagonalize.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 37388 793618618f78
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     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