1.1 --- a/NEWS	Sat Dec 03 21:25:34 2011 +0100
     1.2 +++ b/NEWS	Sun Dec 04 13:10:19 2011 +0100
     1.3 @@ -53,6 +53,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use
     1.8 +theory HOL/Library/Nat_Bijection instead.
     1.9 +
    1.10  * Session HOL-Word: Discontinued many redundant theorems specific to type
    1.11  'a word. INCOMPATIBILITY, use the corresponding generic theorems instead.
    1.12  

     2.1 --- a/src/HOL/IsaMakefile	Sat Dec 03 21:25:34 2011 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Sun Dec 04 13:10:19 2011 +0100
     2.3 @@ -438,7 +438,7 @@
     2.4    Library/Code_Real_Approx_By_Float.thy					\
     2.5    Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
     2.6    Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
     2.7 -  Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy	\
     2.8 +  Library/Convex.thy Library/Countable.thy				\
     2.9    Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy	\
    2.10    Library/Eval_Witness.thy Library/Executable_Set.thy			\
    2.11    Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy	\

     3.1 --- a/src/HOL/Library/Diagonalize.thy	Sat Dec 03 21:25:34 2011 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,149 +0,0 @@
     3.4 -(* Author: Florian Haftmann, TU Muenchen *)
     3.5 -
     3.6 -header {* A constructive version of Cantor's first diagonalization argument. *}
     3.7 -
     3.8 -theory Diagonalize
     3.9 -imports Main
    3.10 -begin
    3.11 -
    3.12 -subsection {* Summation from @{text "0"} to @{text "n"} *}
    3.13 -
    3.14 -definition sum :: "nat \<Rightarrow> nat" where
    3.15 -  "sum n = n * Suc n div 2"
    3.16 -
    3.17 -lemma sum_0:
    3.18 -  "sum 0 = 0"
    3.19 -  unfolding sum_def by simp
    3.20 -
    3.21 -lemma sum_Suc:
    3.22 -  "sum (Suc n) = Suc n + sum n"
    3.23 -  unfolding sum_def by simp
    3.24 -
    3.25 -lemma sum2:
    3.26 -  "2 * sum n = n * Suc n"
    3.27 -proof -
    3.28 -  have "2 dvd n * Suc n"
    3.29 -  proof (cases "2 dvd n")
    3.30 -    case True then show ?thesis by simp
    3.31 -  next
    3.32 -    case False then have "2 dvd Suc n" by arith
    3.33 -    then show ?thesis by (simp del: mult_Suc_right)
    3.34 -  qed
    3.35 -  then have "n * Suc n div 2 * 2 = n * Suc n"
    3.36 -    by (rule dvd_div_mult_self [of "2::nat"])
    3.37 -  then show ?thesis by (simp add: sum_def)
    3.38 -qed
    3.39 -
    3.40 -lemma sum_strict_mono:
    3.41 -  "strict_mono sum"
    3.42 -proof (rule strict_monoI)
    3.43 -  fix m n :: nat
    3.44 -  assume "m < n"
    3.45 -  then have "m * Suc m < n * Suc n" by (intro mult_strict_mono) simp_all
    3.46 -  then have "2 * sum m < 2 * sum n" by (simp add: sum2)
    3.47 -  then show "sum m < sum n" by auto
    3.48 -qed
    3.49 -
    3.50 -lemma sum_not_less_self:
    3.51 -  "n \<le> sum n"
    3.52 -proof -
    3.53 -  have "2 * n \<le> n * Suc n" by auto
    3.54 -  with sum2 have "2 * n \<le> 2 * sum n" by simp
    3.55 -  then show ?thesis by simp
    3.56 -qed
    3.57 -
    3.58 -lemma sum_rest_aux:
    3.59 -  assumes "q \<le> n"
    3.60 -  assumes "sum m \<le> sum n + q"
    3.61 -  shows "m \<le> n"
    3.62 -proof (rule ccontr)
    3.63 -  assume "\<not> m \<le> n"
    3.64 -  then have "n < m" by simp
    3.65 -  then have "m \<ge> Suc n" by simp
    3.66 -  then have "m = m - Suc n + Suc n" by simp
    3.67 -  then have "m = Suc (n + (m - Suc n))" by simp
    3.68 -  then obtain r where "m = Suc (n + r)" by auto
    3.69 -  with `sum m \<le> sum n + q` have "sum (Suc (n + r)) \<le> sum n + q" by simp
    3.70 -  then have "sum (n + r) + Suc (n + r) \<le> sum n + q" unfolding sum_Suc by simp
    3.71 -  with `m = Suc (n + r)` have "sum (n + r) + m \<le> sum n + q" by simp
    3.72 -  have "sum n \<le> sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp
    3.73 -  moreover from `q \<le> n` `n < m` have "q < m" by simp
    3.74 -  ultimately have "sum n + q < sum (n + r) + m" by auto
    3.75 -  with `sum (n + r) + m \<le> sum n + q` show False
    3.76 -    by auto
    3.77 -qed
    3.78 -
    3.79 -lemma sum_rest:
    3.80 -  assumes "q \<le> n"
    3.81 -  shows "sum m \<le> sum n + q \<longleftrightarrow> m \<le> n"
    3.82 -using assms apply (auto intro: sum_rest_aux)
    3.83 -apply (simp add: strict_mono_less_eq [OF sum_strict_mono, symmetric, of m n])
    3.84 -done
    3.85 -
    3.86 -
    3.87 -subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *}
    3.88 -
    3.89 -definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    3.90 -  "diagonalize m n = sum (m + n) + m"
    3.91 -
    3.92 -lemma diagonalize_inject:
    3.93 -  assumes "diagonalize a b = diagonalize c d"
    3.94 -  shows "a = c" and "b = d"
    3.95 -proof -
    3.96 -  from assms have diageq: "sum (a + b) + a = sum (c + d) + c"
    3.97 -    by (simp add: diagonalize_def)
    3.98 -  have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
    3.99 -  then have "a = c \<and> b = d"
   3.100 -  proof (elim disjE)
   3.101 -    assume sumeq: "a + b = c + d"
   3.102 -    then have "a = c" using diageq by auto
   3.103 -    moreover from sumeq this have "b = d" by auto
   3.104 -    ultimately show ?thesis ..
   3.105 -  next
   3.106 -    assume "a + b \<ge> Suc (c + d)"
   3.107 -    with strict_mono_less_eq [OF sum_strict_mono]
   3.108 -      have "sum (a + b) \<ge> sum (Suc (c + d))" by simp
   3.109 -    with diageq show ?thesis by (simp add: sum_Suc)
   3.110 -  next
   3.111 -    assume "c + d \<ge> Suc (a + b)"
   3.112 -    with strict_mono_less_eq [OF sum_strict_mono]
   3.113 -      have "sum (c + d) \<ge> sum (Suc (a + b))" by simp
   3.114 -    with diageq show ?thesis by (simp add: sum_Suc)
   3.115 -  qed
   3.116 -  then show "a = c" and "b = d" by auto
   3.117 -qed
   3.118 -
   3.119 -
   3.120 -subsection {* The reverse diagonalization: reconstruction a pair of @{typ nat}s from one @{typ nat} *}
   3.121 -
   3.122 -text {* The inverse of the @{const sum} function *}
   3.123 -
   3.124 -definition tupelize :: "nat \<Rightarrow> nat \<times> nat" where
   3.125 -  "tupelize q = (let d = Max {d. sum d \<le> q}; m = q - sum d
   3.126 -     in (m, d - m))"
   3.127 -  
   3.128 -lemma tupelize_diagonalize:
   3.129 -  "tupelize (diagonalize m n) = (m, n)"
   3.130 -proof -
   3.131 -  from sum_rest
   3.132 -    have "\<And>r. sum r \<le> sum (m + n) + m \<longleftrightarrow> r \<le> m + n" by simp
   3.133 -  then have "Max {d. sum d \<le> (sum (m + n) + m)} = m + n"
   3.134 -    by (auto intro: Max_eqI)
   3.135 -  then show ?thesis
   3.136 -    by (simp add: tupelize_def diagonalize_def)
   3.137 -qed
   3.138 -
   3.139 -lemma snd_tupelize:
   3.140 -  "snd (tupelize n) \<le> n"
   3.141 -proof -
   3.142 -  have "sum 0 \<le> n" by (simp add: sum_0)
   3.143 -  then have "Max {m \<Colon> nat. sum m \<le> n} \<le> Max {m \<Colon> nat. m \<le> n}"
   3.144 -    by (intro Max_mono [of "{m. sum m \<le> n}" "{m. m \<le> n}"])
   3.145 -      (auto intro: Max_mono order_trans sum_not_less_self)
   3.146 -  also have "Max {m \<Colon> nat. m \<le> n} \<le> n"
   3.147 -    by (subst Max_le_iff) auto
   3.148 -  finally have "Max {m. sum m \<le> n} \<le> n" .
   3.149 -  then show ?thesis by (simp add: tupelize_def Let_def)
   3.150 -qed
   3.151 -
   3.152 -end

     4.1 --- a/src/HOL/Library/Library.thy	Sat Dec 03 21:25:34 2011 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Sun Dec 04 13:10:19 2011 +0100
     4.3 @@ -13,7 +13,6 @@
     4.4    Convex
     4.5    Countable
     4.6    Cset_Monad
     4.7 -  Diagonalize
     4.8    Dlist_Cset
     4.9    Eval_Witness
    4.10    Extended_Nat