equal
deleted
inserted
replaced
1 (* Title: HOL/Nat_Int_Bij.thy |
1 (* Title: HOL/Nat_Int_Bij.thy |
2 ID: $Id$ |
|
3 Author: Stefan Richter, Tobias Nipkow |
2 Author: Stefan Richter, Tobias Nipkow |
4 *) |
3 *) |
5 |
4 |
6 header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*} |
5 header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*} |
7 |
6 |
8 theory Nat_Int_Bij |
7 theory Nat_Int_Bij |
9 imports Hilbert_Choice Presburger |
8 imports Main |
10 begin |
9 begin |
11 |
10 |
12 subsection{* A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *} |
11 subsection{* A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *} |
13 |
12 |
14 text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *} |
13 text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *} |