author | nipkow |
Sat, 20 Jun 2009 01:53:39 +0200 | |
changeset 31729 | b9299916d618 |
parent 30663 | 0b6aff7451b2 |
child 32338 | e73eb2db4727 |
permissions | -rw-r--r-- |
28098 | 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 |
|
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
29888
diff
changeset
|
8 |
imports Main |
28098 | 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 |
||
132 |
subsection{* A bijection between @{text "\<nat>"} and @{text "\<int>"} *} |
|
133 |
||
134 |
definition nat_to_int_bij :: "nat \<Rightarrow> int" where |
|
135 |
"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))" |
|
136 |
||
137 |
definition int_to_nat_bij :: "int \<Rightarrow> nat" where |
|
138 |
"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)" |
|
139 |
||
140 |
lemma i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n" |
|
141 |
by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger |
|
142 |
||
143 |
lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i" |
|
144 |
proof - |
|
145 |
have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger |
|
146 |
thus ?thesis |
|
147 |
by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def) |
|
148 |
qed |
|
149 |
||
150 |
lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij" |
|
151 |
by (simp add: i2n_n2i_id inv_equality n2i_i2n_id) |
|
152 |
||
153 |
lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij" |
|
154 |
by (simp add: i2n_n2i_id inv_equality n2i_i2n_id) |
|
155 |
||
156 |
lemma surj_nat_to_int_bij: "surj nat_to_int_bij" |
|
157 |
by (blast intro: n2i_i2n_id surjI) |
|
158 |
||
159 |
lemma surj_int_to_nat_bij: "surj int_to_nat_bij" |
|
160 |
by (blast intro: i2n_n2i_id surjI) |
|
161 |
||
162 |
lemma inj_nat_to_int_bij: "inj nat_to_int_bij" |
|
163 |
by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv) |
|
164 |
||
165 |
lemma inj_int_to_nat_bij: "inj int_to_nat_bij" |
|
166 |
by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv) |
|
167 |
||
168 |
||
169 |
end |