src/HOL/Library/Nat_Int_Bij.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32822 45fa9254ddc8
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
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 "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
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) \<Rightarrow> 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 \<Rightarrow> (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 \<le> x+y"
nipkow@28098
    35
proof (rule classical)
nipkow@28098
    36
  assume "\<not> ?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 "\<dots> = (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 "\<dots> = (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 "\<dots> = ((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 "\<dots> = ((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 "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
nipkow@28098
    64
    by (simp only: mult_le_mono div_le_mono)
nipkow@28098
    65
  also have "\<dots> \<le> 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 \<le> x+y" by (rule nat2_to_nat_help)
nipkow@28098
    77
    also from eq1 [symmetric] have "x+y \<le> 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 "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> 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 * (\<Sum>i\<le>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 \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}" 
nipkow@28098
   102
    def x \<equiv> "z - (\<Sum>i\<le>r. i)"
nipkow@28098
   103
nipkow@28098
   104
    hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"
nipkow@28098
   105
      by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
nipkow@28098
   106
    also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
nipkow@28098
   107
    hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast
nipkow@28098
   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)"
nipkow@28098
   109
      by (simp add: r_def del:mem_Collect_eq)
nipkow@28098
   110
    {
nipkow@28098
   111
      assume "r<x"
nipkow@28098
   112
      hence "r+1\<le>x"  by simp
nipkow@28098
   113
      hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith
nipkow@28098
   114
      hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
nipkow@28098
   115
      with a have "(r+1)\<le>r"  by simp
nipkow@28098
   116
    }
nipkow@28098
   117
    hence b: "x\<le>r"  by force
nipkow@28098
   118
    
nipkow@28098
   119
    def y \<equiv> "r-x"
nipkow@28098
   120
    have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith
nipkow@28098
   121
    also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp
nipkow@28098
   122
    also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
wenzelm@32960
   123
    also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp }
nipkow@28098
   124
    hence "\<dots> = 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 "\<forall>y. \<exists>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 "\<nat>"} and @{text "\<int>"} *}
nipkow@28098
   136
nipkow@28098
   137
definition nat_to_int_bij :: "nat \<Rightarrow> 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 \<Rightarrow> 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 \<longrightarrow> 2 * m - Suc 0 \<noteq> 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