# HG changeset patch # User haftmann # Date 1236367816 -3600 # Node ID a01b2de0e3e1fb052eb82840cf00930d44a39bf5 # Parent b3ae84c6e509f4d06e85a5e23de789b8bc9dc53d constructive version of Cantor's first diagonalization argument diff -r b3ae84c6e509 -r a01b2de0e3e1 NEWS --- 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". diff -r b3ae84c6e509 -r a01b2de0e3e1 src/HOL/IsaMakefile --- 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 \ diff -r b3ae84c6e509 -r a01b2de0e3e1 src/HOL/Library/Diagonalize.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 \ 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 \ sum n" +proof - + have "2 * n \ n * Suc n" by auto + with sum2 have "2 * n \ 2 * sum n" by simp + then show ?thesis by simp +qed + +lemma sum_rest_aux: + assumes "q \ n" + assumes "sum m \ sum n + q" + shows "m \ n" +proof (rule ccontr) + assume "\ m \ n" + then have "n < m" by simp + then have "m \ 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 \ sum n + q` have "sum (Suc (n + r)) \ sum n + q" by simp + then have "sum (n + r) + Suc (n + r) \ sum n + q" unfolding sum_Suc by simp + with `m = Suc (n + r)` have "sum (n + r) + m \ sum n + q" by simp + have "sum n \ sum (n + r)" unfolding strict_mono_less_eq [OF sum_strict_mono] by simp + moreover from `q \ n` `n < m` have "q < m" by simp + ultimately have "sum n + q < sum (n + r) + m" by auto + with `sum (n + r) + m \ sum n + q` show False + by auto +qed + +lemma sum_rest: + assumes "q \ n" + shows "sum m \ sum n + q \ m \ 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 \ nat \ 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 \ a + b \ Suc (c + d) \ c + d \ Suc (a + b)" by arith + then have "a = c \ 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 \ Suc (c + d)" + with strict_mono_less_eq [OF sum_strict_mono] + have "sum (a + b) \ sum (Suc (c + d))" by simp + with diageq show ?thesis by (simp add: sum_Suc) + next + assume "c + d \ Suc (a + b)" + with strict_mono_less_eq [OF sum_strict_mono] + have "sum (c + d) \ 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 \ nat \ nat" where + "tupelize q = (let d = Max {d. sum d \ q}; m = q - sum d + in (m, d - m))" + +lemma tupelize_diagonalize: + "tupelize (diagonalize m n) = (m, n)" +proof - + from sum_rest + have "\r. sum r \ sum (m + n) + m \ r \ m + n" by simp + then have "Max {d. sum d \ (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) \ n" +proof - + have "sum 0 \ n" by (simp add: sum_0) + then have "Max {m \ nat. sum m \ n} \ Max {m \ nat. m \ n}" + by (intro Max_mono [of "{m. sum m \ n}" "{m. m \ n}"]) + (auto intro: Max_mono order_trans sum_not_less_self) + also have "Max {m \ nat. m \ n} \ n" + by (subst Max_le_iff) auto + finally have "Max {m. sum m \ n} \ n" . + then show ?thesis by (simp add: tupelize_def Let_def) +qed + +end diff -r b3ae84c6e509 -r a01b2de0e3e1 src/HOL/Library/Library.thy --- 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