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