1(* Title: HOL/Library/Nat_Bijection.thy 2 Author: Brian Huffman 3 Author: Florian Haftmann 4 Author: Stefan Richter 5 Author: Tobias Nipkow 6 Author: Alexander Krauss 7*) 8 9section \<open>Bijections between natural numbers and other types\<close> 10 11theory Nat_Bijection 12 imports Main 13begin 14 15subsection \<open>Type \<^typ>\<open>nat \<times> nat\<close>\<close> 16 17text \<open>Triangle numbers: 0, 1, 3, 6, 10, 15, ...\<close> 18 19definition triangle :: "nat \<Rightarrow> nat" 20 where "triangle n = (n * Suc n) div 2" 21 22lemma triangle_0 [simp]: "triangle 0 = 0" 23 by (simp add: triangle_def) 24 25lemma triangle_Suc [simp]: "triangle (Suc n) = triangle n + Suc n" 26 by (simp add: triangle_def) 27 28definition prod_encode :: "nat \<times> nat \<Rightarrow> nat" 29 where "prod_encode = (\<lambda>(m, n). triangle (m + n) + m)" 30 31text \<open>In this auxiliary function, \<^term>\<open>triangle k + m\<close> is an invariant.\<close> 32 33fun prod_decode_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" 34 where "prod_decode_aux k m = 35 (if m \<le> k then (m, k - m) else prod_decode_aux (Suc k) (m - Suc k))" 36 37declare prod_decode_aux.simps [simp del] 38 39definition prod_decode :: "nat \<Rightarrow> nat \<times> nat" 40 where "prod_decode = prod_decode_aux 0" 41 42lemma prod_encode_prod_decode_aux: "prod_encode (prod_decode_aux k m) = triangle k + m" 43 apply (induct k m rule: prod_decode_aux.induct) 44 apply (subst prod_decode_aux.simps) 45 apply (simp add: prod_encode_def) 46 done 47 48lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n" 49 by (simp add: prod_decode_def prod_encode_prod_decode_aux) 50 51lemma prod_decode_triangle_add: "prod_decode (triangle k + m) = prod_decode_aux k m" 52 apply (induct k arbitrary: m) 53 apply (simp add: prod_decode_def) 54 apply (simp only: triangle_Suc add.assoc) 55 apply (subst prod_decode_aux.simps) 56 apply simp 57 done 58 59lemma prod_encode_inverse [simp]: "prod_decode (prod_encode x) = x" 60 unfolding prod_encode_def 61 apply (induct x) 62 apply (simp add: prod_decode_triangle_add) 63 apply (subst prod_decode_aux.simps) 64 apply simp 65 done 66 67lemma inj_prod_encode: "inj_on prod_encode A" 68 by (rule inj_on_inverseI) (rule prod_encode_inverse) 69 70lemma inj_prod_decode: "inj_on prod_decode A" 71 by (rule inj_on_inverseI) (rule prod_decode_inverse) 72 73lemma surj_prod_encode: "surj prod_encode" 74 by (rule surjI) (rule prod_decode_inverse) 75 76lemma surj_prod_decode: "surj prod_decode" 77 by (rule surjI) (rule prod_encode_inverse) 78 79lemma bij_prod_encode: "bij prod_encode" 80 by (rule bijI [OF inj_prod_encode surj_prod_encode]) 81 82lemma bij_prod_decode: "bij prod_decode" 83 by (rule bijI [OF inj_prod_decode surj_prod_decode]) 84 85lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y" 86 by (rule inj_prod_encode [THEN inj_eq]) 87 88lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y" 89 by (rule inj_prod_decode [THEN inj_eq]) 90 91 92text \<open>Ordering properties\<close> 93 94lemma le_prod_encode_1: "a \<le> prod_encode (a, b)" 95 by (simp add: prod_encode_def) 96 97lemma le_prod_encode_2: "b \<le> prod_encode (a, b)" 98 by (induct b) (simp_all add: prod_encode_def) 99 100 101subsection \<open>Type \<^typ>\<open>nat + nat\<close>\<close> 102 103definition sum_encode :: "nat + nat \<Rightarrow> nat" 104 where "sum_encode x = (case x of Inl a \<Rightarrow> 2 * a | Inr b \<Rightarrow> Suc (2 * b))" 105 106definition sum_decode :: "nat \<Rightarrow> nat + nat" 107 where "sum_decode n = (if even n then Inl (n div 2) else Inr (n div 2))" 108 109lemma sum_encode_inverse [simp]: "sum_decode (sum_encode x) = x" 110 by (induct x) (simp_all add: sum_decode_def sum_encode_def) 111 112lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n" 113 by (simp add: even_two_times_div_two sum_decode_def sum_encode_def) 114 115lemma inj_sum_encode: "inj_on sum_encode A" 116 by (rule inj_on_inverseI) (rule sum_encode_inverse) 117 118lemma inj_sum_decode: "inj_on sum_decode A" 119 by (rule inj_on_inverseI) (rule sum_decode_inverse) 120 121lemma surj_sum_encode: "surj sum_encode" 122 by (rule surjI) (rule sum_decode_inverse) 123 124lemma surj_sum_decode: "surj sum_decode" 125 by (rule surjI) (rule sum_encode_inverse) 126 127lemma bij_sum_encode: "bij sum_encode" 128 by (rule bijI [OF inj_sum_encode surj_sum_encode]) 129 130lemma bij_sum_decode: "bij sum_decode" 131 by (rule bijI [OF inj_sum_decode surj_sum_decode]) 132 133lemma sum_encode_eq: "sum_encode x = sum_encode y \<longleftrightarrow> x = y" 134 by (rule inj_sum_encode [THEN inj_eq]) 135 136lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y" 137 by (rule inj_sum_decode [THEN inj_eq]) 138 139 140subsection \<open>Type \<^typ>\<open>int\<close>\<close> 141 142definition int_encode :: "int \<Rightarrow> nat" 143 where "int_encode i = sum_encode (if 0 \<le> i then Inl (nat i) else Inr (nat (- i - 1)))" 144 145definition int_decode :: "nat \<Rightarrow> int" 146 where "int_decode n = (case sum_decode n of Inl a \<Rightarrow> int a | Inr b \<Rightarrow> - int b - 1)" 147 148lemma int_encode_inverse [simp]: "int_decode (int_encode x) = x" 149 by (simp add: int_decode_def int_encode_def) 150 151lemma int_decode_inverse [simp]: "int_encode (int_decode n) = n" 152 unfolding int_decode_def int_encode_def 153 using sum_decode_inverse [of n] by (cases "sum_decode n") simp_all 154 155lemma inj_int_encode: "inj_on int_encode A" 156 by (rule inj_on_inverseI) (rule int_encode_inverse) 157 158lemma inj_int_decode: "inj_on int_decode A" 159 by (rule inj_on_inverseI) (rule int_decode_inverse) 160 161lemma surj_int_encode: "surj int_encode" 162 by (rule surjI) (rule int_decode_inverse) 163 164lemma surj_int_decode: "surj int_decode" 165 by (rule surjI) (rule int_encode_inverse) 166 167lemma bij_int_encode: "bij int_encode" 168 by (rule bijI [OF inj_int_encode surj_int_encode]) 169 170lemma bij_int_decode: "bij int_decode" 171 by (rule bijI [OF inj_int_decode surj_int_decode]) 172 173lemma int_encode_eq: "int_encode x = int_encode y \<longleftrightarrow> x = y" 174 by (rule inj_int_encode [THEN inj_eq]) 175 176lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y" 177 by (rule inj_int_decode [THEN inj_eq]) 178 179 180subsection \<open>Type \<^typ>\<open>nat list\<close>\<close> 181 182fun list_encode :: "nat list \<Rightarrow> nat" 183 where 184 "list_encode [] = 0" 185 | "list_encode (x # xs) = Suc (prod_encode (x, list_encode xs))" 186 187function list_decode :: "nat \<Rightarrow> nat list" 188 where 189 "list_decode 0 = []" 190 | "list_decode (Suc n) = (case prod_decode n of (x, y) \<Rightarrow> x # list_decode y)" 191 by pat_completeness auto 192 193termination list_decode 194 apply (relation "measure id") 195 apply simp_all 196 apply (drule arg_cong [where f="prod_encode"]) 197 apply (drule sym) 198 apply (simp add: le_imp_less_Suc le_prod_encode_2) 199 done 200 201lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x" 202 by (induct x rule: list_encode.induct) simp_all 203 204lemma list_decode_inverse [simp]: "list_encode (list_decode n) = n" 205 apply (induct n rule: list_decode.induct) 206 apply simp 207 apply (simp split: prod.split) 208 apply (simp add: prod_decode_eq [symmetric]) 209 done 210 211lemma inj_list_encode: "inj_on list_encode A" 212 by (rule inj_on_inverseI) (rule list_encode_inverse) 213 214lemma inj_list_decode: "inj_on list_decode A" 215 by (rule inj_on_inverseI) (rule list_decode_inverse) 216 217lemma surj_list_encode: "surj list_encode" 218 by (rule surjI) (rule list_decode_inverse) 219 220lemma surj_list_decode: "surj list_decode" 221 by (rule surjI) (rule list_encode_inverse) 222 223lemma bij_list_encode: "bij list_encode" 224 by (rule bijI [OF inj_list_encode surj_list_encode]) 225 226lemma bij_list_decode: "bij list_decode" 227 by (rule bijI [OF inj_list_decode surj_list_decode]) 228 229lemma list_encode_eq: "list_encode x = list_encode y \<longleftrightarrow> x = y" 230 by (rule inj_list_encode [THEN inj_eq]) 231 232lemma list_decode_eq: "list_decode x = list_decode y \<longleftrightarrow> x = y" 233 by (rule inj_list_decode [THEN inj_eq]) 234 235 236subsection \<open>Finite sets of naturals\<close> 237 238subsubsection \<open>Preliminaries\<close> 239 240lemma finite_vimage_Suc_iff: "finite (Suc -` F) \<longleftrightarrow> finite F" 241 apply (safe intro!: finite_vimageI inj_Suc) 242 apply (rule finite_subset [where B="insert 0 (Suc ` Suc -` F)"]) 243 apply (rule subsetI) 244 apply (case_tac x) 245 apply simp 246 apply simp 247 apply (rule finite_insert [THEN iffD2]) 248 apply (erule finite_imageI) 249 done 250 251lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A" 252 by auto 253 254lemma vimage_Suc_insert_Suc: "Suc -` insert (Suc n) A = insert n (Suc -` A)" 255 by auto 256 257lemma div2_even_ext_nat: 258 fixes x y :: nat 259 assumes "x div 2 = y div 2" 260 and "even x \<longleftrightarrow> even y" 261 shows "x = y" 262proof - 263 from \<open>even x \<longleftrightarrow> even y\<close> have "x mod 2 = y mod 2" 264 by (simp only: even_iff_mod_2_eq_zero) auto 265 with assms have "x div 2 * 2 + x mod 2 = y div 2 * 2 + y mod 2" 266 by simp 267 then show ?thesis 268 by simp 269qed 270 271 272subsubsection \<open>From sets to naturals\<close> 273 274definition set_encode :: "nat set \<Rightarrow> nat" 275 where "set_encode = sum ((^) 2)" 276 277lemma set_encode_empty [simp]: "set_encode {} = 0" 278 by (simp add: set_encode_def) 279 280lemma set_encode_inf: "\<not> finite A \<Longrightarrow> set_encode A = 0" 281 by (simp add: set_encode_def) 282 283lemma set_encode_insert [simp]: "finite A \<Longrightarrow> n \<notin> A \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A" 284 by (simp add: set_encode_def) 285 286lemma even_set_encode_iff: "finite A \<Longrightarrow> even (set_encode A) \<longleftrightarrow> 0 \<notin> A" 287 by (induct set: finite) (auto simp: set_encode_def) 288 289lemma set_encode_vimage_Suc: "set_encode (Suc -` A) = set_encode A div 2" 290 apply (cases "finite A") 291 apply (erule finite_induct) 292 apply simp 293 apply (case_tac x) 294 apply (simp add: even_set_encode_iff vimage_Suc_insert_0) 295 apply (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc) 296 apply (simp add: set_encode_def finite_vimage_Suc_iff) 297 done 298 299lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric] 300 301 302subsubsection \<open>From naturals to sets\<close> 303 304definition set_decode :: "nat \<Rightarrow> nat set" 305 where "set_decode x = {n. odd (x div 2 ^ n)}" 306 307lemma set_decode_0 [simp]: "0 \<in> set_decode x \<longleftrightarrow> odd x" 308 by (simp add: set_decode_def) 309 310lemma set_decode_Suc [simp]: "Suc n \<in> set_decode x \<longleftrightarrow> n \<in> set_decode (x div 2)" 311 by (simp add: set_decode_def div_mult2_eq) 312 313lemma set_decode_zero [simp]: "set_decode 0 = {}" 314 by (simp add: set_decode_def) 315 316lemma set_decode_div_2: "set_decode (x div 2) = Suc -` set_decode x" 317 by auto 318 319lemma set_decode_plus_power_2: 320 "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)" 321proof (induct n arbitrary: z) 322 case 0 323 show ?case 324 proof (rule set_eqI) 325 show "q \<in> set_decode (2 ^ 0 + z) \<longleftrightarrow> q \<in> insert 0 (set_decode z)" for q 326 by (induct q) (use 0 in simp_all) 327 qed 328next 329 case (Suc n) 330 show ?case 331 proof (rule set_eqI) 332 show "q \<in> set_decode (2 ^ Suc n + z) \<longleftrightarrow> q \<in> insert (Suc n) (set_decode z)" for q 333 by (induct q) (use Suc in simp_all) 334 qed 335qed 336 337lemma finite_set_decode [simp]: "finite (set_decode n)" 338 apply (induct n rule: nat_less_induct) 339 apply (case_tac "n = 0") 340 apply simp 341 apply (drule_tac x="n div 2" in spec) 342 apply simp 343 apply (simp add: set_decode_div_2) 344 apply (simp add: finite_vimage_Suc_iff) 345 done 346 347 348subsubsection \<open>Proof of isomorphism\<close> 349 350lemma set_decode_inverse [simp]: "set_encode (set_decode n) = n" 351 apply (induct n rule: nat_less_induct) 352 apply (case_tac "n = 0") 353 apply simp 354 apply (drule_tac x="n div 2" in spec) 355 apply simp 356 apply (simp add: set_decode_div_2 set_encode_vimage_Suc) 357 apply (erule div2_even_ext_nat) 358 apply (simp add: even_set_encode_iff) 359 done 360 361lemma set_encode_inverse [simp]: "finite A \<Longrightarrow> set_decode (set_encode A) = A" 362 apply (erule finite_induct) 363 apply simp_all 364 apply (simp add: set_decode_plus_power_2) 365 done 366 367lemma inj_on_set_encode: "inj_on set_encode (Collect finite)" 368 by (rule inj_on_inverseI [where g = "set_decode"]) simp 369 370lemma set_encode_eq: "finite A \<Longrightarrow> finite B \<Longrightarrow> set_encode A = set_encode B \<longleftrightarrow> A = B" 371 by (rule iffI) (simp_all add: inj_onD [OF inj_on_set_encode]) 372 373lemma subset_decode_imp_le: 374 assumes "set_decode m \<subseteq> set_decode n" 375 shows "m \<le> n" 376proof - 377 have "n = m + set_encode (set_decode n - set_decode m)" 378 proof - 379 obtain A B where 380 "m = set_encode A" "finite A" 381 "n = set_encode B" "finite B" 382 by (metis finite_set_decode set_decode_inverse) 383 with assms show ?thesis 384 by auto (simp add: set_encode_def add.commute sum.subset_diff) 385 qed 386 then show ?thesis 387 by (metis le_add1) 388qed 389 390end 391