338 in PR Z if_stmt)" |
338 in PR Z if_stmt)" |
339 |
339 |
340 definition |
340 definition |
341 "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" |
341 "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" |
342 |
342 |
343 |
343 text {* Iteration *} |
344 section {* Prime Numbers *} |
344 |
345 |
345 definition |
346 definition |
346 "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])" |
347 "rec_prime = |
347 |
348 (let conj1 = CN rec_less [constn 1, Id 1 0] in |
348 fun Iter where |
349 let disj = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in |
349 "Iter f 0 = id" |
350 let imp = CN rec_imp [rec_dvd, disj] in |
350 | "Iter f (Suc n) = f \<circ> (Iter f n)" |
351 let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in |
351 |
352 CN rec_conj [conj1, conj2])" |
352 lemma iter_comm: |
353 |
353 "(Iter f n) (f x) = f ((Iter f n) x)" |
|
354 by (induct n) (simp_all) |
|
355 |
|
356 lemma iter_lemma [simp]: |
|
357 "rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x" |
|
358 by (induct n) (simp_all add: rec_iter_def) |
354 |
359 |
355 section {* Correctness of Recursive Functions *} |
360 section {* Correctness of Recursive Functions *} |
356 |
361 |
357 lemma constn_lemma [simp]: |
362 lemma constn_lemma [simp]: |
358 "rec_eval (constn n) xs = n" |
363 "rec_eval (constn n) xs = n" |
526 |
531 |
527 lemma rem_lemma [simp]: |
532 lemma rem_lemma [simp]: |
528 shows "rec_eval rec_mod [y, x] = y mod x" |
533 shows "rec_eval rec_mod [y, x] = y mod x" |
529 by (simp add: rec_mod_def mod_div_equality' nat_mult_commute) |
534 by (simp add: rec_mod_def mod_div_equality' nat_mult_commute) |
530 |
535 |
531 |
|
532 section {* Prime Numbers *} |
|
533 |
|
534 lemma prime_alt_def: |
|
535 fixes p::nat |
|
536 shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))" |
|
537 apply(auto simp add: prime_nat_def dvd_def) |
|
538 apply(drule_tac x="k" in spec) |
|
539 apply(auto) |
|
540 done |
|
541 |
|
542 lemma prime_lemma [simp]: |
|
543 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
|
544 by (auto simp add: rec_prime_def Let_def prime_alt_def) |
|
545 |
536 |
546 section {* Bounded Maximisation *} |
537 section {* Bounded Maximisation *} |
547 |
538 |
548 fun BMax_rec where |
539 fun BMax_rec where |
549 "BMax_rec R 0 = 0" |
540 "BMax_rec R 0 = 0" |
774 lemma enclen_zero [simp]: |
765 lemma enclen_zero [simp]: |
775 "enclen 0 = 0" |
766 "enclen 0 = 0" |
776 by (simp add: enclen_def) |
767 by (simp add: enclen_def) |
777 |
768 |
778 |
769 |
779 |
770 definition |
780 section {* Discrete Logarithms *} |
771 "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
781 |
772 |
782 definition |
773 lemma ldec_iter: |
783 "rec_lg = |
774 "ldec z n = pdec1 ((Iter pdec2 n) z) - 1" |
784 (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in |
775 apply(induct n arbitrary: z) |
785 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
776 apply(simp_all) |
786 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
777 apply(subst iter_comm) |
787 in CN rec_ifz [cond, Z, max])" |
778 apply(simp) |
788 |
779 done |
789 definition |
780 |
790 "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)" |
781 lemma ldec_lemma [simp]: |
791 |
782 "rec_eval rec_ldec [z, n] = ldec z n" |
792 lemma lg_lemma [simp]: |
783 by (simp add: ldec_iter rec_ldec_def) |
793 "rec_eval rec_lg [x, y] = Lg x y" |
|
794 by (simp add: rec_lg_def Lg_def Let_def) |
|
795 |
|
796 definition |
|
797 "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)" |
|
798 |
|
799 definition |
|
800 "rec_lo = |
|
801 (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in |
|
802 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
|
803 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
|
804 in CN rec_ifz [cond, Z, max])" |
|
805 |
|
806 lemma lo_lemma [simp]: |
|
807 "rec_eval rec_lo [x, y] = Lo x y" |
|
808 by (simp add: rec_lo_def Lo_def Let_def) |
|
809 |
|
810 section {* NextPrime number function *} |
|
811 |
|
812 text {* |
|
813 @{text "NextPrime x"} returns the first prime number after @{text "x"}; |
|
814 @{text "Pi i"} returns the i-th prime number. *} |
|
815 |
|
816 definition NextPrime ::"nat \<Rightarrow> nat" |
|
817 where |
|
818 "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)" |
|
819 |
|
820 definition rec_nextprime :: "recf" |
|
821 where |
|
822 "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in |
|
823 let conj2 = CN rec_less [Id 2 1, Id 2 0] in |
|
824 let conj3 = CN rec_prime [Id 2 0] in |
|
825 let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3] |
|
826 in MN (CN rec_not [conjs]))" |
|
827 |
|
828 lemma nextprime_lemma [simp]: |
|
829 "rec_eval rec_nextprime [x] = NextPrime x" |
|
830 by (simp add: rec_nextprime_def Let_def NextPrime_def) |
|
831 |
|
832 lemma NextPrime_simps [simp]: |
|
833 shows "NextPrime 2 = 3" |
|
834 and "NextPrime 3 = 5" |
|
835 apply(simp_all add: NextPrime_def) |
|
836 apply(rule Least_equality) |
|
837 apply(auto) |
|
838 apply(eval) |
|
839 apply(rule Least_equality) |
|
840 apply(auto) |
|
841 apply(eval) |
|
842 apply(case_tac "y = 4") |
|
843 apply(auto) |
|
844 done |
|
845 |
|
846 fun Pi :: "nat \<Rightarrow> nat" |
|
847 where |
|
848 "Pi 0 = 2" | |
|
849 "Pi (Suc x) = NextPrime (Pi x)" |
|
850 |
|
851 lemma Pi_simps [simp]: |
|
852 shows "Pi 1 = 3" |
|
853 and "Pi 2 = 5" |
|
854 using NextPrime_simps |
|
855 by(simp_all add: numeral_eq_Suc One_nat_def) |
|
856 |
|
857 definition |
|
858 "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])" |
|
859 |
|
860 lemma pi_lemma [simp]: |
|
861 "rec_eval rec_pi [x] = Pi x" |
|
862 by (induct x) (simp_all add: rec_pi_def) |
|
863 |
784 |
864 end |
785 end |
865 |
786 |