|
1 (* Title: HOL/Library/NatPair.thy |
|
2 ID: $Id$ |
|
3 Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 Copyright 1996 University of Cambridge |
|
5 *) |
|
6 |
|
7 header {* |
|
8 \title{Pairs of Natural Numbers} |
|
9 \author{Stefan Richter} |
|
10 *} |
|
11 |
|
12 theory NatPair = Main: |
|
13 |
|
14 text{*An injective function from $\mathbf{N}^2$ to |
|
15 $\mathbf{N}$. Definition and proofs are from |
|
16 Arnold Oberschelp. Rekursionstheorie. BI-Wissenschafts-Verlag, 1993 |
|
17 (page 85). *} |
|
18 |
|
19 constdefs |
|
20 nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" |
|
21 "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n" |
|
22 |
|
23 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" |
|
24 proof (cases "2 dvd a") |
|
25 case True |
|
26 thus ?thesis by (rule dvd_mult2) |
|
27 next |
|
28 case False |
|
29 hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) |
|
30 hence "Suc a mod 2 = 0" by (simp add: mod_Suc) |
|
31 hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) |
|
32 thus ?thesis by (rule dvd_mult) |
|
33 qed |
|
34 |
|
35 lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" |
|
36 shows nat2_to_nat_help: "u+v \<le> x+y" |
|
37 proof (rule classical) |
|
38 assume "\<not> ?thesis" |
|
39 hence contrapos: "x+y < u+v" |
|
40 by simp |
|
41 have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" |
|
42 by (unfold nat2_to_nat_def) (simp add: Let_def) |
|
43 also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" |
|
44 by (simp only: div_mult_self1_is_m) |
|
45 also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 |
|
46 + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" |
|
47 proof - |
|
48 have "2 dvd (x+y)*Suc(x+y)" |
|
49 by (rule dvd2_a_x_suc_a) |
|
50 hence "(x+y)*Suc(x+y) mod 2 = 0" |
|
51 by (simp only: dvd_eq_mod_eq_0) |
|
52 also |
|
53 have "2 * Suc(x+y) mod 2 = 0" |
|
54 by (rule mod_mult_self1_is_0) |
|
55 ultimately have |
|
56 "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" |
|
57 by simp |
|
58 thus ?thesis |
|
59 by simp |
|
60 qed |
|
61 also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" |
|
62 by (rule div_add1_eq[THEN sym]) |
|
63 also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" |
|
64 by (simp only: add_mult_distrib[THEN sym]) |
|
65 also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2" |
|
66 by (simp only: mult_le_mono div_le_mono) |
|
67 also have "\<dots> \<le> nat2_to_nat (u,v)" |
|
68 by (unfold nat2_to_nat_def) (simp add: Let_def) |
|
69 finally show ?thesis |
|
70 by (simp only: eq) |
|
71 qed |
|
72 |
|
73 lemma nat2_to_nat_inj: "inj nat2_to_nat" |
|
74 proof - |
|
75 {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)" |
|
76 hence "u+v \<le> x+y" by (rule nat2_to_nat_help) |
|
77 also from prems[THEN sym] have "x+y \<le> u+v" |
|
78 by (rule nat2_to_nat_help) |
|
79 finally have eq: "u+v = x+y" . |
|
80 with prems have ux: "u=x" |
|
81 by (simp add: nat2_to_nat_def Let_def) |
|
82 with eq have vy: "v=y" |
|
83 by simp |
|
84 with ux have "(u,v) = (x,y)" |
|
85 by simp |
|
86 } |
|
87 hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" |
|
88 by fast |
|
89 thus ?thesis |
|
90 by (unfold inj_on_def) simp |
|
91 qed |
|
92 |
|
93 end |