1 theory Recs |
1 theory Recs |
2 imports Main Fact "~~/src/HOL/Number_Theory/Primes" |
2 imports Main Fact "~~/src/HOL/Number_Theory/Primes" |
3 begin |
3 begin |
|
4 |
|
5 (* |
|
6 some definitions from |
|
7 |
|
8 A Course in Formal Languages, Automata and Groups |
|
9 I M Chiswell |
|
10 |
|
11 and |
|
12 |
|
13 Lecture on undecidability |
|
14 Michael M. Wolf |
|
15 *) |
4 |
16 |
5 lemma if_zero_one [simp]: |
17 lemma if_zero_one [simp]: |
6 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
18 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
7 "(0::nat) < (if P then 1 else 0) = P" |
19 "(0::nat) < (if P then 1 else 0) = P" |
8 "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))" |
20 "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))" |
164 "CN f gs \<equiv> Cn (arity (hd gs)) f gs" |
176 "CN f gs \<equiv> Cn (arity (hd gs)) f gs" |
165 |
177 |
166 abbreviation |
178 abbreviation |
167 "PR f g \<equiv> Pr (arity f) f g" |
179 "PR f g \<equiv> Pr (arity f) f g" |
168 |
180 |
|
181 abbreviation |
|
182 "MN f \<equiv> Mn (arity f - 1) f" |
|
183 |
169 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
184 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
170 where |
185 where |
171 "rec_eval Z xs = 0" |
186 "rec_eval Z xs = 0" |
172 | "rec_eval S xs = Suc (xs ! 0)" |
187 | "rec_eval S xs = Suc (xs ! 0)" |
173 | "rec_eval (Id m n) xs = xs ! n" |
188 | "rec_eval (Id m n) xs = xs ! n" |
300 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
315 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
301 |
316 |
302 definition |
317 definition |
303 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
318 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
304 |
319 |
305 text {* Dvd *} |
320 text {* Dvd, Quotient, Reminder *} |
306 |
321 |
307 definition |
322 definition |
308 "rec_dvd_swap = CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0]" |
323 "rec_dvd_swap = CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0]" |
309 |
324 |
310 definition |
325 definition |
311 "rec_dvd = rec_swap rec_dvd_swap" |
326 "rec_dvd = rec_swap rec_dvd_swap" |
312 |
327 |
313 |
328 definition |
|
329 "rec_quo = (let lhs = CN S [Id 3 0] in |
|
330 let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in |
|
331 let cond = CN rec_noteq [lhs, rhs] in |
|
332 let ifz = CN rec_ifz [cond, CN S [Id 3 1], Id 3 1] |
|
333 in PR Z ifz)" |
|
334 |
|
335 definition |
|
336 "rec_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" |
314 |
337 |
315 section {* Correctness of Recursive Functions *} |
338 section {* Correctness of Recursive Functions *} |
316 |
339 |
317 lemma constn_lemma [simp]: |
340 lemma constn_lemma [simp]: |
318 "rec_eval (constn n) xs = n" |
341 "rec_eval (constn n) xs = n" |
441 by (auto simp add: rec_dvd_swap_def) |
464 by (auto simp add: rec_dvd_swap_def) |
442 |
465 |
443 lemma dvd_lemma [simp]: |
466 lemma dvd_lemma [simp]: |
444 "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)" |
467 "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)" |
445 by (simp add: rec_dvd_def) |
468 by (simp add: rec_dvd_def) |
|
469 |
|
470 |
|
471 fun Quo where |
|
472 "Quo x 0 = 0" |
|
473 | "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)" |
|
474 |
|
475 lemma Quo0: |
|
476 shows "Quo 0 y = 0" |
|
477 apply(induct y) |
|
478 apply(auto) |
|
479 done |
|
480 |
|
481 lemma Quo1: |
|
482 "x * (Quo x y) \<le> y" |
|
483 by (induct y) (simp_all) |
|
484 |
|
485 lemma Quo2: |
|
486 "b * (Quo b a) + a mod b = a" |
|
487 by (induct a) (auto simp add: mod_Suc) |
|
488 |
|
489 lemma Quo3: |
|
490 "n * (Quo n m) = m - m mod n" |
|
491 using Quo2[of n m] by (auto) |
|
492 |
|
493 lemma Quo4: |
|
494 assumes h: "0 < x" |
|
495 shows "y < x + x * Quo x y" |
|
496 proof - |
|
497 have "x - (y mod x) > 0" using mod_less_divisor assms by auto |
|
498 then have "y < y + (x - (y mod x))" by simp |
|
499 then have "y < x + (y - (y mod x))" by simp |
|
500 then show "y < x + x * (Quo x y)" by (simp add: Quo3) |
|
501 qed |
|
502 |
|
503 lemma Quo_div: |
|
504 shows "Quo x y = y div x" |
|
505 apply(case_tac "x = 0") |
|
506 apply(simp add: Quo0) |
|
507 apply(subst split_div_lemma[symmetric]) |
|
508 apply(auto intro: Quo1 Quo4) |
|
509 done |
|
510 |
|
511 lemma Quo_rec_quo: |
|
512 shows "rec_eval rec_quo [y, x] = Quo x y" |
|
513 by (induct y) (simp_all add: rec_quo_def) |
|
514 |
|
515 lemma quo_lemma [simp]: |
|
516 shows "rec_eval rec_quo [y, x] = y div x" |
|
517 by (simp add: Quo_div Quo_rec_quo) |
|
518 |
|
519 lemma rem_lemma [simp]: |
|
520 shows "rec_eval rec_rem [y, x] = y mod x" |
|
521 by (simp add: rec_rem_def mod_div_equality' nat_mult_commute) |
446 |
522 |
447 |
523 |
448 section {* Prime Numbers *} |
524 section {* Prime Numbers *} |
449 |
525 |
450 lemma prime_alt_def: |
526 lemma prime_alt_def: |
516 |
592 |
517 lemma max2_lemma [simp]: |
593 lemma max2_lemma [simp]: |
518 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
594 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
519 by (induct x) (simp_all add: rec_max2_def) |
595 by (induct x) (simp_all add: rec_max2_def) |
520 |
596 |
|
597 |
|
598 section {* Discrete Logarithms *} |
|
599 |
521 definition |
600 definition |
522 "rec_lg = |
601 "rec_lg = |
523 (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in |
602 (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in |
524 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
603 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
525 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
604 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
526 in CN rec_ifz [cond, Z, max])" |
605 in CN rec_ifz [cond, Z, max])" |
527 |
606 |
528 definition |
607 definition |
529 "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)" |
608 "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)" |
530 |
609 |
531 lemma lg_lemma: |
610 lemma lg_lemma [simp]: |
532 "rec_eval rec_lg [x, y] = Lg x y" |
611 "rec_eval rec_lg [x, y] = Lg x y" |
533 by (simp add: rec_lg_def Lg_def Let_def) |
612 by (simp add: rec_lg_def Lg_def Let_def) |
534 |
613 |
535 |
614 |
|
615 section {* Universal Function *} |
|
616 |
|
617 text {* |
|
618 @{text "Nstd c"} returns true if the configuration coded |
|
619 by @{text "c"} is not a stardard final configuration. |
|
620 *} |
|
621 fun Nstd :: "nat \<Rightarrow> bool" |
|
622 where |
|
623 "Nstd c = (stat c \<noteq> 0 \<or> left c \<noteq> 0 \<or> |
|
624 right c \<noteq> 2 ^ (Lg (Suc (right c)) 2) - 1 \<or> |
|
625 right c = 0)" |
|
626 |
|
627 |
|
628 definition |
|
629 "value x = (Lg (Suc x) 2) - 1" |
|
630 |
|
631 definition |
|
632 "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]" |
|
633 |
|
634 lemma value_lemma [simp]: |
|
635 "rec_eval rec_value [x] = value x" |
|
636 by (simp add: rec_value_def value_def) |
|
637 |
|
638 definition |
|
639 where |
|
640 "rec_UF = CN rec_valu [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]" |
|
641 |
|
642 end |
|
643 |
|
644 |
|
645 (* |
536 |
646 |
537 |
647 |
538 |
648 |
539 fun mtest where |
649 fun mtest where |
540 "mtest R 0 = if R 0 then 0 else 1" |
650 "mtest R 0 = if R 0 then 0 else 1" |