|
1 theory Recs |
|
2 imports Main Fact |
|
3 "~~/src/HOL/Number_Theory/Primes" |
|
4 "~~/src/HOL/Library/Nat_Bijection" |
|
5 "~~/src/HOL/Library/Discrete" |
|
6 begin |
|
7 |
|
8 declare One_nat_def[simp del] |
|
9 |
|
10 (* |
|
11 some definitions from |
|
12 |
|
13 A Course in Formal Languages, Automata and Groups |
|
14 I M Chiswell |
|
15 |
|
16 and |
|
17 |
|
18 Lecture on undecidability |
|
19 Michael M. Wolf |
|
20 *) |
|
21 |
|
22 lemma if_zero_one [simp]: |
|
23 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
|
24 "(0::nat) < (if P then 1 else 0) = P" |
|
25 "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))" |
|
26 by (simp_all) |
|
27 |
|
28 lemma nth: |
|
29 "(x # xs) ! 0 = x" |
|
30 "(x # y # xs) ! 1 = y" |
|
31 "(x # y # z # xs) ! 2 = z" |
|
32 "(x # y # z # u # xs) ! 3 = u" |
|
33 by (simp_all) |
|
34 |
|
35 |
|
36 section {* Some auxiliary lemmas about @{text "\<Sum>"} and @{text "\<Prod>"} *} |
|
37 |
|
38 lemma setprod_atMost_Suc[simp]: |
|
39 "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)" |
|
40 by(simp add:atMost_Suc mult_ac) |
|
41 |
|
42 lemma setprod_lessThan_Suc[simp]: |
|
43 "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
|
44 by (simp add:lessThan_Suc mult_ac) |
|
45 |
|
46 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
|
47 setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}" |
|
48 apply(subst setsum_Un_disjoint[symmetric]) |
|
49 apply(auto simp add: ivl_disj_un_one) |
|
50 done |
|
51 |
|
52 lemma setsum_eq_zero [simp]: |
|
53 fixes f::"nat \<Rightarrow> nat" |
|
54 shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" |
|
55 "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" |
|
56 by (auto) |
|
57 |
|
58 lemma setprod_eq_zero [simp]: |
|
59 fixes f::"nat \<Rightarrow> nat" |
|
60 shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)" |
|
61 "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" |
|
62 by (auto) |
|
63 |
|
64 lemma setsum_one_less: |
|
65 fixes n::nat |
|
66 assumes "\<forall>i < n. f i \<le> 1" |
|
67 shows "(\<Sum>i < n. f i) \<le> n" |
|
68 using assms |
|
69 by (induct n) (auto) |
|
70 |
|
71 lemma setsum_one_le: |
|
72 fixes n::nat |
|
73 assumes "\<forall>i \<le> n. f i \<le> 1" |
|
74 shows "(\<Sum>i \<le> n. f i) \<le> Suc n" |
|
75 using assms |
|
76 by (induct n) (auto) |
|
77 |
|
78 lemma setsum_eq_one_le: |
|
79 fixes n::nat |
|
80 assumes "\<forall>i \<le> n. f i = 1" |
|
81 shows "(\<Sum>i \<le> n. f i) = Suc n" |
|
82 using assms |
|
83 by (induct n) (auto) |
|
84 |
|
85 lemma setsum_least_eq: |
|
86 fixes f::"nat \<Rightarrow> nat" |
|
87 assumes h0: "p \<le> n" |
|
88 assumes h1: "\<forall>i \<in> {..<p}. f i = 1" |
|
89 assumes h2: "\<forall>i \<in> {p..n}. f i = 0" |
|
90 shows "(\<Sum>i \<le> n. f i) = p" |
|
91 proof - |
|
92 have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" |
|
93 using h1 by (induct p) (simp_all) |
|
94 have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" |
|
95 using h2 by auto |
|
96 have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)" |
|
97 using h0 by (simp add: setsum_add_nat_ivl2) |
|
98 also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp |
|
99 finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp |
|
100 qed |
|
101 |
|
102 lemma nat_mult_le_one: |
|
103 fixes m n::nat |
|
104 assumes "m \<le> 1" "n \<le> 1" |
|
105 shows "m * n \<le> 1" |
|
106 using assms by (induct n) (auto) |
|
107 |
|
108 lemma setprod_one_le: |
|
109 fixes f::"nat \<Rightarrow> nat" |
|
110 assumes "\<forall>i \<le> n. f i \<le> 1" |
|
111 shows "(\<Prod>i \<le> n. f i) \<le> 1" |
|
112 using assms |
|
113 by (induct n) (auto intro: nat_mult_le_one) |
|
114 |
|
115 lemma setprod_greater_zero: |
|
116 fixes f::"nat \<Rightarrow> nat" |
|
117 assumes "\<forall>i \<le> n. f i \<ge> 0" |
|
118 shows "(\<Prod>i \<le> n. f i) \<ge> 0" |
|
119 using assms by (induct n) (auto) |
|
120 |
|
121 lemma setprod_eq_one: |
|
122 fixes f::"nat \<Rightarrow> nat" |
|
123 assumes "\<forall>i \<le> n. f i = Suc 0" |
|
124 shows "(\<Prod>i \<le> n. f i) = Suc 0" |
|
125 using assms by (induct n) (auto) |
|
126 |
|
127 lemma setsum_cut_off_less: |
|
128 fixes f::"nat \<Rightarrow> nat" |
|
129 assumes h1: "m \<le> n" |
|
130 and h2: "\<forall>i \<in> {m..<n}. f i = 0" |
|
131 shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" |
|
132 proof - |
|
133 have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" |
|
134 using h2 by auto |
|
135 have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)" |
|
136 using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) |
|
137 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
|
138 finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp |
|
139 qed |
|
140 |
|
141 lemma setsum_cut_off_le: |
|
142 fixes f::"nat \<Rightarrow> nat" |
|
143 assumes h1: "m \<le> n" |
|
144 and h2: "\<forall>i \<in> {m..n}. f i = 0" |
|
145 shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" |
|
146 proof - |
|
147 have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" |
|
148 using h2 by auto |
|
149 have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)" |
|
150 using h1 by (simp add: setsum_add_nat_ivl2) |
|
151 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
|
152 finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp |
|
153 qed |
|
154 |
|
155 lemma setprod_one [simp]: |
|
156 fixes n::nat |
|
157 shows "(\<Prod>i < n. Suc 0) = Suc 0" |
|
158 "(\<Prod>i \<le> n. Suc 0) = Suc 0" |
|
159 by (induct n) (simp_all) |
|
160 |
|
161 |
|
162 |
|
163 section {* Recursive Functions *} |
|
164 |
|
165 datatype recf = Z |
|
166 | S |
|
167 | Id nat nat |
|
168 | Cn nat recf "recf list" |
|
169 | Pr nat recf recf |
|
170 | Mn nat recf |
|
171 |
|
172 fun arity :: "recf \<Rightarrow> nat" |
|
173 where |
|
174 "arity Z = 1" |
|
175 | "arity S = 1" |
|
176 | "arity (Id m n) = m" |
|
177 | "arity (Cn n f gs) = n" |
|
178 | "arity (Pr n f g) = Suc n" |
|
179 | "arity (Mn n f) = n" |
|
180 |
|
181 text {* Abbreviations for calculating the arity of the constructors *} |
|
182 |
|
183 abbreviation |
|
184 "CN f gs \<equiv> Cn (arity (hd gs)) f gs" |
|
185 |
|
186 abbreviation |
|
187 "PR f g \<equiv> Pr (arity f) f g" |
|
188 |
|
189 abbreviation |
|
190 "MN f \<equiv> Mn (arity f - 1) f" |
|
191 |
|
192 text {* the evaluation function and termination relation *} |
|
193 |
|
194 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
|
195 where |
|
196 "rec_eval Z xs = 0" |
|
197 | "rec_eval S xs = Suc (xs ! 0)" |
|
198 | "rec_eval (Id m n) xs = xs ! n" |
|
199 | "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" |
|
200 | "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs" |
|
201 | "rec_eval (Pr n f g) (Suc x # xs) = |
|
202 rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)" |
|
203 | "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)" |
|
204 |
|
205 inductive |
|
206 terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
|
207 where |
|
208 termi_z: "terminates Z [n]" |
|
209 | termi_s: "terminates S [n]" |
|
210 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (Id m n) xs" |
|
211 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); |
|
212 \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs" |
|
213 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs)); |
|
214 terminates f xs; |
|
215 length xs = n\<rbrakk> |
|
216 \<Longrightarrow> terminates (Pr n f g) (x # xs)" |
|
217 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); |
|
218 rec_eval f (r # xs) = 0; |
|
219 \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs" |
|
220 |
|
221 |
|
222 section {* Arithmetic Functions *} |
|
223 |
|
224 text {* |
|
225 @{text "constn n"} is the recursive function which computes |
|
226 natural number @{text "n"}. |
|
227 *} |
|
228 fun constn :: "nat \<Rightarrow> recf" |
|
229 where |
|
230 "constn 0 = Z" | |
|
231 "constn (Suc n) = CN S [constn n]" |
|
232 |
|
233 definition |
|
234 "rec_swap f = CN f [Id 2 1, Id 2 0]" |
|
235 |
|
236 definition |
|
237 "rec_add = PR (Id 1 0) (CN S [Id 3 1])" |
|
238 |
|
239 definition |
|
240 "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])" |
|
241 |
|
242 definition |
|
243 "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))" |
|
244 |
|
245 definition |
|
246 "rec_fact_aux = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])" |
|
247 |
|
248 definition |
|
249 "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]" |
|
250 |
|
251 definition |
|
252 "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
|
253 |
|
254 definition |
|
255 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))" |
|
256 |
|
257 lemma constn_lemma [simp]: |
|
258 "rec_eval (constn n) xs = n" |
|
259 by (induct n) (simp_all) |
|
260 |
|
261 lemma swap_lemma [simp]: |
|
262 "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]" |
|
263 by (simp add: rec_swap_def) |
|
264 |
|
265 lemma add_lemma [simp]: |
|
266 "rec_eval rec_add [x, y] = x + y" |
|
267 by (induct x) (simp_all add: rec_add_def) |
|
268 |
|
269 lemma mult_lemma [simp]: |
|
270 "rec_eval rec_mult [x, y] = x * y" |
|
271 by (induct x) (simp_all add: rec_mult_def) |
|
272 |
|
273 lemma power_lemma [simp]: |
|
274 "rec_eval rec_power [x, y] = x ^ y" |
|
275 by (induct y) (simp_all add: rec_power_def) |
|
276 |
|
277 lemma fact_aux_lemma [simp]: |
|
278 "rec_eval rec_fact_aux [x, y] = fact x" |
|
279 by (induct x) (simp_all add: rec_fact_aux_def) |
|
280 |
|
281 lemma fact_lemma [simp]: |
|
282 "rec_eval rec_fact [x] = fact x" |
|
283 by (simp add: rec_fact_def) |
|
284 |
|
285 lemma pred_lemma [simp]: |
|
286 "rec_eval rec_pred [x] = x - 1" |
|
287 by (induct x) (simp_all add: rec_pred_def) |
|
288 |
|
289 lemma minus_lemma [simp]: |
|
290 "rec_eval rec_minus [x, y] = x - y" |
|
291 by (induct y) (simp_all add: rec_minus_def) |
|
292 |
|
293 |
|
294 section {* Logical functions *} |
|
295 |
|
296 text {* |
|
297 The @{text "sign"} function returns 1 when the input argument |
|
298 is greater than @{text "0"}. *} |
|
299 |
|
300 definition |
|
301 "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]" |
|
302 |
|
303 definition |
|
304 "rec_not = CN rec_minus [constn 1, Id 1 0]" |
|
305 |
|
306 text {* |
|
307 @{text "rec_eq"} compares two arguments: returns @{text "1"} |
|
308 if they are equal; @{text "0"} otherwise. *} |
|
309 definition |
|
310 "rec_eq = CN rec_minus [CN (constn 1) [Id 2 0], CN rec_add [rec_minus, rec_swap rec_minus]]" |
|
311 |
|
312 definition |
|
313 "rec_noteq = CN rec_not [rec_eq]" |
|
314 |
|
315 definition |
|
316 "rec_conj = CN rec_sign [rec_mult]" |
|
317 |
|
318 definition |
|
319 "rec_disj = CN rec_sign [rec_add]" |
|
320 |
|
321 definition |
|
322 "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]" |
|
323 |
|
324 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero, |
|
325 y otherwise; @{term "rec_if [z, x, y]"} returns x if z is *not* |
|
326 zero, y otherwise *} |
|
327 |
|
328 definition |
|
329 "rec_ifz = PR (Id 2 0) (Id 4 3)" |
|
330 |
|
331 definition |
|
332 "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]" |
|
333 |
|
334 |
|
335 lemma sign_lemma [simp]: |
|
336 "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)" |
|
337 by (simp add: rec_sign_def) |
|
338 |
|
339 lemma not_lemma [simp]: |
|
340 "rec_eval rec_not [x] = (if x = 0 then 1 else 0)" |
|
341 by (simp add: rec_not_def) |
|
342 |
|
343 lemma eq_lemma [simp]: |
|
344 "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)" |
|
345 by (simp add: rec_eq_def) |
|
346 |
|
347 lemma noteq_lemma [simp]: |
|
348 "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)" |
|
349 by (simp add: rec_noteq_def) |
|
350 |
|
351 lemma conj_lemma [simp]: |
|
352 "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)" |
|
353 by (simp add: rec_conj_def) |
|
354 |
|
355 lemma disj_lemma [simp]: |
|
356 "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
357 by (simp add: rec_disj_def) |
|
358 |
|
359 lemma imp_lemma [simp]: |
|
360 "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)" |
|
361 by (simp add: rec_imp_def) |
|
362 |
|
363 lemma ifz_lemma [simp]: |
|
364 "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" |
|
365 by (case_tac z) (simp_all add: rec_ifz_def) |
|
366 |
|
367 lemma if_lemma [simp]: |
|
368 "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" |
|
369 by (simp add: rec_if_def) |
|
370 |
|
371 section {* Less and Le Relations *} |
|
372 |
|
373 text {* |
|
374 @{text "rec_less"} compares two arguments and returns @{text "1"} if |
|
375 the first is less than the second; otherwise returns @{text "0"}. *} |
|
376 |
|
377 definition |
|
378 "rec_less = CN rec_sign [rec_swap rec_minus]" |
|
379 |
|
380 definition |
|
381 "rec_le = CN rec_disj [rec_less, rec_eq]" |
|
382 |
|
383 lemma less_lemma [simp]: |
|
384 "rec_eval rec_less [x, y] = (if x < y then 1 else 0)" |
|
385 by (simp add: rec_less_def) |
|
386 |
|
387 lemma le_lemma [simp]: |
|
388 "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)" |
|
389 by(simp add: rec_le_def) |
|
390 |
|
391 |
|
392 section {* Summation and Product Functions *} |
|
393 |
|
394 definition |
|
395 "rec_sigma1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) |
|
396 (CN rec_add [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])" |
|
397 |
|
398 definition |
|
399 "rec_sigma2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) |
|
400 (CN rec_add [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])" |
|
401 |
|
402 definition |
|
403 "rec_accum1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) |
|
404 (CN rec_mult [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])" |
|
405 |
|
406 definition |
|
407 "rec_accum2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) |
|
408 (CN rec_mult [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])" |
|
409 |
|
410 definition |
|
411 "rec_accum3 f = PR (CN f [CN Z [Id 3 0], Id 3 0, Id 3 1, Id 3 2]) |
|
412 (CN rec_mult [Id 5 1, CN f [CN S [Id 5 0], Id 5 2, Id 5 3, Id 5 4]])" |
|
413 |
|
414 |
|
415 lemma sigma1_lemma [simp]: |
|
416 shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])" |
|
417 by (induct x) (simp_all add: rec_sigma1_def) |
|
418 |
|
419 lemma sigma2_lemma [simp]: |
|
420 shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f [z, y1, y2])" |
|
421 by (induct x) (simp_all add: rec_sigma2_def) |
|
422 |
|
423 lemma accum1_lemma [simp]: |
|
424 shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f [z, y])" |
|
425 by (induct x) (simp_all add: rec_accum1_def) |
|
426 |
|
427 lemma accum2_lemma [simp]: |
|
428 shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f [z, y1, y2])" |
|
429 by (induct x) (simp_all add: rec_accum2_def) |
|
430 |
|
431 lemma accum3_lemma [simp]: |
|
432 shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2, y3])" |
|
433 by (induct x) (simp_all add: rec_accum3_def) |
|
434 |
|
435 |
|
436 section {* Bounded Quantifiers *} |
|
437 |
|
438 definition |
|
439 "rec_all1 f = CN rec_sign [rec_accum1 f]" |
|
440 |
|
441 definition |
|
442 "rec_all2 f = CN rec_sign [rec_accum2 f]" |
|
443 |
|
444 definition |
|
445 "rec_all3 f = CN rec_sign [rec_accum3 f]" |
|
446 |
|
447 definition |
|
448 "rec_all1_less f = (let cond1 = CN rec_eq [Id 3 0, Id 3 1] in |
|
449 let cond2 = CN f [Id 3 0, Id 3 2] |
|
450 in CN (rec_all2 (CN rec_disj [cond1, cond2])) [Id 2 0, Id 2 0, Id 2 1])" |
|
451 |
|
452 definition |
|
453 "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in |
|
454 let cond2 = CN f [Id 4 0, Id 4 2, Id 4 3] in |
|
455 CN (rec_all3 (CN rec_disj [cond1, cond2])) [Id 3 0, Id 3 0, Id 3 1, Id 3 2])" |
|
456 |
|
457 definition |
|
458 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
|
459 |
|
460 definition |
|
461 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
|
462 |
|
463 |
|
464 lemma ex1_lemma [simp]: |
|
465 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
466 by (simp add: rec_ex1_def) |
|
467 |
|
468 lemma ex2_lemma [simp]: |
|
469 "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
470 by (simp add: rec_ex2_def) |
|
471 |
|
472 lemma all1_lemma [simp]: |
|
473 "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
474 by (simp add: rec_all1_def) |
|
475 |
|
476 lemma all2_lemma [simp]: |
|
477 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
478 by (simp add: rec_all2_def) |
|
479 |
|
480 lemma all3_lemma [simp]: |
|
481 "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)" |
|
482 by (simp add: rec_all3_def) |
|
483 |
|
484 lemma all1_less_lemma [simp]: |
|
485 "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
486 apply(auto simp add: Let_def rec_all1_less_def) |
|
487 apply (metis nat_less_le)+ |
|
488 done |
|
489 |
|
490 lemma all2_less_lemma [simp]: |
|
491 "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
492 apply(auto simp add: Let_def rec_all2_less_def) |
|
493 apply(metis nat_less_le)+ |
|
494 done |
|
495 |
|
496 section {* Quotients *} |
|
497 |
|
498 definition |
|
499 "rec_quo = (let lhs = CN S [Id 3 0] in |
|
500 let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in |
|
501 let cond = CN rec_eq [lhs, rhs] in |
|
502 let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1] |
|
503 in PR Z if_stmt)" |
|
504 |
|
505 fun Quo where |
|
506 "Quo x 0 = 0" |
|
507 | "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)" |
|
508 |
|
509 lemma Quo0: |
|
510 shows "Quo 0 y = 0" |
|
511 by (induct y) (auto) |
|
512 |
|
513 lemma Quo1: |
|
514 "x * (Quo x y) \<le> y" |
|
515 by (induct y) (simp_all) |
|
516 |
|
517 lemma Quo2: |
|
518 "b * (Quo b a) + a mod b = a" |
|
519 by (induct a) (auto simp add: mod_Suc) |
|
520 |
|
521 lemma Quo3: |
|
522 "n * (Quo n m) = m - m mod n" |
|
523 using Quo2[of n m] by (auto) |
|
524 |
|
525 lemma Quo4: |
|
526 assumes h: "0 < x" |
|
527 shows "y < x + x * Quo x y" |
|
528 proof - |
|
529 have "x - (y mod x) > 0" using mod_less_divisor assms by auto |
|
530 then have "y < y + (x - (y mod x))" by simp |
|
531 then have "y < x + (y - (y mod x))" by simp |
|
532 then show "y < x + x * (Quo x y)" by (simp add: Quo3) |
|
533 qed |
|
534 |
|
535 lemma Quo_div: |
|
536 shows "Quo x y = y div x" |
|
537 apply(case_tac "x = 0") |
|
538 apply(simp add: Quo0) |
|
539 apply(subst split_div_lemma[symmetric]) |
|
540 apply(auto intro: Quo1 Quo4) |
|
541 done |
|
542 |
|
543 lemma Quo_rec_quo: |
|
544 shows "rec_eval rec_quo [y, x] = Quo x y" |
|
545 by (induct y) (simp_all add: rec_quo_def) |
|
546 |
|
547 lemma quo_lemma [simp]: |
|
548 shows "rec_eval rec_quo [y, x] = y div x" |
|
549 by (simp add: Quo_div Quo_rec_quo) |
|
550 |
|
551 |
|
552 section {* Iteration *} |
|
553 |
|
554 definition |
|
555 "rec_iter f = PR (Id 1 0) (CN f [Id 3 1])" |
|
556 |
|
557 fun Iter where |
|
558 "Iter f 0 = id" |
|
559 | "Iter f (Suc n) = f \<circ> (Iter f n)" |
|
560 |
|
561 lemma Iter_comm: |
|
562 "(Iter f n) (f x) = f ((Iter f n) x)" |
|
563 by (induct n) (simp_all) |
|
564 |
|
565 lemma iter_lemma [simp]: |
|
566 "rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x" |
|
567 by (induct n) (simp_all add: rec_iter_def) |
|
568 |
|
569 |
|
570 section {* Bounded Maximisation *} |
|
571 |
|
572 |
|
573 fun BMax_rec where |
|
574 "BMax_rec R 0 = 0" |
|
575 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)" |
|
576 |
|
577 definition |
|
578 BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat" |
|
579 where |
|
580 "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" |
|
581 |
|
582 lemma BMax_rec_eq1: |
|
583 "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)" |
|
584 apply(induct x) |
|
585 apply(auto intro: Greatest_equality Greatest_equality[symmetric]) |
|
586 apply(simp add: le_Suc_eq) |
|
587 by metis |
|
588 |
|
589 lemma BMax_rec_eq2: |
|
590 "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" |
|
591 apply(induct x) |
|
592 apply(auto intro: Max_eqI Max_eqI[symmetric]) |
|
593 apply(simp add: le_Suc_eq) |
|
594 by metis |
|
595 |
|
596 lemma BMax_rec_eq3: |
|
597 "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})" |
|
598 by (simp add: BMax_rec_eq2 Set.filter_def) |
|
599 |
|
600 definition |
|
601 "rec_max1 f = PR Z (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 3 0], Id 3 1])" |
|
602 |
|
603 lemma max1_lemma [simp]: |
|
604 "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x" |
|
605 by (induct x) (simp_all add: rec_max1_def) |
|
606 |
|
607 definition |
|
608 "rec_max2 f = PR Z (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" |
|
609 |
|
610 lemma max2_lemma [simp]: |
|
611 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
|
612 by (induct x) (simp_all add: rec_max2_def) |
|
613 |
|
614 |
|
615 section {* Encodings using Cantor's pairing function *} |
|
616 |
|
617 text {* |
|
618 We use Cantor's pairing function from Nat_Bijection. |
|
619 However, we need to prove that the formulation of the |
|
620 decoding function there is recursive. For this we first |
|
621 prove that we can extract the maximal triangle number |
|
622 using @{term prod_decode}. |
|
623 *} |
|
624 |
|
625 abbreviation Max_triangle_aux where |
|
626 "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)" |
|
627 |
|
628 abbreviation Max_triangle where |
|
629 "Max_triangle z \<equiv> Max_triangle_aux 0 z" |
|
630 |
|
631 abbreviation |
|
632 "pdec1 z \<equiv> fst (prod_decode z)" |
|
633 |
|
634 abbreviation |
|
635 "pdec2 z \<equiv> snd (prod_decode z)" |
|
636 |
|
637 abbreviation |
|
638 "penc m n \<equiv> prod_encode (m, n)" |
|
639 |
|
640 lemma fst_prod_decode: |
|
641 "pdec1 z = z - triangle (Max_triangle z)" |
|
642 by (subst (3) prod_decode_inverse[symmetric]) |
|
643 (simp add: prod_encode_def prod_decode_def split: prod.split) |
|
644 |
|
645 lemma snd_prod_decode: |
|
646 "pdec2 z = Max_triangle z - pdec1 z" |
|
647 by (simp only: prod_decode_def) |
|
648 |
|
649 lemma le_triangle: |
|
650 "m \<le> triangle (n + m)" |
|
651 by (induct_tac m) (simp_all) |
|
652 |
|
653 lemma Max_triangle_triangle_le: |
|
654 "triangle (Max_triangle z) \<le> z" |
|
655 by (subst (9) prod_decode_inverse[symmetric]) |
|
656 (simp add: prod_decode_def prod_encode_def split: prod.split) |
|
657 |
|
658 lemma Max_triangle_le: |
|
659 "Max_triangle z \<le> z" |
|
660 proof - |
|
661 have "Max_triangle z \<le> triangle (Max_triangle z)" |
|
662 using le_triangle[of _ 0, simplified] by simp |
|
663 also have "... \<le> z" by (rule Max_triangle_triangle_le) |
|
664 finally show "Max_triangle z \<le> z" . |
|
665 qed |
|
666 |
|
667 lemma w_aux: |
|
668 "Max_triangle (triangle k + m) = Max_triangle_aux k m" |
|
669 by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add) |
|
670 |
|
671 lemma y_aux: "y \<le> Max_triangle_aux y k" |
|
672 apply(induct k arbitrary: y rule: nat_less_induct) |
|
673 apply(subst (1 2) prod_decode_aux.simps) |
|
674 apply(simp) |
|
675 apply(rule impI) |
|
676 apply(drule_tac x="n - Suc y" in spec) |
|
677 apply(drule mp) |
|
678 apply(auto)[1] |
|
679 apply(drule_tac x="Suc y" in spec) |
|
680 apply(erule Suc_leD) |
|
681 done |
|
682 |
|
683 lemma Max_triangle_greatest: |
|
684 "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)" |
|
685 apply(rule Greatest_equality[symmetric]) |
|
686 apply(rule disjI1) |
|
687 apply(rule conjI) |
|
688 apply(rule Max_triangle_triangle_le) |
|
689 apply(rule Max_triangle_le) |
|
690 apply(erule disjE) |
|
691 apply(erule conjE) |
|
692 apply(subst (asm) (1) le_iff_add) |
|
693 apply(erule exE) |
|
694 apply(clarify) |
|
695 apply(simp only: w_aux) |
|
696 apply(rule y_aux) |
|
697 apply(simp) |
|
698 done |
|
699 |
|
700 |
|
701 definition |
|
702 "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]" |
|
703 |
|
704 definition |
|
705 "rec_max_triangle = |
|
706 (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in |
|
707 CN (rec_max1 cond) [Id 1 0, Id 1 0])" |
|
708 |
|
709 |
|
710 lemma triangle_lemma [simp]: |
|
711 "rec_eval rec_triangle [x] = triangle x" |
|
712 by (simp add: rec_triangle_def triangle_def) |
|
713 |
|
714 lemma max_triangle_lemma [simp]: |
|
715 "rec_eval rec_max_triangle [x] = Max_triangle x" |
|
716 by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) |
|
717 |
|
718 |
|
719 text {* Encodings for Products *} |
|
720 |
|
721 definition |
|
722 "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]" |
|
723 |
|
724 definition |
|
725 "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]" |
|
726 |
|
727 definition |
|
728 "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" |
|
729 |
|
730 lemma pdec1_lemma [simp]: |
|
731 "rec_eval rec_pdec1 [z] = pdec1 z" |
|
732 by (simp add: rec_pdec1_def fst_prod_decode) |
|
733 |
|
734 lemma pdec2_lemma [simp]: |
|
735 "rec_eval rec_pdec2 [z] = pdec2 z" |
|
736 by (simp add: rec_pdec2_def snd_prod_decode) |
|
737 |
|
738 lemma penc_lemma [simp]: |
|
739 "rec_eval rec_penc [m, n] = penc m n" |
|
740 by (simp add: rec_penc_def prod_encode_def) |
|
741 |
|
742 |
|
743 text {* Encodings of Lists *} |
|
744 |
|
745 fun |
|
746 lenc :: "nat list \<Rightarrow> nat" |
|
747 where |
|
748 "lenc [] = 0" |
|
749 | "lenc (x # xs) = penc (Suc x) (lenc xs)" |
|
750 |
|
751 fun |
|
752 ldec :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
753 where |
|
754 "ldec z 0 = (pdec1 z) - 1" |
|
755 | "ldec z (Suc n) = ldec (pdec2 z) n" |
|
756 |
|
757 lemma pdec_zero_simps [simp]: |
|
758 "pdec1 0 = 0" |
|
759 "pdec2 0 = 0" |
|
760 by (simp_all add: prod_decode_def prod_decode_aux.simps) |
|
761 |
|
762 lemma ldec_zero: |
|
763 "ldec 0 n = 0" |
|
764 by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps) |
|
765 |
|
766 lemma list_encode_inverse: |
|
767 "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)" |
|
768 by (induct xs arbitrary: n rule: lenc.induct) |
|
769 (auto simp add: ldec_zero nth_Cons split: nat.splits) |
|
770 |
|
771 lemma lenc_length_le: |
|
772 "length xs \<le> lenc xs" |
|
773 by (induct xs) (simp_all add: prod_encode_def) |
|
774 |
|
775 |
|
776 text {* Membership for the List Encoding *} |
|
777 |
|
778 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
779 "within z 0 = (0 < z)" |
|
780 | "within z (Suc n) = within (pdec2 z) n" |
|
781 |
|
782 definition enclen :: "nat \<Rightarrow> nat" where |
|
783 "enclen z = BMax_rec (\<lambda>x. within z (x - 1)) z" |
|
784 |
|
785 lemma within_False [simp]: |
|
786 "within 0 n = False" |
|
787 by (induct n) (simp_all) |
|
788 |
|
789 lemma within_length [simp]: |
|
790 "within (lenc xs) s = (s < length xs)" |
|
791 apply(induct s arbitrary: xs) |
|
792 apply(case_tac xs) |
|
793 apply(simp_all add: prod_encode_def) |
|
794 apply(case_tac xs) |
|
795 apply(simp_all) |
|
796 done |
|
797 |
|
798 text {* Length of Encoded Lists *} |
|
799 |
|
800 lemma enclen_length [simp]: |
|
801 "enclen (lenc xs) = length xs" |
|
802 unfolding enclen_def |
|
803 apply(simp add: BMax_rec_eq1) |
|
804 apply(rule Greatest_equality) |
|
805 apply(auto simp add: lenc_length_le) |
|
806 done |
|
807 |
|
808 lemma enclen_penc [simp]: |
|
809 "enclen (penc (Suc x) (lenc xs)) = Suc (enclen (lenc xs))" |
|
810 by (simp only: lenc.simps[symmetric] enclen_length) (simp) |
|
811 |
|
812 lemma enclen_zero [simp]: |
|
813 "enclen 0 = 0" |
|
814 by (simp add: enclen_def) |
|
815 |
|
816 |
|
817 text {* Recursive Definitions for List Encodings *} |
|
818 |
|
819 fun |
|
820 rec_lenc :: "recf list \<Rightarrow> recf" |
|
821 where |
|
822 "rec_lenc [] = Z" |
|
823 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" |
|
824 |
|
825 definition |
|
826 "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
|
827 |
|
828 definition |
|
829 "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
|
830 |
|
831 definition |
|
832 "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]" |
|
833 |
|
834 lemma ldec_iter: |
|
835 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
|
836 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
|
837 |
|
838 lemma within_iter: |
|
839 "within z n = (0 < Iter pdec2 n z)" |
|
840 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
|
841 |
|
842 lemma lenc_lemma [simp]: |
|
843 "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)" |
|
844 by (induct fs) (simp_all) |
|
845 |
|
846 lemma ldec_lemma [simp]: |
|
847 "rec_eval rec_ldec [z, n] = ldec z n" |
|
848 by (simp add: ldec_iter rec_ldec_def) |
|
849 |
|
850 lemma within_lemma [simp]: |
|
851 "rec_eval rec_within [z, n] = (if within z n then 1 else 0)" |
|
852 by (simp add: within_iter rec_within_def) |
|
853 |
|
854 lemma enclen_lemma [simp]: |
|
855 "rec_eval rec_enclen [z] = enclen z" |
|
856 by (simp add: rec_enclen_def enclen_def) |
|
857 |
|
858 |
|
859 end |
|
860 |