--- a/NEWS Fri Mar 06 20:29:37 2009 +0100
+++ b/NEWS Fri Mar 06 20:30:16 2009 +0100
@@ -220,6 +220,9 @@
*** HOL ***
+* Theory Library/Diagonalize.thy provides constructive version of
+Cantor's first diagonalization argument.
+
* New predicate "strict_mono" classifies strict functions on partial orders.
With strict functions on linear orders, reasoning about (in)equalities is
facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less".
--- a/src/HOL/IsaMakefile Fri Mar 06 20:29:37 2009 +0100
+++ b/src/HOL/IsaMakefile Fri Mar 06 20:30:16 2009 +0100
@@ -318,7 +318,7 @@
Library/Finite_Cartesian_Product.thy \
Library/FrechetDeriv.thy \
Library/Fundamental_Theorem_Algebra.thy \
- Library/Inner_Product.thy \
+ Library/Inner_Product.thy Library/Lattice_Syntax.thy \
Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \
Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy \
Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \
@@ -332,13 +332,13 @@
Library/List_lexord.thy Library/Commutative_Ring.thy \
Library/comm_ring.ML Library/Coinductive_List.thy \
Library/AssocList.thy Library/Formal_Power_Series.thy \
- Library/Binomial.thy Library/Eval_Witness.thy \
+ Library/Binomial.thy Library/Eval_Witness.thy \
Library/Code_Index.thy Library/Code_Char.thy \
Library/Code_Char_chr.thy Library/Code_Integer.thy \
- Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
- Library/Boolean_Algebra.thy Library/Countable.thy \
- Library/RBT.thy Library/Univ_Poly.thy \
- Library/Random.thy Library/Quickcheck.thy \
+ Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
+ Library/Boolean_Algebra.thy Library/Countable.thy \
+ Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \
+ Library/Random.thy Library/Quickcheck.thy \
Library/Poly_Deriv.thy \
Library/Polynomial.thy \
Library/Product_plus.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Diagonalize.thy Fri Mar 06 20:30:16 2009 +0100
@@ -0,0 +1,149 @@
+(* 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 Fri Mar 06 20:29:37 2009 +0100
+++ b/src/HOL/Library/Library.thy Fri Mar 06 20:30:16 2009 +0100
@@ -17,6 +17,7 @@
ContNotDenum
Countable
Determinants
+ Diagonalize
Efficient_Nat
Enum
Eval_Witness
@@ -28,6 +29,7 @@
Fundamental_Theorem_Algebra
Infinite_Set
Inner_Product
+ Lattice_Syntax
ListVector
Mapping
Multiset