remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality

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

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

--- a/src/HOL/Library/Diagonalize.thy	Sat Dec 03 21:25:34 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-(* 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

--- a/src/HOL/Library/Library.thy	Sat Dec 03 21:25:34 2011 +0100
+++ b/src/HOL/Library/Library.thy	Sun Dec 04 13:10:19 2011 +0100
@@ -13,7 +13,6 @@
   Convex
   Countable
   Cset_Monad
-  Diagonalize
   Dlist_Cset
   Eval_Witness
   Extended_Nat