|
1 (* Title: HOL/Library/DenumRat.thy |
|
2 ID: $Id$ |
|
3 Author: Benjamin Porter, 2006 |
|
4 *) |
|
5 |
|
6 header "Denumerability of the Rationals" |
|
7 |
|
8 theory DenumRat |
|
9 imports |
|
10 Complex_Main NatPair |
|
11 begin |
|
12 |
|
13 lemma nat_to_int_surj: "\<exists>f::nat\<Rightarrow>int. surj f" |
|
14 proof |
|
15 let ?f = "\<lambda>n. if (n mod 2 = 0) then - int (n div 2) else int ((n - 1) div 2 + 1)" |
|
16 have "\<forall>y. \<exists>x. y = ?f x" |
|
17 proof |
|
18 fix y::int |
|
19 { |
|
20 assume yl0: "y \<le> 0" |
|
21 then obtain n where ndef: "n = nat (- y * 2)" by simp |
|
22 from yl0 have g0: "- y * 2 \<ge> 0" by simp |
|
23 hence "nat (- y * 2) mod (nat 2) = nat ((-y * 2) mod 2)" by (subst nat_mod_distrib, auto) |
|
24 moreover have "(-y * 2) mod 2 = 0" by arith |
|
25 ultimately have "nat (- y * 2) mod 2 = 0" by simp |
|
26 with ndef have "n mod 2 = 0" by simp |
|
27 hence "?f n = - int (n div 2)" by simp |
|
28 also with ndef have "\<dots> = - int (nat (-y * 2) div 2)" by simp |
|
29 also with g0 have "\<dots> = - int (nat (((-y) * 2) div 2))" using nat_div_distrib by auto |
|
30 also have "\<dots> = - int (nat (-y))" using zdiv_zmult_self1 [of "2" "- y"] |
|
31 by simp |
|
32 also from yl0 have "\<dots> = y" using nat_0_le by auto |
|
33 finally have "?f n = y" . |
|
34 hence "\<exists>x. y = ?f x" by blast |
|
35 } |
|
36 moreover |
|
37 { |
|
38 assume "\<not>(y \<le> 0)" |
|
39 hence yg0: "y > 0" by simp |
|
40 hence yn0: "y \<noteq> 0" by simp |
|
41 from yg0 have g0: "y*2 + -2 \<ge> 0" by arith |
|
42 from yg0 obtain n where ndef: "n = nat (y * 2 - 1)" by simp |
|
43 from yg0 have "nat (y*2 - 1) mod 2 = nat ((y*2 - 1) mod 2)" using nat_mod_distrib by auto |
|
44 also have "\<dots> = nat ((y*2 + - 1) mod 2)" by (auto simp add: diff_int_def) |
|
45 also have "\<dots> = nat (1)" by (auto simp add: zmod_zadd_left_eq) |
|
46 finally have "n mod 2 = 1" using ndef by auto |
|
47 hence "?f n = int ((n - 1) div 2 + 1)" by simp |
|
48 also with ndef have "\<dots> = int ((nat (y*2 - 1) - 1) div 2 + 1)" by simp |
|
49 also with yg0 have "\<dots> = int (nat (y*2 - 2) div 2 + 1)" by arith |
|
50 also have "\<dots> = int (nat (y*2 + -2) div 2 + 1)" by (simp add: diff_int_def) |
|
51 also have "\<dots> = int (nat (y*2 + -2) div (nat 2) + 1)" by auto |
|
52 also from g0 have "\<dots> = int (nat ((y*2 + -2) div 2) + 1)" |
|
53 using nat_div_distrib by auto |
|
54 also have "\<dots> = int (nat ((y*2) div 2 + (-2) div 2 + ((y*2) mod 2 + (-2) mod 2) div 2) + 1)" |
|
55 by (auto simp add: zdiv_zadd1_eq) |
|
56 also from yg0 g0 have "\<dots> = int (nat (y))" |
|
57 by (auto) |
|
58 finally have "?f n = y" using yg0 by auto |
|
59 hence "\<exists>x. y = ?f x" by blast |
|
60 } |
|
61 ultimately show "\<exists>x. y = ?f x" by (rule case_split) |
|
62 qed |
|
63 thus "surj ?f" by (fold surj_def) |
|
64 qed |
|
65 |
|
66 lemma nat2_to_int2_surj: "\<exists>f::(nat*nat)\<Rightarrow>(int*int). surj f" |
|
67 proof - |
|
68 from nat_to_int_surj obtain g::"nat\<Rightarrow>int" where "surj g" .. |
|
69 hence aux: "\<forall>y. \<exists>x. y = g x" by (unfold surj_def) |
|
70 let ?f = "\<lambda>n. (g (fst n), g (snd n))" |
|
71 { |
|
72 fix y::"(int*int)" |
|
73 from aux have "\<exists>x1 x2. fst y = g x1 \<and> snd y = g x2" by auto |
|
74 hence "\<exists>x. fst y = g (fst x) \<and> snd y = g (snd x)" by auto |
|
75 hence "\<exists>x. (fst y, snd y) = (g (fst x), g (snd x))" by blast |
|
76 hence "\<exists>x. y = ?f x" by auto |
|
77 } |
|
78 hence "\<forall>y. \<exists>x. y = ?f x" by auto |
|
79 hence "surj ?f" by (fold surj_def) |
|
80 thus ?thesis by auto |
|
81 qed |
|
82 |
|
83 lemma rat_denum: |
|
84 "\<exists>f::nat\<Rightarrow>rat. surj f" |
|
85 proof - |
|
86 have "inj nat2_to_nat" by (rule nat2_to_nat_inj) |
|
87 hence "surj (inv nat2_to_nat)" by (rule inj_imp_surj_inv) |
|
88 moreover from nat2_to_int2_surj obtain h::"(nat*nat)\<Rightarrow>(int*int)" where "surj h" .. |
|
89 ultimately have "surj (h o (inv nat2_to_nat))" by (rule comp_surj) |
|
90 hence "\<exists>f::nat\<Rightarrow>(int*int). surj f" by auto |
|
91 then obtain g::"nat\<Rightarrow>(int*int)" where "surj g" by auto |
|
92 hence gdef: "\<forall>y. \<exists>x. y = g x" by (unfold surj_def) |
|
93 { |
|
94 fix y |
|
95 obtain a b where y: "y = Fract a b" by (cases y) |
|
96 from gdef |
|
97 obtain x where "(a,b) = g x" by blast |
|
98 hence "g x = (a,b)" .. |
|
99 with y have "y = (split Fract o g) x" by simp |
|
100 hence "\<exists>x. y = (split Fract o g) x" .. |
|
101 } |
|
102 hence "surj (split Fract o g)" |
|
103 by (simp add: surj_def) |
|
104 thus ?thesis by blast |
|
105 qed |
|
106 |
|
107 |
|
108 end |