9 imports Int Inductive |
9 imports Int Inductive |
10 begin |
10 begin |
11 |
11 |
12 subsection {* The @{text num} type *} |
12 subsection {* The @{text num} type *} |
13 |
13 |
14 text {* |
14 datatype num = One | Dig0 num | Dig1 num |
15 We construct @{text num} as a copy of strictly positive |
15 |
|
16 text {* Increment function for type @{typ num} *} |
|
17 |
|
18 primrec |
|
19 inc :: "num \<Rightarrow> num" |
|
20 where |
|
21 "inc One = Dig0 One" |
|
22 | "inc (Dig0 x) = Dig1 x" |
|
23 | "inc (Dig1 x) = Dig0 (inc x)" |
|
24 |
|
25 text {* Converting between type @{typ num} and type @{typ nat} *} |
|
26 |
|
27 primrec |
|
28 nat_of_num :: "num \<Rightarrow> nat" |
|
29 where |
|
30 "nat_of_num One = Suc 0" |
|
31 | "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x" |
|
32 | "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)" |
|
33 |
|
34 primrec |
|
35 num_of_nat :: "nat \<Rightarrow> num" |
|
36 where |
|
37 "num_of_nat 0 = One" |
|
38 | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" |
|
39 |
|
40 lemma nat_of_num_gt_0: "0 < nat_of_num x" |
|
41 by (induct x) simp_all |
|
42 |
|
43 lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0" |
|
44 by (induct x) simp_all |
|
45 |
|
46 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)" |
|
47 by (induct x) simp_all |
|
48 |
|
49 lemma num_of_nat_double: |
|
50 "0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)" |
|
51 by (induct n) simp_all |
|
52 |
|
53 text {* |
|
54 Type @{typ num} is isomorphic to the strictly positive |
16 natural numbers. |
55 natural numbers. |
17 *} |
56 *} |
18 |
57 |
19 typedef (open) num = "\<lambda>n\<Colon>nat. n > 0" |
58 lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" |
20 morphisms nat_of_num num_of_nat_abs |
59 by (induct x) (simp_all add: num_of_nat_double nat_of_num_gt_0) |
21 by (auto simp add: mem_def) |
60 |
22 |
61 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
23 text {* |
62 by (induct n) (simp_all add: nat_of_num_inc) |
24 A totalized abstraction function. It is not entirely clear |
|
25 whether this is really useful. |
|
26 *} |
|
27 |
|
28 definition num_of_nat :: "nat \<Rightarrow> num" where |
|
29 "num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)" |
|
30 |
|
31 lemma num_cases [case_names nat, cases type: num]: |
|
32 assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)" |
|
33 shows P |
|
34 apply (rule num_of_nat_abs_cases) |
|
35 apply (unfold mem_def) |
|
36 using assms unfolding num_of_nat_def |
|
37 apply auto |
|
38 done |
|
39 |
|
40 lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1" |
|
41 by (simp add: num_of_nat_def) |
|
42 |
|
43 lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)" |
|
44 apply (simp add: num_of_nat_def) |
|
45 apply (subst num_of_nat_abs_inverse) |
|
46 apply (auto simp add: mem_def num_of_nat_abs_inverse) |
|
47 done |
|
48 |
|
49 lemma num_of_nat_inject: |
|
50 "num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)" |
|
51 by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def]) |
|
52 |
|
53 lemma nat_of_num_gt_0: "0 < nat_of_num x" |
|
54 using nat_of_num [of x, unfolded mem_def] . |
|
55 |
63 |
56 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" |
64 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y" |
57 apply safe |
65 apply safe |
58 apply (drule arg_cong [where f=num_of_nat_abs]) |
66 apply (drule arg_cong [where f=num_of_nat]) |
59 apply (simp add: nat_of_num_inverse) |
67 apply (simp add: nat_of_num_inverse) |
60 done |
68 done |
61 |
69 |
62 |
|
63 lemma split_num_all: |
|
64 "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))" |
|
65 proof |
|
66 fix n |
|
67 assume "\<And>m\<Colon>num. PROP P m" |
|
68 then show "PROP P (num_of_nat n)" . |
|
69 next |
|
70 fix m |
|
71 have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0" |
|
72 using nat_of_num by (auto simp add: mem_def) |
|
73 have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m" |
|
74 by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num) |
|
75 assume "\<And>n. PROP P (num_of_nat n)" |
|
76 then have "PROP P (num_of_nat (nat_of_num m))" . |
|
77 then show "PROP P m" unfolding nat_of_num_inverse . |
|
78 qed |
|
79 |
|
80 |
|
81 subsection {* Digit representation for @{typ num} *} |
|
82 |
|
83 instantiation num :: "semiring" |
70 instantiation num :: "semiring" |
84 begin |
71 begin |
85 |
|
86 definition One :: num where |
|
87 one_num_def [code del]: "One = num_of_nat 1" |
|
88 |
72 |
89 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
73 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
90 [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)" |
74 [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)" |
91 |
75 |
92 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
76 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where |
93 [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)" |
77 [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)" |
94 |
78 |
95 definition Dig0 :: "num \<Rightarrow> num" where |
79 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" |
96 [code del]: "Dig0 n = n + n" |
80 unfolding plus_num_def |
97 |
81 by (intro num_of_nat_inverse add_pos_pos nat_of_num_gt_0) |
98 definition Dig1 :: "num \<Rightarrow> num" where |
82 |
99 [code del]: "Dig1 n = n + n + One" |
83 lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y" |
|
84 unfolding times_num_def |
|
85 by (intro num_of_nat_inverse mult_pos_pos nat_of_num_gt_0) |
100 |
86 |
101 instance proof |
87 instance proof |
102 qed (simp_all add: one_num_def plus_num_def times_num_def |
88 qed (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult nat_distrib) |
103 split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib) |
89 |
104 |
90 end |
105 end |
91 |
106 |
92 lemma num_induct [case_names One inc]: |
107 text {* |
93 fixes P :: "num \<Rightarrow> bool" |
108 The following proofs seem horribly complicated. |
94 assumes One: "P One" |
109 Any room for simplification!? |
95 and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
110 *} |
96 shows "P x" |
111 |
97 proof - |
112 lemma nat_dig_cases [case_names 0 1 dig0 dig1]: |
98 obtain n where n: "Suc n = nat_of_num x" |
113 fixes n :: nat |
99 by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0) |
114 assumes "n = 0 \<Longrightarrow> P" |
100 have "P (num_of_nat (Suc n))" |
115 and "n = 1 \<Longrightarrow> P" |
101 proof (induct n) |
116 and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P" |
102 case 0 show ?case using One by simp |
117 and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P" |
|
118 shows P |
|
119 using assms proof (induct n) |
|
120 case 0 then show ?case by simp |
|
121 next |
|
122 case (Suc n) |
|
123 show P proof (rule Suc.hyps) |
|
124 assume "n = 0" |
|
125 then have "Suc n = 1" by simp |
|
126 then show P by (rule Suc.prems(2)) |
|
127 next |
103 next |
128 assume "n = 1" |
104 case (Suc n) |
129 have "1 > (0\<Colon>nat)" by simp |
105 then have "P (inc (num_of_nat (Suc n)))" by (rule inc) |
130 moreover from `n = 1` have "Suc n = 1 + 1" by simp |
106 then show "P (num_of_nat (Suc (Suc n)))" by simp |
131 ultimately show P by (rule Suc.prems(3)) |
|
132 next |
|
133 fix m |
|
134 assume "0 < m" and "n = m + m" |
|
135 note `0 < m` |
|
136 moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp |
|
137 ultimately show P by (rule Suc.prems(4)) |
|
138 next |
|
139 fix m |
|
140 assume "0 < m" and "n = Suc (m + m)" |
|
141 have "0 < Suc m" by simp |
|
142 moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp |
|
143 ultimately show P by (rule Suc.prems(3)) |
|
144 qed |
107 qed |
145 qed |
108 with n show "P x" |
146 |
109 by (simp add: nat_of_num_inverse) |
147 lemma num_induct_raw: |
|
148 fixes n :: nat |
|
149 assumes not0: "n > 0" |
|
150 assumes "P 1" |
|
151 and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)" |
|
152 and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))" |
|
153 shows "P n" |
|
154 using not0 proof (induct n rule: less_induct) |
|
155 case (less n) |
|
156 show "P n" proof (cases n rule: nat_dig_cases) |
|
157 case 0 then show ?thesis using less by simp |
|
158 next |
|
159 case 1 then show ?thesis using assms by simp |
|
160 next |
|
161 case (dig0 m) |
|
162 then show ?thesis apply simp |
|
163 apply (rule assms(3)) apply assumption |
|
164 apply (rule less) |
|
165 apply simp_all |
|
166 done |
|
167 next |
|
168 case (dig1 m) |
|
169 then show ?thesis apply simp |
|
170 apply (rule assms(4)) apply assumption |
|
171 apply (rule less) |
|
172 apply simp_all |
|
173 done |
|
174 qed |
|
175 qed |
|
176 |
|
177 lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then One else num_of_nat n + One)" |
|
178 by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse) |
|
179 |
|
180 lemma num_induct [case_names 1 Suc, induct type: num]: |
|
181 fixes P :: "num \<Rightarrow> bool" |
|
182 assumes 1: "P One" |
|
183 and Suc: "\<And>n. P n \<Longrightarrow> P (n + One)" |
|
184 shows "P n" |
|
185 proof (cases n) |
|
186 case (nat m) then show ?thesis by (induct m arbitrary: n) |
|
187 (auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm) |
|
188 qed |
|
189 |
|
190 rep_datatype One Dig0 Dig1 proof - |
|
191 fix P m |
|
192 assume 1: "P One" |
|
193 and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)" |
|
194 and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)" |
|
195 obtain n where "0 < n" and m: "m = num_of_nat n" |
|
196 by (cases m) auto |
|
197 from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw) |
|
198 case 1 from `0 < n` show ?case . |
|
199 next |
|
200 case 2 with 1 show ?case by (simp add: one_num_def) |
|
201 next |
|
202 case (3 n) then have "P (num_of_nat n)" by auto |
|
203 then have "P (Dig0 (num_of_nat n))" by (rule Dig0) |
|
204 with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse) |
|
205 next |
|
206 case (4 n) then have "P (num_of_nat n)" by auto |
|
207 then have "P (Dig1 (num_of_nat n))" by (rule Dig1) |
|
208 with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse) |
|
209 qed |
|
210 with m show "P m" by simp |
|
211 next |
|
212 fix m n |
|
213 show "Dig0 m = Dig0 n \<longleftrightarrow> m = n" |
|
214 apply (cases m) apply (cases n) |
|
215 by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject) |
|
216 next |
|
217 fix m n |
|
218 show "Dig1 m = Dig1 n \<longleftrightarrow> m = n" |
|
219 apply (cases m) apply (cases n) |
|
220 by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject) |
|
221 next |
|
222 fix n |
|
223 show "One \<noteq> Dig0 n" |
|
224 apply (cases n) |
|
225 by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject) |
|
226 next |
|
227 fix n |
|
228 show "One \<noteq> Dig1 n" |
|
229 apply (cases n) |
|
230 by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject) |
|
231 next |
|
232 fix m n |
|
233 have "\<And>n m. n + n \<noteq> Suc (m + m)" |
|
234 proof - |
|
235 fix n m |
|
236 show "n + n \<noteq> Suc (m + m)" |
|
237 proof (induct m arbitrary: n) |
|
238 case 0 then show ?case by (cases n) simp_all |
|
239 next |
|
240 case (Suc m) then show ?case by (cases n) simp_all |
|
241 qed |
|
242 qed |
|
243 then show "Dig0 n \<noteq> Dig1 m" |
|
244 apply (cases n) apply (cases m) |
|
245 by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject) |
|
246 qed |
110 qed |
247 |
111 |
248 text {* |
112 text {* |
249 From now on, there are two possible models for @{typ num}: |
113 From now on, there are two possible models for @{typ num}: |
250 as positive naturals (rules @{text "num_induct"}, @{text "num_cases"}) |
114 as positive naturals (rule @{text "num_induct"}) |
251 and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}). |
115 and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}). |
252 |
116 |
253 It is not entirely clear in which context it is better to use |
117 It is not entirely clear in which context it is better to use |
254 the one or the other, or whether the construction should be reversed. |
118 the one or the other, or whether the construction should be reversed. |
255 *} |
119 *} |
352 |
219 |
353 text {* |
220 text {* |
354 First, addition and multiplication on digits. |
221 First, addition and multiplication on digits. |
355 *} |
222 *} |
356 |
223 |
357 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" |
|
358 unfolding plus_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0) |
|
359 |
|
360 lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y" |
|
361 unfolding times_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0) |
|
362 |
|
363 lemma nat_of_num_One: "nat_of_num One = 1" |
|
364 unfolding one_num_def by (simp add: num_of_nat_inverse) |
|
365 |
|
366 lemma nat_of_num_Dig0: "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x" |
|
367 unfolding Dig0_def by (simp add: nat_of_num_add) |
|
368 |
|
369 lemma nat_of_num_Dig1: "nat_of_num (Dig1 x) = nat_of_num x + nat_of_num x + 1" |
|
370 unfolding Dig1_def by (simp add: nat_of_num_add nat_of_num_One) |
|
371 |
|
372 lemmas nat_of_num_simps = |
|
373 nat_of_num_One nat_of_num_Dig0 nat_of_num_Dig1 |
|
374 nat_of_num_add nat_of_num_mult |
|
375 |
|
376 lemma Dig_plus [numeral, simp, code]: |
224 lemma Dig_plus [numeral, simp, code]: |
377 "One + One = Dig0 One" |
225 "One + One = Dig0 One" |
378 "One + Dig0 m = Dig1 m" |
226 "One + Dig0 m = Dig1 m" |
379 "One + Dig1 m = Dig0 (m + One)" |
227 "One + Dig1 m = Dig0 (m + One)" |
380 "Dig0 n + One = Dig1 n" |
228 "Dig0 n + One = Dig1 n" |
381 "Dig0 n + Dig0 m = Dig0 (n + m)" |
229 "Dig0 n + Dig0 m = Dig0 (n + m)" |
382 "Dig0 n + Dig1 m = Dig1 (n + m)" |
230 "Dig0 n + Dig1 m = Dig1 (n + m)" |
383 "Dig1 n + One = Dig0 (n + One)" |
231 "Dig1 n + One = Dig0 (n + One)" |
384 "Dig1 n + Dig0 m = Dig1 (n + m)" |
232 "Dig1 n + Dig0 m = Dig1 (n + m)" |
385 "Dig1 n + Dig1 m = Dig0 (n + m + One)" |
233 "Dig1 n + Dig1 m = Dig0 (n + m + One)" |
386 by (simp_all add: num_eq_iff nat_of_num_simps) |
234 by (simp_all add: num_eq_iff nat_of_num_add) |
387 |
235 |
388 lemma Dig_times [numeral, simp, code]: |
236 lemma Dig_times [numeral, simp, code]: |
389 "One * One = One" |
237 "One * One = One" |
390 "One * Dig0 n = Dig0 n" |
238 "One * Dig0 n = Dig0 n" |
391 "One * Dig1 n = Dig1 n" |
239 "One * Dig1 n = Dig1 n" |
415 blow-up. But it could be worth the effort. |
264 blow-up. But it could be worth the effort. |
416 *} |
265 *} |
417 |
266 |
418 lemma of_num_plus_one [numeral]: |
267 lemma of_num_plus_one [numeral]: |
419 "of_num n + 1 = of_num (n + One)" |
268 "of_num n + 1 = of_num (n + One)" |
420 by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac) |
269 by (rule sym, induct n) (simp_all add: of_num.simps add_ac) |
421 |
270 |
422 lemma of_num_one_plus [numeral]: |
271 lemma of_num_one_plus [numeral]: |
423 "1 + of_num n = of_num (n + One)" |
272 "1 + of_num n = of_num (n + One)" |
424 unfolding of_num_plus_one [symmetric] add_commute .. |
273 unfolding of_num_plus_one [symmetric] add_commute .. |
425 |
274 |
|
275 text {* Rules for addition in the One/inc view *} |
|
276 |
|
277 lemma add_One: "x + One = inc x" |
|
278 by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
|
279 |
|
280 lemma add_inc: "x + inc y = inc (x + y)" |
|
281 by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
|
282 |
|
283 text {* Rules for multiplication in the One/inc view *} |
|
284 |
|
285 lemma mult_One: "x * One = x" |
|
286 by (simp add: num_eq_iff nat_of_num_mult) |
|
287 |
|
288 lemma mult_inc: "x * inc y = x * y + x" |
|
289 by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) |
|
290 |
426 lemma of_num_plus [numeral]: |
291 lemma of_num_plus [numeral]: |
427 "of_num m + of_num n = of_num (m + n)" |
292 "of_num m + of_num n = of_num (m + n)" |
428 by (induct n rule: num_induct) |
293 by (induct n rule: num_induct) |
429 (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m] |
294 (simp_all add: add_One add_inc of_num_one of_num_inc add_ac) |
430 add_ac of_num_plus_one [symmetric]) |
|
431 |
295 |
432 lemma of_num_times_one [numeral]: |
296 lemma of_num_times_one [numeral]: |
433 "of_num n * 1 = of_num n" |
297 "of_num n * 1 = of_num n" |
434 by simp |
298 by simp |
435 |
299 |
436 lemma of_num_one_times [numeral]: |
300 lemma of_num_one_times [numeral]: |
437 "1 * of_num n = of_num n" |
301 "1 * of_num n = of_num n" |
438 by simp |
302 by simp |
439 |
303 |
440 lemma times_One [simp]: "m * One = m" |
|
441 by (simp add: num_eq_iff nat_of_num_simps) |
|
442 |
|
443 lemma of_num_times [numeral]: |
304 lemma of_num_times [numeral]: |
444 "of_num m * of_num n = of_num (m * n)" |
305 "of_num m * of_num n = of_num (m * n)" |
445 by (induct n rule: num_induct) |
306 by (induct n rule: num_induct) |
446 (simp_all add: of_num_plus [symmetric] |
307 (simp_all add: of_num_plus [symmetric] mult_One mult_inc |
447 semiring_class.right_distrib right_distrib of_num_one) |
308 semiring_class.right_distrib right_distrib of_num_one of_num_inc) |
448 |
309 |
449 end |
310 end |
450 |
311 |
451 text {* |
312 text {* |
452 Structures with a @{term 0}. |
313 Structures with a @{term 0}. |