9 theory NatPair |
9 theory NatPair |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 text{* |
13 text{* |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition |
15 \<nat>}. Definition and proofs are from \cite[page |
15 and proofs are from \cite[page 85]{Oberschelp:1993}. |
16 85]{Oberschelp:1993}. |
|
17 *} |
16 *} |
18 |
17 |
19 constdefs |
18 definition |
20 nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" |
19 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" |
20 "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" |
22 |
21 |
23 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" |
22 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" |
24 proof (cases "2 dvd a") |
23 proof (cases "2 dvd a") |
25 case True |
24 case True |
26 thus ?thesis by (rule dvd_mult2) |
25 then show ?thesis by (rule dvd_mult2) |
27 next |
26 next |
28 case False |
27 case False |
29 hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) |
28 then have "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) |
29 then have "Suc a mod 2 = 0" by (simp add: mod_Suc) |
31 hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) |
30 then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) |
32 thus ?thesis by (rule dvd_mult) |
31 then show ?thesis by (rule dvd_mult) |
33 qed |
32 qed |
34 |
33 |
35 lemma |
34 lemma |
36 assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" |
35 assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" |
37 shows nat2_to_nat_help: "u+v \<le> x+y" |
36 shows nat2_to_nat_help: "u+v \<le> x+y" |
38 proof (rule classical) |
37 proof (rule classical) |
39 assume "\<not> ?thesis" |
38 assume "\<not> ?thesis" |
40 hence contrapos: "x+y < u+v" |
39 then have contrapos: "x+y < u+v" |
41 by simp |
40 by simp |
42 have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" |
41 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) |
42 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" |
43 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) |
44 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 |
45 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" |
46 + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" |
48 proof - |
47 proof - |
49 have "2 dvd (x+y)*Suc(x+y)" |
48 have "2 dvd (x+y)*Suc(x+y)" |
50 by (rule dvd2_a_x_suc_a) |
49 by (rule dvd2_a_x_suc_a) |
51 hence "(x+y)*Suc(x+y) mod 2 = 0" |
50 then have "(x+y)*Suc(x+y) mod 2 = 0" |
52 by (simp only: dvd_eq_mod_eq_0) |
51 by (simp only: dvd_eq_mod_eq_0) |
53 also |
52 also |
54 have "2 * Suc(x+y) mod 2 = 0" |
53 have "2 * Suc(x+y) mod 2 = 0" |
55 by (rule mod_mult_self1_is_0) |
54 by (rule mod_mult_self1_is_0) |
56 ultimately have |
55 ultimately have |
57 "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" |
56 "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" |
58 by simp |
57 by simp |
59 thus ?thesis |
58 then show ?thesis |
60 by simp |
59 by simp |
61 qed |
60 qed |
62 also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" |
61 also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" |
63 by (rule div_add1_eq [symmetric]) |
62 by (rule div_add1_eq [symmetric]) |
64 also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" |
63 also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" |
73 |
72 |
74 theorem nat2_to_nat_inj: "inj nat2_to_nat" |
73 theorem nat2_to_nat_inj: "inj nat2_to_nat" |
75 proof - |
74 proof - |
76 { |
75 { |
77 fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)" |
76 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) |
77 then have "u+v \<le> x+y" by (rule nat2_to_nat_help) |
79 also from prems [symmetric] have "x+y \<le> u+v" |
78 also from prems [symmetric] have "x+y \<le> u+v" |
80 by (rule nat2_to_nat_help) |
79 by (rule nat2_to_nat_help) |
81 finally have eq: "u+v = x+y" . |
80 finally have eq: "u+v = x+y" . |
82 with prems have ux: "u=x" |
81 with prems have ux: "u=x" |
83 by (simp add: nat2_to_nat_def Let_def) |
82 by (simp add: nat2_to_nat_def Let_def) |
84 with eq have vy: "v=y" |
83 with eq have vy: "v=y" |
85 by simp |
84 by simp |
86 with ux have "(u,v) = (x,y)" |
85 with ux have "(u,v) = (x,y)" |
87 by simp |
86 by simp |
88 } |
87 } |
89 hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" |
88 then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" |
90 by fast |
89 by fast |
91 thus ?thesis |
90 then show ?thesis |
92 by (unfold inj_on_def) simp |
91 by (unfold inj_on_def) simp |
93 qed |
92 qed |
94 |
93 |
95 end |
94 end |