1 theory NatBijection |
|
2 imports Main Parity "~~/src/HOL/Library/Discrete" |
|
3 begin |
|
4 |
|
5 declare One_nat_def[simp del] |
|
6 |
|
7 fun oddfactor :: "nat \<Rightarrow> nat" where |
|
8 [simp del]: "oddfactor n = (if n = 0 then 0 |
|
9 else if even n then oddfactor (n div 2) else ((n - 1) div 2))" |
|
10 |
|
11 fun evenfactor :: "nat \<Rightarrow> nat" where |
|
12 [simp del]: "evenfactor n = (if n = 0 then 0 |
|
13 else if even n then 2 * evenfactor (n div 2) else 1)" |
|
14 |
|
15 lemma oddfactor [simp]: |
|
16 "oddfactor 0 = 0" |
|
17 "odd n \<Longrightarrow> oddfactor n = (n - 1) div 2" |
|
18 "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)" |
|
19 by (simp_all add: oddfactor.simps) |
|
20 |
|
21 lemma evenfactor [simp]: |
|
22 "evenfactor 0 = 0" |
|
23 "odd n \<Longrightarrow> evenfactor n = 1" |
|
24 "even n \<Longrightarrow> evenfactor n = 2 * evenfactor (n div 2)" |
|
25 apply(simp_all add: evenfactor.simps) |
|
26 apply(case_tac n) |
|
27 apply(simp_all) |
|
28 done |
|
29 |
|
30 fun penc :: "(nat \<times> nat) \<Rightarrow> nat" where |
|
31 "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1" |
|
32 |
|
33 fun pdec :: "nat \<Rightarrow> nat \<times> nat" where |
|
34 "pdec z = (Discrete.log (evenfactor (Suc z)), oddfactor (Suc z))" |
|
35 |
|
36 lemma q2: "pdec (penc m) = m" |
|
37 apply(case_tac m) |
|
38 apply(simp) |
|
39 apply(simp only: penc.simps pdec.simps) |
|
40 apply(case_tac m) |
|
41 apply(simp only: penc.simps pdec.simps) |
|
42 apply(subst y1) |
|
43 apply(subst y2) |
|
44 apply(simp) |
|
45 done |
|
46 |
|
47 |
|
48 lemma oddfactor_odd: |
|
49 "oddfactor n = 0 \<or> odd (oddfactor n)" |
|
50 apply(induct n rule: nat_less_induct) |
|
51 apply(case_tac "n = 0") |
|
52 apply(simp) |
|
53 apply(case_tac "odd n") |
|
54 apply(auto) |
|
55 done |
|
56 |
|
57 lemma bigger: "oddfactor (Suc n) > 0" |
|
58 apply(induct n rule: nat_less_induct) |
|
59 apply(case_tac "n = 0") |
|
60 apply(simp) |
|
61 apply(case_tac "odd n") |
|
62 apply(auto) |
|
63 apply(drule_tac x="n div 2" in spec) |
|
64 apply(drule mp) |
|
65 apply(auto) |
|
66 by (smt numeral_2_eq_2 odd_nat_plus_one_div_two) |
|
67 |
|
68 fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
69 "pencode m n = (2 ^ m) * (2 * n + 1) - 1" |
|
70 |
|
71 fun pdecode2 :: "nat \<Rightarrow> nat" where |
|
72 "pdecode2 z = (oddfactor (Suc z) - 1) div 2" |
|
73 |
|
74 fun pdecode1 :: "nat \<Rightarrow> nat" where |
|
75 "pdecode1 z = Discrete.log ((Suc z) div (oddfactor (Suc z)))" |
|
76 |
|
77 lemma k: |
|
78 "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n" |
|
79 apply(induct m) |
|
80 apply(simp_all) |
|
81 done |
|
82 |
|
83 lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n" |
|
84 apply(induct n rule: nat_less_induct) |
|
85 apply(case_tac "n=0") |
|
86 apply(simp) |
|
87 apply(case_tac "odd n") |
|
88 apply(simp) |
|
89 apply(rule_tac x="0" in exI) |
|
90 apply(simp) |
|
91 apply(simp) |
|
92 apply(drule_tac x="n div 2" in spec) |
|
93 apply(erule impE) |
|
94 apply(simp) |
|
95 apply(erule exE) |
|
96 apply(rule_tac x="Suc k" in exI) |
|
97 apply(simp) |
|
98 by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral) |
|
99 |
|
100 |
|
101 lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y" |
|
102 by simp |
|
103 |
|
104 lemma m: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) = n div (oddfactor n)" |
|
105 apply(induct n rule: nat_less_induct) |
|
106 apply(case_tac "n=0") |
|
107 apply(simp) |
|
108 apply(case_tac "odd n") |
|
109 apply(simp) |
|
110 apply(drule_tac x="n div 2" in spec) |
|
111 apply(drule mp) |
|
112 apply(auto)[1] |
|
113 apply(drule mp) |
|
114 apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat) |
|
115 apply(subst (asm) oddfactor(3)[symmetric]) |
|
116 apply(simp) |
|
117 apply(subst (asm) oddfactor(3)[symmetric]) |
|
118 apply(simp) |
|
119 apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2") |
|
120 prefer 2 |
|
121 apply (metis div_mult2_eq nat_mult_commute) |
|
122 apply(simp only: log_half) |
|
123 apply(case_tac "n div oddfactor n = 0") |
|
124 apply(simp) |
|
125 apply(simp del: oddfactor) |
|
126 apply(drule test) |
|
127 apply(subst (asm) power.simps(2)[symmetric]) |
|
128 apply(subgoal_tac "Suc (Discrete.log (n div oddfactor n) - 1) = Discrete.log (n div oddfactor n)") |
|
129 prefer 2 |
|
130 apply (smt log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76)) |
|
131 apply(simp only: One_nat_def) |
|
132 apply(subst dvd_mult_div_cancel) |
|
133 apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww) |
|
134 apply(simp (no_asm)) |
|
135 done |
|
136 |
|
137 lemma m1: "n div oddfactor n * oddfactor n = n" |
|
138 apply(induct n rule: nat_less_induct) |
|
139 apply(case_tac "n=0") |
|
140 apply(simp) |
|
141 apply(case_tac "odd n") |
|
142 apply(simp) |
|
143 apply(simp) |
|
144 apply(drule_tac x="n div 2" in spec) |
|
145 apply(drule mp) |
|
146 apply(auto)[1] |
|
147 by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww) |
|
148 |
|
149 |
|
150 lemma m2: "0 < n ==> 2 ^ Discrete.log (n div (oddfactor n)) * (oddfactor n) = n" |
|
151 apply(subst m) |
|
152 apply(simp) |
|
153 apply(subst m1) |
|
154 apply(simp) |
|
155 done |
|
156 |
|
157 lemma y1: |
|
158 "pdecode2 (pencode m n) = n" |
|
159 apply(simp del: One_nat_def) |
|
160 apply(subst k) |
|
161 apply(auto) |
|
162 done |
|
163 |
|
164 lemma y2: |
|
165 "pdecode1 (pencode m n) = m" |
|
166 apply(simp only: pdecode1.simps pencode.simps) |
|
167 apply(subst Suc_diff_1) |
|
168 apply(auto)[1] |
|
169 apply(subst Suc_diff_1) |
|
170 apply(auto)[1] |
|
171 apply(subst k) |
|
172 apply(auto)[1] |
|
173 by (metis Suc_eq_plus1 Suc_neq_Zero comm_semiring_1_class.normalizing_semiring_rules(7) div_mult_self1_is_id log_exp) |
|
174 |
|
175 lemma yy: |
|
176 "pencode (pdecode1 m) (pdecode2 m) = m" |
|
177 apply(induct m rule: nat_less_induct) |
|
178 apply(simp (no_asm)) |
|
179 apply(case_tac "n = 0") |
|
180 apply(simp) |
|
181 apply(subst dvd_mult_div_cancel) |
|
182 using oddfactor_odd |
|
183 apply - |
|
184 apply(drule_tac x="Suc n" in meta_spec) |
|
185 apply(erule disjE) |
|
186 apply(auto)[1] |
|
187 apply (metis One_nat_def even_num_iff nat_even_iff_2_dvd odd_pos) |
|
188 using bigger |
|
189 apply - |
|
190 apply(rotate_tac 3) |
|
191 apply(drule_tac x="n" in meta_spec) |
|
192 apply(simp del: pencode.simps pdecode2.simps pdecode1.simps One_nat_def add: One_nat_def[symmetric]) |
|
193 apply(subst m2) |
|
194 apply(simp) |
|
195 apply(simp) |
|
196 done |
|
197 |
|
198 fun penc where |
|
199 "penc (m, n) = pencode m n" |
|
200 |
|
201 fun pdec where |
|
202 "pdec m = (pdecode1 m, pdecode2 m)" |
|
203 |
|
204 lemma q1: "penc (pdec m) = m" |
|
205 apply(simp only: penc.simps pdec.simps) |
|
206 apply(rule yy) |
|
207 done |
|
208 |
|
209 lemma q2: "pdec (penc m) = m" |
|
210 apply(simp only: penc.simps pdec.simps) |
|
211 apply(case_tac m) |
|
212 apply(simp only: penc.simps pdec.simps) |
|
213 apply(subst y1) |
|
214 apply(subst y2) |
|
215 apply(simp) |
|
216 done |
|
217 |
|
218 lemma inj_penc: "inj_on penc A" |
|
219 apply(rule inj_on_inverseI) |
|
220 apply(rule q2) |
|
221 done |
|
222 |
|
223 lemma inj_pdec: "inj_on pdec A" |
|
224 apply(rule inj_on_inverseI) |
|
225 apply(rule q1) |
|
226 done |
|
227 |
|
228 lemma surj_penc: "surj penc" |
|
229 apply(rule surjI) |
|
230 apply(rule q1) |
|
231 done |
|
232 |
|
233 lemma surj_pdec: "surj pdec" |
|
234 apply(rule surjI) |
|
235 apply(rule q2) |
|
236 done |
|
237 |
|
238 lemma |
|
239 "bij pdec" |
|
240 by(simp add: bij_def surj_pdec inj_pdec) |
|
241 |
|
242 lemma |
|
243 "bij penc" |
|
244 by(simp add: bij_def surj_penc inj_penc) |
|
245 |
|
246 lemma "a \<le> penc (a, 0)" |
|
247 apply(induct a) |
|
248 apply(simp) |
|
249 apply(simp) |
|
250 by (smt nat_one_le_power) |
|
251 |
|
252 lemma "penc(a, 0) \<le> penc (a, b)" |
|
253 apply(simp) |
|
254 by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute) |
|
255 |
|
256 lemma "b \<le> penc (a, b)" |
|
257 apply(simp) |
|
258 proof - |
|
259 have f1: "(1\<Colon>nat) + 1 = 2" |
|
260 by (metis mult_2 nat_mult_1_right) |
|
261 have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2" |
|
262 by (metis mult_le_mono2 nat_mult_1_right) |
|
263 have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1" |
|
264 by (metis le_add1 le_trans nat_add_left_cancel_le) |
|
265 hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1" |
|
266 using f2 by (metis le_add1 le_trans one_le_power) |
|
267 hence "b \<le> 2 ^ a * (b + b + 1) - 1" |
|
268 using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute) |
|
269 thus "b \<le> 2 ^ a * (2 * b + 1) - 1" |
|
270 by (metis mult_2) |
|
271 qed |
|
272 |
|
273 |
|
274 end |
|