src/HOL/Library/NatPair.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 15140 322485b816ac child 19736 d8d0f8f51d69 permissions -rw-r--r--
Constant "If" is now local
1 (*  Title:      HOL/Library/NatPair.thy
2     ID:         \$Id\$
3     Author:     Stefan Richter
4     Copyright   2003 Technische Universitaet Muenchen
5 *)
7 header {* Pairs of Natural Numbers *}
9 theory NatPair
10 imports Main
11 begin
13 text{*
14   An injective function from @{text "\<nat>\<twosuperior>"} to @{text
15   \<nat>}.  Definition and proofs are from \cite[page
16   85]{Oberschelp:1993}.
17 *}
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"
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
35 lemma
36   assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
37   shows nat2_to_nat_help: "u+v \<le> x+y"
38 proof (rule classical)
39   assume "\<not> ?thesis"
40   hence contrapos: "x+y < u+v"
41     by simp
42   have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
43     by (unfold nat2_to_nat_def) (simp add: Let_def)
44   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
45     by (simp only: div_mult_self1_is_m)
46   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
47     + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
48   proof -
49     have "2 dvd (x+y)*Suc(x+y)"
50       by (rule dvd2_a_x_suc_a)
51     hence "(x+y)*Suc(x+y) mod 2 = 0"
52       by (simp only: dvd_eq_mod_eq_0)
53     also
54     have "2 * Suc(x+y) mod 2 = 0"
55       by (rule mod_mult_self1_is_0)
56     ultimately have
57       "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
58       by simp
59     thus ?thesis
60       by simp
61   qed
62   also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
63     by (rule div_add1_eq [symmetric])
64   also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
65     by (simp only: add_mult_distrib [symmetric])
66   also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
67     by (simp only: mult_le_mono div_le_mono)
68   also have "\<dots> \<le> nat2_to_nat (u,v)"
69     by (unfold nat2_to_nat_def) (simp add: Let_def)
70   finally show ?thesis
71     by (simp only: eq)
72 qed
74 theorem nat2_to_nat_inj: "inj nat2_to_nat"
75 proof -
76   {
77     fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
78     hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
79     also from prems [symmetric] have "x+y \<le> u+v"
80       by (rule nat2_to_nat_help)
81     finally have eq: "u+v = x+y" .
82     with prems have ux: "u=x"
83       by (simp add: nat2_to_nat_def Let_def)
84     with eq have vy: "v=y"
85       by simp
86     with ux have "(u,v) = (x,y)"
87       by simp
88   }
89   hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
90     by fast
91   thus ?thesis
92     by (unfold inj_on_def) simp
93 qed
95 end