summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Diagonalize.thy

author | haftmann |

Fri Aug 27 19:34:23 2010 +0200 (2010-08-27 ago) | |

changeset 38857 | 97775f3e8722 |

parent 37388 | 793618618f78 |

permissions | -rw-r--r-- |

renamed class/constant eq to equal; tuned some instantiations

1 (* Author: Florian Haftmann, TU Muenchen *)

3 header {* A constructive version of Cantor's first diagonalization argument. *}

5 theory Diagonalize

6 imports Main

7 begin

9 subsection {* Summation from @{text "0"} to @{text "n"} *}

11 definition sum :: "nat \<Rightarrow> nat" where

12 "sum n = n * Suc n div 2"

14 lemma sum_0:

15 "sum 0 = 0"

16 unfolding sum_def by simp

18 lemma sum_Suc:

19 "sum (Suc n) = Suc n + sum n"

20 unfolding sum_def by simp

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

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

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

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

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

84 subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *}

86 definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

87 "diagonalize m n = sum (m + n) + m"

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

117 subsection {* The reverse diagonalization: reconstruction a pair of @{typ nat}s from one @{typ nat} *}

119 text {* The inverse of the @{const sum} function *}

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))"

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

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

149 end