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