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