267 |
269 |
268 definition |
270 definition |
269 "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]" |
271 "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]" |
270 |
272 |
271 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero, |
273 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero, |
272 y otherwise *} |
274 y otherwise; @{term "rec_if [z, x, y]"} returns x if z is *not* |
|
275 zero, y otherwise *} |
273 |
276 |
274 definition |
277 definition |
275 "rec_ifz = PR (Id 2 0) (Id 4 3)" |
278 "rec_ifz = PR (Id 2 0) (Id 4 3)" |
276 |
|
277 text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero, |
|
278 y otherwise *} |
|
279 |
279 |
280 definition |
280 definition |
281 "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]" |
281 "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]" |
282 |
282 |
283 text {* |
283 text {* |
284 @{text "rec_less"} compares two arguments and returns @{text "1"} if |
284 @{text "rec_less"} compares two arguments and returns @{text "1"} if |
285 the first is less than the second; otherwise returns @{text "0"}. *} |
285 the first is less than the second; otherwise returns @{text "0"}. *} |
|
286 |
286 definition |
287 definition |
287 "rec_less = CN rec_sign [rec_swap rec_minus]" |
288 "rec_less = CN rec_sign [rec_swap rec_minus]" |
288 |
289 |
289 definition |
290 definition |
290 "rec_le = CN rec_disj [rec_less, rec_eq]" |
291 "rec_le = CN rec_disj [rec_less, rec_eq]" |
315 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
316 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
316 |
317 |
317 definition |
318 definition |
318 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
319 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
319 |
320 |
320 text {* Dvd, Quotient, Reminder *} |
321 text {* Dvd, Quotient, Modulo *} |
321 |
322 |
322 definition |
323 definition |
323 "rec_dvd = |
324 "rec_dvd = |
324 rec_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])" |
325 rec_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])" |
325 |
326 |
329 let cond = CN rec_eq [lhs, rhs] in |
330 let cond = CN rec_eq [lhs, rhs] in |
330 let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1] |
331 let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1] |
331 in PR Z if_stmt)" |
332 in PR Z if_stmt)" |
332 |
333 |
333 definition |
334 definition |
334 "rec_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" |
335 "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" |
|
336 |
|
337 |
|
338 section {* Prime Numbers *} |
|
339 |
|
340 definition |
|
341 "rec_prime = |
|
342 (let conj1 = CN rec_less [constn 1, Id 1 0] in |
|
343 let disj = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in |
|
344 let imp = CN rec_imp [rec_dvd, disj] in |
|
345 let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in |
|
346 CN rec_conj [conj1, conj2])" |
|
347 |
335 |
348 |
336 section {* Correctness of Recursive Functions *} |
349 section {* Correctness of Recursive Functions *} |
337 |
350 |
338 lemma constn_lemma [simp]: |
351 lemma constn_lemma [simp]: |
339 "rec_eval (constn n) xs = n" |
352 "rec_eval (constn n) xs = n" |
504 lemma quo_lemma [simp]: |
517 lemma quo_lemma [simp]: |
505 shows "rec_eval rec_quo [y, x] = y div x" |
518 shows "rec_eval rec_quo [y, x] = y div x" |
506 by (simp add: Quo_div Quo_rec_quo) |
519 by (simp add: Quo_div Quo_rec_quo) |
507 |
520 |
508 lemma rem_lemma [simp]: |
521 lemma rem_lemma [simp]: |
509 shows "rec_eval rec_rem [y, x] = y mod x" |
522 shows "rec_eval rec_mod [y, x] = y mod x" |
510 by (simp add: rec_rem_def mod_div_equality' nat_mult_commute) |
523 by (simp add: rec_mod_def mod_div_equality' nat_mult_commute) |
511 |
524 |
512 |
525 |
513 section {* Prime Numbers *} |
526 section {* Prime Numbers *} |
514 |
527 |
515 lemma prime_alt_def: |
528 lemma prime_alt_def: |
517 shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))" |
530 shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))" |
518 apply(auto simp add: prime_nat_def dvd_def) |
531 apply(auto simp add: prime_nat_def dvd_def) |
519 apply(drule_tac x="k" in spec) |
532 apply(drule_tac x="k" in spec) |
520 apply(auto) |
533 apply(auto) |
521 done |
534 done |
522 |
|
523 definition |
|
524 "rec_prime = |
|
525 (let conj1 = CN rec_less [constn 1, Id 1 0] in |
|
526 let disj = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in |
|
527 let imp = CN rec_imp [rec_dvd, disj] in |
|
528 let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in |
|
529 CN rec_conj [conj1, conj2])" |
|
530 |
535 |
531 lemma prime_lemma [simp]: |
536 lemma prime_lemma [simp]: |
532 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
537 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
533 by (auto simp add: rec_prime_def Let_def prime_alt_def) |
538 by (auto simp add: rec_prime_def Let_def prime_alt_def) |
534 |
539 |
603 definition |
608 definition |
604 "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)" |
609 "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)" |
605 |
610 |
606 definition |
611 definition |
607 "rec_lo = |
612 "rec_lo = |
608 (let calc = CN rec_noteq [CN rec_rem [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in |
613 (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in |
609 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
614 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
610 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
615 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
611 in CN rec_ifz [cond, Z, max])" |
616 in CN rec_ifz [cond, Z, max])" |
612 |
617 |
613 lemma lo_lemma [simp]: |
618 lemma lo_lemma [simp]: |
614 "rec_eval rec_lo [x, y] = Lo x y" |
619 "rec_eval rec_lo [x, y] = Lo x y" |
615 by (simp add: rec_lo_def Lo_def Let_def) |
620 by (simp add: rec_lo_def Lo_def Let_def) |
616 |
621 |
617 |
622 |
618 |
623 |
619 text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *} |
624 text {* |
|
625 @{text "NextPrime x"} returns the first prime number after @{text "x"}; |
|
626 @{text "Pi i"} returns the i-th prime number. *} |
620 |
627 |
621 fun NextPrime ::"nat \<Rightarrow> nat" |
628 fun NextPrime ::"nat \<Rightarrow> nat" |
622 where |
629 where |
623 "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)" |
630 "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)" |
624 |
631 |
645 |
652 |
646 lemma pi_lemma [simp]: |
653 lemma pi_lemma [simp]: |
647 "rec_eval rec_pi [x] = Pi x" |
654 "rec_eval rec_pi [x] = Pi x" |
648 by (induct x) (simp_all add: rec_pi_def) |
655 by (induct x) (simp_all add: rec_pi_def) |
649 |
656 |
650 |
|
651 end |
657 end |
652 |
658 |
653 |
|
654 (* |
659 (* |
655 |
|
656 |
|
657 |
|
658 fun mtest where |
|
659 "mtest R 0 = if R 0 then 0 else 1" |
|
660 | "mtest R (Suc n) = (if R n then mtest R n else (Suc n))" |
|
661 |
|
662 |
|
663 lemma |
|
664 "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX" |
|
665 apply(simp only: rec_maxr2_def) |
|
666 apply(case_tac x) |
|
667 apply(clarify) |
|
668 apply(subst rec_eval.simps) |
|
669 apply(simp only: constn_lemma) |
|
670 defer |
|
671 apply(clarify) |
|
672 apply(subst rec_eval.simps) |
|
673 apply(simp only: rec_maxr2_def[symmetric]) |
|
674 apply(subst rec_eval.simps) |
|
675 apply(simp only: map.simps nth) |
|
676 apply(subst rec_eval.simps) |
|
677 apply(simp only: map.simps nth) |
|
678 apply(subst rec_eval.simps) |
|
679 apply(simp only: map.simps nth) |
|
680 apply(subst rec_eval.simps) |
|
681 apply(simp only: map.simps nth) |
|
682 apply(subst rec_eval.simps) |
|
683 apply(simp only: map.simps nth) |
|
684 apply(subst rec_eval.simps) |
|
685 apply(simp only: map.simps nth) |
|
686 |
|
687 |
|
688 definition |
|
689 "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))" |
|
690 |
|
691 definition |
|
692 "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])" |
|
693 |
|
694 definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat" |
|
695 where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})" |
|
696 |
|
697 definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat" |
|
698 where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})" |
|
699 |
660 |
700 lemma rec_minr2_le_Suc: |
661 lemma rec_minr2_le_Suc: |
701 "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x" |
662 "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x" |
702 apply(simp add: rec_minr2_def) |
663 apply(simp add: rec_minr2_def) |
703 apply(auto intro!: setsum_one_le setprod_one_le) |
664 apply(auto intro!: setsum_one_le setprod_one_le) |