src/HOL/Library/Nat_Bijection.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 69593 3dda49e08b9d permissions -rw-r--r--
improved code equations taken over from AFP
```     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>\<open>nat \<times> nat\<close>\<close>
```
```    16
```
```    17 text \<open>Triangle numbers: 0, 1, 3, 6, 10, 15, ...\<close>
```
```    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   by (simp add: triangle_def)
```
```    24
```
```    25 lemma triangle_Suc [simp]: "triangle (Suc n) = triangle n + Suc n"
```
```    26   by (simp add: triangle_def)
```
```    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>\<open>triangle k + m\<close> is an invariant.\<close>
```
```    32
```
```    33 fun 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
```
```    37 declare prod_decode_aux.simps [simp del]
```
```    38
```
```    39 definition prod_decode :: "nat \<Rightarrow> nat \<times> nat"
```
```    40   where "prod_decode = prod_decode_aux 0"
```
```    41
```
```    42 lemma 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
```
```    48 lemma prod_decode_inverse [simp]: "prod_encode (prod_decode n) = n"
```
```    49   by (simp add: prod_decode_def prod_encode_prod_decode_aux)
```
```    50
```
```    51 lemma 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
```
```    59 lemma 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
```
```    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   by (simp add: prod_encode_def)
```
```    96
```
```    97 lemma le_prod_encode_2: "b \<le> prod_encode (a, b)"
```
```    98   by (induct b) (simp_all add: prod_encode_def)
```
```    99
```
```   100
```
```   101 subsection \<open>Type \<^typ>\<open>nat + nat\<close>\<close>
```
```   102
```
```   103 definition 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
```
```   106 definition 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
```
```   109 lemma sum_encode_inverse [simp]: "sum_decode (sum_encode x) = x"
```
```   110   by (induct x) (simp_all add: sum_decode_def sum_encode_def)
```
```   111
```
```   112 lemma 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
```
```   115 lemma inj_sum_encode: "inj_on sum_encode A"
```
```   116   by (rule inj_on_inverseI) (rule sum_encode_inverse)
```
```   117
```
```   118 lemma inj_sum_decode: "inj_on sum_decode A"
```
```   119   by (rule inj_on_inverseI) (rule sum_decode_inverse)
```
```   120
```
```   121 lemma surj_sum_encode: "surj sum_encode"
```
```   122   by (rule surjI) (rule sum_decode_inverse)
```
```   123
```
```   124 lemma surj_sum_decode: "surj sum_decode"
```
```   125   by (rule surjI) (rule sum_encode_inverse)
```
```   126
```
```   127 lemma bij_sum_encode: "bij sum_encode"
```
```   128   by (rule bijI [OF inj_sum_encode surj_sum_encode])
```
```   129
```
```   130 lemma bij_sum_decode: "bij sum_decode"
```
```   131   by (rule bijI [OF inj_sum_decode surj_sum_decode])
```
```   132
```
```   133 lemma sum_encode_eq: "sum_encode x = sum_encode y \<longleftrightarrow> x = y"
```
```   134   by (rule inj_sum_encode [THEN inj_eq])
```
```   135
```
```   136 lemma sum_decode_eq: "sum_decode x = sum_decode y \<longleftrightarrow> x = y"
```
```   137   by (rule inj_sum_decode [THEN inj_eq])
```
```   138
```
```   139
```
```   140 subsection \<open>Type \<^typ>\<open>int\<close>\<close>
```
```   141
```
```   142 definition 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
```
```   145 definition 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
```
```   148 lemma int_encode_inverse [simp]: "int_decode (int_encode x) = x"
```
```   149   by (simp add: int_decode_def int_encode_def)
```
```   150
```
```   151 lemma 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
```
```   155 lemma inj_int_encode: "inj_on int_encode A"
```
```   156   by (rule inj_on_inverseI) (rule int_encode_inverse)
```
```   157
```
```   158 lemma inj_int_decode: "inj_on int_decode A"
```
```   159   by (rule inj_on_inverseI) (rule int_decode_inverse)
```
```   160
```
```   161 lemma surj_int_encode: "surj int_encode"
```
```   162   by (rule surjI) (rule int_decode_inverse)
```
```   163
```
```   164 lemma surj_int_decode: "surj int_decode"
```
```   165   by (rule surjI) (rule int_encode_inverse)
```
```   166
```
```   167 lemma bij_int_encode: "bij int_encode"
```
```   168   by (rule bijI [OF inj_int_encode surj_int_encode])
```
```   169
```
```   170 lemma bij_int_decode: "bij int_decode"
```
```   171   by (rule bijI [OF inj_int_decode surj_int_decode])
```
```   172
```
```   173 lemma int_encode_eq: "int_encode x = int_encode y \<longleftrightarrow> x = y"
```
```   174   by (rule inj_int_encode [THEN inj_eq])
```
```   175
```
```   176 lemma int_decode_eq: "int_decode x = int_decode y \<longleftrightarrow> x = y"
```
```   177   by (rule inj_int_decode [THEN inj_eq])
```
```   178
```
```   179
```
```   180 subsection \<open>Type \<^typ>\<open>nat list\<close>\<close>
```
```   181
```
```   182 fun 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
```
```   187 function 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
```
```   193 termination 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
```
```   201 lemma list_encode_inverse [simp]: "list_decode (list_encode x) = x"
```
```   202   by (induct x rule: list_encode.induct) simp_all
```
```   203
```
```   204 lemma 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
```
```   211 lemma inj_list_encode: "inj_on list_encode A"
```
```   212   by (rule inj_on_inverseI) (rule list_encode_inverse)
```
```   213
```
```   214 lemma inj_list_decode: "inj_on list_decode A"
```
```   215   by (rule inj_on_inverseI) (rule list_decode_inverse)
```
```   216
```
```   217 lemma surj_list_encode: "surj list_encode"
```
```   218   by (rule surjI) (rule list_decode_inverse)
```
```   219
```
```   220 lemma surj_list_decode: "surj list_decode"
```
```   221   by (rule surjI) (rule list_encode_inverse)
```
```   222
```
```   223 lemma bij_list_encode: "bij list_encode"
```
```   224   by (rule bijI [OF inj_list_encode surj_list_encode])
```
```   225
```
```   226 lemma bij_list_decode: "bij list_decode"
```
```   227   by (rule bijI [OF inj_list_decode surj_list_decode])
```
```   228
```
```   229 lemma list_encode_eq: "list_encode x = list_encode y \<longleftrightarrow> x = y"
```
```   230   by (rule inj_list_encode [THEN inj_eq])
```
```   231
```
```   232 lemma list_decode_eq: "list_decode x = list_decode y \<longleftrightarrow> x = y"
```
```   233   by (rule inj_list_decode [THEN inj_eq])
```
```   234
```
```   235
```
```   236 subsection \<open>Finite sets of naturals\<close>
```
```   237
```
```   238 subsubsection \<open>Preliminaries\<close>
```
```   239
```
```   240 lemma 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
```
```   251 lemma vimage_Suc_insert_0: "Suc -` insert 0 A = Suc -` A"
```
```   252   by auto
```
```   253
```
```   254 lemma vimage_Suc_insert_Suc: "Suc -` insert (Suc n) A = insert n (Suc -` A)"
```
```   255   by auto
```
```   256
```
```   257 lemma 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"
```
```   262 proof -
```
```   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
```
```   269 qed
```
```   270
```
```   271
```
```   272 subsubsection \<open>From sets to naturals\<close>
```
```   273
```
```   274 definition set_encode :: "nat set \<Rightarrow> nat"
```
```   275   where "set_encode = sum ((^) 2)"
```
```   276
```
```   277 lemma set_encode_empty [simp]: "set_encode {} = 0"
```
```   278   by (simp add: set_encode_def)
```
```   279
```
```   280 lemma set_encode_inf: "\<not> finite A \<Longrightarrow> set_encode A = 0"
```
```   281   by (simp add: set_encode_def)
```
```   282
```
```   283 lemma 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
```
```   286 lemma 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
```
```   289 lemma 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
```
```   299 lemmas set_encode_div_2 = set_encode_vimage_Suc [symmetric]
```
```   300
```
```   301
```
```   302 subsubsection \<open>From naturals to sets\<close>
```
```   303
```
```   304 definition set_decode :: "nat \<Rightarrow> nat set"
```
```   305   where "set_decode x = {n. odd (x div 2 ^ n)}"
```
```   306
```
```   307 lemma set_decode_0 [simp]: "0 \<in> set_decode x \<longleftrightarrow> odd x"
```
```   308   by (simp add: set_decode_def)
```
```   309
```
```   310 lemma 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
```
```   313 lemma set_decode_zero [simp]: "set_decode 0 = {}"
```
```   314   by (simp add: set_decode_def)
```
```   315
```
```   316 lemma set_decode_div_2: "set_decode (x div 2) = Suc -` set_decode x"
```
```   317   by auto
```
```   318
```
```   319 lemma set_decode_plus_power_2:
```
```   320   "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
```
```   321 proof (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
```
```   328 next
```
```   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
```
```   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")
```
```   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
```
```   348 subsubsection \<open>Proof of isomorphism\<close>
```
```   349
```
```   350 lemma 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
```
```   361 lemma 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
```
```   367 lemma inj_on_set_encode: "inj_on set_encode (Collect finite)"
```
```   368   by (rule inj_on_inverseI [where g = "set_decode"]) simp
```
```   369
```
```   370 lemma 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
```
```   373 lemma subset_decode_imp_le:
```
```   374   assumes "set_decode m \<subseteq> set_decode n"
```
```   375   shows "m \<le> n"
```
```   376 proof -
```
```   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)
```
```   388 qed
```
```   389
```
```   390 end
```