src/HOL/Nat_Int_Bij.thy
 author wenzelm Wed Sep 17 21:27:14 2008 +0200 (2008-09-17) changeset 28263 69eaa97e7e96 parent 28098 c92850d2d16c permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:      HOL/Nat_Int_Bij.thy

     2     ID:         $Id$

     3     Author:     Stefan Richter, Tobias Nipkow

     4 *)

     5

     6 header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}

     7

     8 theory Nat_Int_Bij

     9 imports Hilbert_Choice Presburger

    10 begin

    11

    12 subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}

    13

    14 text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}

    15

    16 definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where

    17 "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"

    18 definition nat_to_nat2::  "nat \<Rightarrow> (nat * nat)" where

    19 "nat_to_nat2 = inv nat2_to_nat"

    20

    21 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"

    22 proof (cases "2 dvd a")

    23   case True

    24   then show ?thesis by (rule dvd_mult2)

    25 next

    26   case False

    27   then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)

    28   then have "Suc a mod 2 = 0" by (simp add: mod_Suc)

    29   then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)

    30   then show ?thesis by (rule dvd_mult)

    31 qed

    32

    33 lemma

    34   assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"

    35   shows nat2_to_nat_help: "u+v \<le> x+y"

    36 proof (rule classical)

    37   assume "\<not> ?thesis"

    38   then have contrapos: "x+y < u+v"

    39     by simp

    40   have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"

    41     by (unfold nat2_to_nat_def) (simp add: Let_def)

    42   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"

    43     by (simp only: div_mult_self1_is_m)

    44   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2

    45     + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"

    46   proof -

    47     have "2 dvd (x+y)*Suc(x+y)"

    48       by (rule dvd2_a_x_suc_a)

    49     then have "(x+y)*Suc(x+y) mod 2 = 0"

    50       by (simp only: dvd_eq_mod_eq_0)

    51     also

    52     have "2 * Suc(x+y) mod 2 = 0"

    53       by (rule mod_mult_self1_is_0)

    54     ultimately have

    55       "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"

    56       by simp

    57     then show ?thesis

    58       by simp

    59   qed

    60   also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"

    61     by (rule div_add1_eq [symmetric])

    62   also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"

    63     by (simp only: add_mult_distrib [symmetric])

    64   also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"

    65     by (simp only: mult_le_mono div_le_mono)

    66   also have "\<dots> \<le> nat2_to_nat (u,v)"

    67     by (unfold nat2_to_nat_def) (simp add: Let_def)

    68   finally show ?thesis

    69     by (simp only: eq)

    70 qed

    71

    72 theorem nat2_to_nat_inj: "inj nat2_to_nat"

    73 proof -

    74   {

    75     fix u v x y

    76     assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"

    77     then have "u+v \<le> x+y" by (rule nat2_to_nat_help)

    78     also from eq1 [symmetric] have "x+y \<le> u+v"

    79       by (rule nat2_to_nat_help)

    80     finally have eq2: "u+v = x+y" .

    81     with eq1 have ux: "u=x"

    82       by (simp add: nat2_to_nat_def Let_def)

    83     with eq2 have vy: "v=y" by simp

    84     with ux have "(u,v) = (x,y)" by simp

    85   }

    86   then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast

    87   then show ?thesis unfolding inj_on_def by simp

    88 qed

    89

    90 lemma nat_to_nat2_surj: "surj nat_to_nat2"

    91 by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)

    92

    93

    94 lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"

    95 using gauss_sum[where 'a = nat]

    96 by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)

    97

    98 lemma nat2_to_nat_surj: "surj nat2_to_nat"

    99 proof (unfold surj_def)

   100   {

   101     fix z::nat

   102     def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}"

   103     def x \<equiv> "z - (\<Sum>i\<le>r. i)"

   104

   105     hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"

   106       by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)

   107     also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp

   108     hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast

   109     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)"

   110       by (simp add: r_def del:mem_Collect_eq)

   111     {

   112       assume "r<x"

   113       hence "r+1\<le>x"  by simp

   114       hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith

   115       hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp

   116       with a have "(r+1)\<le>r"  by simp

   117     }

   118     hence b: "x\<le>r"  by force

   119

   120     def y \<equiv> "r-x"

   121     have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith

   122     also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp

   123     also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp

   124     also { have "2 dvd ((x+y)*(x+y+1))"	using dvd2_a_x_suc_a by simp }

   125     hence "\<dots> = 2 * nat2_to_nat(x,y)"

   126       using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)

   127     finally have "z=nat2_to_nat (x, y)"  by simp

   128   }

   129   thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast

   130 qed

   131

   132

   133 subsection{*  A bijection between @{text "\<nat>"} and @{text "\<int>"} *}

   134

   135 definition nat_to_int_bij :: "nat \<Rightarrow> int" where

   136 "nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"

   137

   138 definition int_to_nat_bij :: "int \<Rightarrow> nat" where

   139 "int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"

   140

   141 lemma  i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"

   142 by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger

   143

   144 lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"

   145 proof -

   146   have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger

   147   thus ?thesis

   148     by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)

   149 qed

   150

   151 lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"

   152 by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)

   153

   154 lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"

   155 by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)

   156

   157 lemma surj_nat_to_int_bij: "surj nat_to_int_bij"

   158 by (blast intro: n2i_i2n_id surjI)

   159

   160 lemma surj_int_to_nat_bij: "surj int_to_nat_bij"

   161 by (blast intro: i2n_n2i_id surjI)

   162

   163 lemma inj_nat_to_int_bij: "inj nat_to_int_bij"

   164 by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)

   165

   166 lemma inj_int_to_nat_bij: "inj int_to_nat_bij"

   167 by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)

   168

   169

   170 end