src/HOL/Library/Nat_Int_Bij.thy
 author paulson Thu Oct 01 16:42:53 2009 +0100 (2009-10-01) changeset 32822 45fa9254ddc8 parent 32338 e73eb2db4727 child 32960 69916a850301 permissions -rw-r--r--
Proved a new theorem: nat_to_nat2_inj
 nipkow@28098  1 (* Title: HOL/Nat_Int_Bij.thy  nipkow@28098  2  Author: Stefan Richter, Tobias Nipkow  nipkow@28098  3 *)  nipkow@28098  4 nipkow@28098  5 header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}  nipkow@28098  6 nipkow@28098  7 theory Nat_Int_Bij  haftmann@30663  8 imports Main  nipkow@28098  9 begin  nipkow@28098  10 nipkow@28098  11 subsection{* A bijection between @{text "\"} and @{text "\\"} *}  nipkow@28098  12 nipkow@28098  13 text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}  nipkow@28098  14 nipkow@28098  15 definition nat2_to_nat:: "(nat * nat) \ nat" where  nipkow@28098  16 "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"  nipkow@28098  17 definition nat_to_nat2:: "nat \ (nat * nat)" where  nipkow@28098  18 "nat_to_nat2 = inv nat2_to_nat"  nipkow@28098  19 nipkow@28098  20 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"  nipkow@28098  21 proof (cases "2 dvd a")  nipkow@28098  22  case True  nipkow@28098  23  then show ?thesis by (rule dvd_mult2)  nipkow@28098  24 next  nipkow@28098  25  case False  nipkow@28098  26  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)  nipkow@28098  27  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)  nipkow@28098  28  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)  nipkow@28098  29  then show ?thesis by (rule dvd_mult)  nipkow@28098  30 qed  nipkow@28098  31 nipkow@28098  32 lemma  nipkow@28098  33  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"  nipkow@28098  34  shows nat2_to_nat_help: "u+v \ x+y"  nipkow@28098  35 proof (rule classical)  nipkow@28098  36  assume "\ ?thesis"  nipkow@28098  37  then have contrapos: "x+y < u+v"  nipkow@28098  38  by simp  nipkow@28098  39  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"  nipkow@28098  40  by (unfold nat2_to_nat_def) (simp add: Let_def)  nipkow@28098  41  also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"  nipkow@28098  42  by (simp only: div_mult_self1_is_m)  nipkow@28098  43  also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2  nipkow@28098  44  + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"  nipkow@28098  45  proof -  nipkow@28098  46  have "2 dvd (x+y)*Suc(x+y)"  nipkow@28098  47  by (rule dvd2_a_x_suc_a)  nipkow@28098  48  then have "(x+y)*Suc(x+y) mod 2 = 0"  nipkow@28098  49  by (simp only: dvd_eq_mod_eq_0)  nipkow@28098  50  also  nipkow@28098  51  have "2 * Suc(x+y) mod 2 = 0"  nipkow@28098  52  by (rule mod_mult_self1_is_0)  nipkow@28098  53  ultimately have  nipkow@28098  54  "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"  nipkow@28098  55  by simp  nipkow@28098  56  then show ?thesis  nipkow@28098  57  by simp  nipkow@28098  58  qed  nipkow@28098  59  also have "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"  nipkow@28098  60  by (rule div_add1_eq [symmetric])  nipkow@28098  61  also have "\ = ((x+y+2)*Suc(x+y)) div 2"  nipkow@28098  62  by (simp only: add_mult_distrib [symmetric])  nipkow@28098  63  also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2"  nipkow@28098  64  by (simp only: mult_le_mono div_le_mono)  nipkow@28098  65  also have "\ \ nat2_to_nat (u,v)"  nipkow@28098  66  by (unfold nat2_to_nat_def) (simp add: Let_def)  nipkow@28098  67  finally show ?thesis  nipkow@28098  68  by (simp only: eq)  nipkow@28098  69 qed  nipkow@28098  70 nipkow@28098  71 theorem nat2_to_nat_inj: "inj nat2_to_nat"  nipkow@28098  72 proof -  nipkow@28098  73  {  nipkow@28098  74  fix u v x y  nipkow@28098  75  assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"  nipkow@28098  76  then have "u+v \ x+y" by (rule nat2_to_nat_help)  nipkow@28098  77  also from eq1 [symmetric] have "x+y \ u+v"  nipkow@28098  78  by (rule nat2_to_nat_help)  nipkow@28098  79  finally have eq2: "u+v = x+y" .  nipkow@28098  80  with eq1 have ux: "u=x"  nipkow@28098  81  by (simp add: nat2_to_nat_def Let_def)  nipkow@28098  82  with eq2 have vy: "v=y" by simp  nipkow@28098  83  with ux have "(u,v) = (x,y)" by simp  nipkow@28098  84  }  nipkow@28098  85  then have "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" by fast  nipkow@28098  86  then show ?thesis unfolding inj_on_def by simp  nipkow@28098  87 qed  nipkow@28098  88 nipkow@28098  89 lemma nat_to_nat2_surj: "surj nat_to_nat2"  nipkow@28098  90 by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)  nipkow@28098  91 nipkow@28098  92 nipkow@28098  93 lemma gauss_sum_nat_upto: "2 * (\i\n::nat. i) = n * (n + 1)"  nipkow@28098  94 using gauss_sum[where 'a = nat]  nipkow@28098  95 by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)  nipkow@28098  96 nipkow@28098  97 lemma nat2_to_nat_surj: "surj nat2_to_nat"  nipkow@28098  98 proof (unfold surj_def)  nipkow@28098  99  {  nipkow@28098  100  fix z::nat  nipkow@28098  101  def r \ "Max {r. (\i\r. i) \ z}"  nipkow@28098  102  def x \ "z - (\i\r. i)"  nipkow@28098  103 nipkow@28098  104  hence "finite {r. (\i\r. i) \ z}"  nipkow@28098  105  by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)  nipkow@28098  106  also have "0 \ {r. (\i\r. i) \ z}" by simp  nipkow@28098  107  hence "{r::nat. (\i\r. i) \ z} \ {}" by fast  nipkow@28098  108  ultimately have a: "r \ {r. (\i\r. i) \ z} \ (\s \ {r. (\i\r. i) \ z}. s \ r)"  nipkow@28098  109  by (simp add: r_def del:mem_Collect_eq)  nipkow@28098  110  {  nipkow@28098  111  assume "rx" by simp  nipkow@28098  113  hence "(\i\r. i)+(r+1)\z" using x_def by arith  nipkow@28098  114  hence "(r+1) \ {r. (\i\r. i) \ z}" by simp  nipkow@28098  115  with a have "(r+1)\r" by simp  nipkow@28098  116  }  nipkow@28098  117  hence b: "x\r" by force  nipkow@28098  118   nipkow@28098  119  def y \ "r-x"  nipkow@28098  120  have "2*z=2*(\i\r. i)+2*x" using x_def a by simp arith  nipkow@28098  121  also have "\ = r * (r+1) + 2*x" using gauss_sum_nat_upto by simp  nipkow@28098  122  also have "\ = (x+y)*(x+y+1)+2*x" using y_def b by simp  nipkow@28098  123  also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp }  nipkow@28098  124  hence "\ = 2 * nat2_to_nat(x,y)"  nipkow@28098  125  using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)  nipkow@28098  126  finally have "z=nat2_to_nat (x, y)" by simp  nipkow@28098  127  }  nipkow@28098  128  thus "\y. \x. y = nat2_to_nat x" by fast  nipkow@28098  129 qed  nipkow@28098  130 paulson@32822  131 lemma nat_to_nat2_inj: "inj nat_to_nat2"  paulson@32822  132  by (simp add: nat_to_nat2_def surj_imp_inj_inv nat2_to_nat_surj)  paulson@32822  133 nipkow@28098  134 nipkow@28098  135 subsection{* A bijection between @{text "\"} and @{text "\"} *}  nipkow@28098  136 nipkow@28098  137 definition nat_to_int_bij :: "nat \ int" where  nipkow@28098  138 "nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"  nipkow@28098  139 nipkow@28098  140 definition int_to_nat_bij :: "int \ nat" where  nipkow@28098  141 "int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"  nipkow@28098  142 nipkow@28098  143 lemma i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"  nipkow@28098  144 by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger  nipkow@28098  145 nipkow@28098  146 lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"  nipkow@28098  147 proof -  nipkow@28098  148  have "ALL m n::nat. m>0 \ 2 * m - Suc 0 \ 2 * n" by presburger  nipkow@28098  149  thus ?thesis  nipkow@28098  150  by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)  nipkow@28098  151 qed  nipkow@28098  152 nipkow@28098  153 lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"  nipkow@28098  154 by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)  nipkow@28098  155 nipkow@28098  156 lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"  nipkow@28098  157 by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)  nipkow@28098  158 nipkow@28098  159 lemma surj_nat_to_int_bij: "surj nat_to_int_bij"  nipkow@28098  160 by (blast intro: n2i_i2n_id surjI)  nipkow@28098  161 nipkow@28098  162 lemma surj_int_to_nat_bij: "surj int_to_nat_bij"  nipkow@28098  163 by (blast intro: i2n_n2i_id surjI)  nipkow@28098  164 nipkow@28098  165 lemma inj_nat_to_int_bij: "inj nat_to_int_bij"  nipkow@28098  166 by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)  nipkow@28098  167 nipkow@28098  168 lemma inj_int_to_nat_bij: "inj int_to_nat_bij"  nipkow@28098  169 by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)  nipkow@28098  170 nipkow@32338  171 lemma bij_nat_to_int_bij: "bij nat_to_int_bij"  nipkow@32338  172 by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)  nipkow@32338  173 nipkow@32338  174 lemma bij_int_to_nat_bij: "bij int_to_nat_bij"  nipkow@32338  175 by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)  nipkow@32338  176 nipkow@28098  177 nipkow@28098  178 end