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