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