609 |
619 |
610 lemma lg_lemma [simp]: |
620 lemma lg_lemma [simp]: |
611 "rec_eval rec_lg [x, y] = Lg x y" |
621 "rec_eval rec_lg [x, y] = Lg x y" |
612 by (simp add: rec_lg_def Lg_def Let_def) |
622 by (simp add: rec_lg_def Lg_def Let_def) |
613 |
623 |
|
624 definition |
|
625 "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)" |
|
626 |
|
627 definition |
|
628 "rec_lo = |
|
629 (let calc = CN rec_noteq [CN rec_rem [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in |
|
630 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
|
631 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
|
632 in CN rec_ifz [cond, Z, max])" |
|
633 |
|
634 lemma lo_lemma [simp]: |
|
635 "rec_eval rec_lo [x, y] = Lo x y" |
|
636 by (simp add: rec_lo_def Lo_def Let_def) |
|
637 |
614 |
638 |
615 section {* Universal Function *} |
639 section {* Universal Function *} |
|
640 |
|
641 text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *} |
|
642 |
|
643 fun NextPrime ::"nat \<Rightarrow> nat" |
|
644 where |
|
645 "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)" |
|
646 |
|
647 definition rec_nextprime :: "recf" |
|
648 where |
|
649 "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in |
|
650 let conj2 = CN rec_less [Id 2 1, Id 2 0] in |
|
651 let conj3 = CN rec_prime [Id 2 0] in |
|
652 let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3] |
|
653 in MN (CN rec_not [conjs]))" |
|
654 |
|
655 lemma nextprime_lemma [simp]: |
|
656 "rec_eval rec_nextprime [x] = NextPrime x" |
|
657 by (simp add: rec_nextprime_def Let_def) |
|
658 |
|
659 |
|
660 fun Pi :: "nat \<Rightarrow> nat" |
|
661 where |
|
662 "Pi 0 = 2" | |
|
663 "Pi (Suc x) = NextPrime (Pi x)" |
|
664 |
|
665 definition |
|
666 "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])" |
|
667 |
|
668 lemma pi_lemma [simp]: |
|
669 "rec_eval rec_pi [x] = Pi x" |
|
670 by (induct x) (simp_all add: rec_pi_def) |
|
671 |
|
672 |
|
673 fun Left where |
|
674 "Left c = Lo c (Pi 0)" |
|
675 |
|
676 definition |
|
677 "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]" |
|
678 |
|
679 lemma left_lemma [simp]: |
|
680 "rec_eval rec_left [c] = Left c" |
|
681 by(simp add: rec_left_def) |
|
682 |
|
683 fun Right where |
|
684 "Right c = Lo c (Pi 2)" |
|
685 |
|
686 definition |
|
687 "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]" |
|
688 |
|
689 lemma right_lemma [simp]: |
|
690 "rec_eval rec_right [c] = Right c" |
|
691 by(simp add: rec_right_def) |
|
692 |
|
693 fun Stat where |
|
694 "Stat c = Lo c (Pi 1)" |
|
695 |
|
696 definition |
|
697 "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]" |
|
698 |
|
699 lemma stat_lemma [simp]: |
|
700 "rec_eval rec_stat [c] = Stat c" |
|
701 by(simp add: rec_stat_def) |
|
702 |
|
703 |
|
704 |
|
705 text{* coding of the configuration *} |
|
706 |
|
707 text {* |
|
708 @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural |
|
709 numbers encoded by number @{text "sr"} using Godel's coding. |
|
710 *} |
|
711 fun Entry where |
|
712 "Entry sr i = Lo sr (Pi (Suc i))" |
|
713 |
|
714 definition |
|
715 "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]" |
|
716 |
|
717 lemma entry_lemma [simp]: |
|
718 "rec_eval rec_entry [sr, i] = Entry sr i" |
|
719 by(simp add: rec_entry_def) |
|
720 |
|
721 |
|
722 fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat" |
|
723 where |
|
724 "Listsum2 xs 0 = 0" |
|
725 | "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n" |
|
726 |
|
727 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf" |
|
728 where |
|
729 "rec_listsum2 vl 0 = CN Z [Id vl 0]" |
|
730 | "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]" |
|
731 |
|
732 lemma listsum2_lemma [simp]: |
|
733 "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n" |
|
734 by (induct n) (simp_all) |
|
735 |
|
736 text {* |
|
737 @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the |
|
738 B book, but this definition generalises the original one to deal with multiple |
|
739 input arguments. |
|
740 *} |
|
741 fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat" |
|
742 where |
|
743 "Strt' xs 0 = 0" |
|
744 | "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n |
|
745 in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))" |
|
746 |
|
747 fun Strt :: "nat list \<Rightarrow> nat" |
|
748 where |
|
749 "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))" |
|
750 |
|
751 fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf" |
|
752 where |
|
753 "rec_strt' xs 0 = Z" |
|
754 | "rec_strt' xs (Suc n) = |
|
755 (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in |
|
756 let t1 = CN rec_power [constn 2, dbound] in |
|
757 let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in |
|
758 CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])" |
|
759 |
|
760 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list" |
|
761 where |
|
762 "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]" |
|
763 |
|
764 fun rec_strt :: "nat \<Rightarrow> recf" |
|
765 where |
|
766 "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)" |
|
767 |
|
768 lemma strt'_lemma [simp]: |
|
769 "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n" |
|
770 by (induct n) (simp_all add: Let_def) |
|
771 |
|
772 |
|
773 lemma map_suc: |
|
774 "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" |
|
775 proof - |
|
776 have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def) |
|
777 then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp |
|
778 also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp |
|
779 also have "... = map Suc xs" by (simp add: map_nth) |
|
780 finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" . |
|
781 qed |
|
782 |
|
783 lemma strt_lemma [simp]: |
|
784 "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs" |
|
785 by (simp add: comp_def map_suc[symmetric]) |
|
786 |
|
787 |
|
788 text {* The @{text "Scan"} function on page 90 of B book. *} |
|
789 fun Scan :: "nat \<Rightarrow> nat" |
|
790 where |
|
791 "Scan r = r mod 2" |
|
792 |
|
793 definition |
|
794 "rec_scan = CN rec_rem [Id 1 0, constn 2]" |
|
795 |
|
796 lemma scan_lemma [simp]: |
|
797 "rec_eval rec_scan [r] = r mod 2" |
|
798 by(simp add: rec_scan_def) |
|
799 |
|
800 |
|
801 text {* The specifation of the mutli-way branching statement on |
|
802 page 79 of Boolos's book. *} |
|
803 |
|
804 type_synonym ftype = "nat list \<Rightarrow> nat" |
|
805 type_synonym rtype = "nat list \<Rightarrow> bool" |
|
806 |
|
807 fun Embranch :: "(ftype * rtype) list \<Rightarrow> nat list \<Rightarrow> nat" |
|
808 where |
|
809 "Embranch [] xs = 0" | |
|
810 "Embranch ((g, c) # gcs) xs = (if c xs then g xs else Embranch gcs xs)" |
|
811 |
|
812 fun rec_embranch' :: "(recf * recf) list \<Rightarrow> nat \<Rightarrow> recf" |
|
813 where |
|
814 "rec_embranch' [] xs = Z" | |
|
815 "rec_embranch' ((g, c) # gcs) xs = |
|
816 CN rec_add [CN rec_mult [g, c], rec_embranch' gcs xs]" |
|
817 |
|
818 fun rec_embranch :: "(recf * recf) list \<Rightarrow> recf" |
|
819 where |
|
820 "rec_embranch [] = Z" |
|
821 | "rec_embranch ((rg, rc) # rgcs) = (let vl = arity rg in |
|
822 rec_embranch' ((rg, rc) # rgcs) vl)" |
|
823 |
|
824 (* |
|
825 lemma embranch_lemma [simp]: |
|
826 shows "rec_eval (rec_embranch (zip rgs rcs)) xs = |
|
827 Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs" |
|
828 apply(induct rcs arbitrary: rgs) |
|
829 apply(simp) |
|
830 apply(simp) |
|
831 apply(case_tac rgs) |
|
832 apply(simp) |
|
833 apply(simp) |
|
834 apply(case_tac rcs) |
|
835 apply(simp_all) |
|
836 apply(rule conjI) |
|
837 *) |
|
838 |
|
839 fun Newleft0 :: "nat list \<Rightarrow> nat" |
|
840 where |
|
841 "Newleft0 [p, r] = p" |
|
842 |
|
843 definition rec_newleft0 :: "recf" |
|
844 where |
|
845 "rec_newleft0 = Id 2 0" |
|
846 |
|
847 fun Newrgt0 :: "nat list \<Rightarrow> nat" |
|
848 where |
|
849 "Newrgt0 [p, r] = r - Scan r" |
|
850 |
|
851 definition rec_newrgt0 :: "recf" |
|
852 where |
|
853 "rec_newrgt0 = CN rec_minus [Id 2 1, CN rec_scan [Id 2 1]]" |
|
854 |
|
855 (*newleft1, newrgt1: left rgt number after execute on step*) |
|
856 fun Newleft1 :: "nat list \<Rightarrow> nat" |
|
857 where |
|
858 "Newleft1 [p, r] = p" |
|
859 |
|
860 definition rec_newleft1 :: "recf" |
|
861 where |
|
862 "rec_newleft1 = Id 2 0" |
|
863 |
|
864 fun Newrgt1 :: "nat list \<Rightarrow> nat" |
|
865 where |
|
866 "Newrgt1 [p, r] = r + 1 - Scan r" |
|
867 |
|
868 definition |
|
869 "rec_newrgt1 = CN rec_minus [CN rec_add [Id 2 1, constn 1], CN rec_scan [Id 2 1]]" |
|
870 |
|
871 fun Newleft2 :: "nat list \<Rightarrow> nat" |
|
872 where |
|
873 "Newleft2 [p, r] = p div 2" |
|
874 |
|
875 definition |
|
876 "rec_newleft2 = CN rec_quo [Id 2 0, constn 2]" |
|
877 |
|
878 fun Newrgt2 :: "nat list \<Rightarrow> nat" |
|
879 where |
|
880 "Newrgt2 [p, r] = 2 * r + p mod 2" |
|
881 |
|
882 definition |
|
883 "rec_newrgt2 = CN rec_add [CN rec_mult [constn 2, Id 2 1], |
|
884 CN rec_rem [Id 2 0, constn 2]]" |
|
885 |
|
886 fun Newleft3 :: "nat list \<Rightarrow> nat" |
|
887 where |
|
888 "Newleft3 [p, r] = 2 * p + r mod 2" |
|
889 |
|
890 definition rec_newleft3 :: "recf" |
|
891 where |
|
892 "rec_newleft3 = CN rec_add [CN rec_mult [constn 2, Id 2 0], |
|
893 CN rec_rem [Id 2 1, constn 2]]" |
|
894 |
|
895 fun Newrgt3 :: "nat list \<Rightarrow> nat" |
|
896 where |
|
897 "Newrgt3 [p, r] = r div 2" |
|
898 |
|
899 definition |
|
900 "rec_newrgt3 = CN rec_quo [Id 2 1, constn 2]" |
|
901 |
|
902 text {* The @{text "new_left"} function on page 91 of B book. *} |
|
903 |
|
904 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
905 where |
|
906 "Newleft p r a = (if a = 0 \<or> a = 1 then Newleft0 [p, r] |
|
907 else if a = 2 then Newleft2 [p, r] |
|
908 else if a = 3 then Newleft3 [p, r] |
|
909 else p)" |
|
910 |
|
911 definition |
|
912 "rec_newleft = |
|
913 (let g0 = CN rec_newleft0 [Id 3 0, Id 3 1] in |
|
914 let g1 = CN rec_newleft2 [Id 3 0, Id 3 1] in |
|
915 let g2 = CN rec_newleft3 [Id 3 0, Id 3 1] in |
|
916 let g3 = Id 3 0 in |
|
917 let r0 = CN rec_disj [CN rec_eq [Id 3 2, constn 0], |
|
918 CN rec_eq [Id 3 2, constn 1]] in |
|
919 let r1 = CN rec_eq [Id 3 2, constn 2] in |
|
920 let r2 = CN rec_eq [Id 3 2, constn 3] in |
|
921 let r3 = CN rec_less [constn 3, Id 3 2] in |
|
922 let gs = [g0, g1, g2, g3] in |
|
923 let rs = [r0, r1, r2, r3] in |
|
924 rec_embranch (zip gs rs))" |
|
925 |
|
926 |
|
927 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
928 where |
|
929 "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r" |
|
930 |
|
931 |
616 |
932 |
617 text {* |
933 text {* |
618 @{text "Nstd c"} returns true if the configuration coded |
934 @{text "Nstd c"} returns true if the configuration coded |
619 by @{text "c"} is not a stardard final configuration. |
935 by @{text "c"} is not a stardard final configuration. |
620 *} |
936 *} |
621 fun Nstd :: "nat \<Rightarrow> bool" |
937 fun Nstd :: "nat \<Rightarrow> bool" |
622 where |
938 where |
623 "Nstd c = (stat c \<noteq> 0 \<or> left c \<noteq> 0 \<or> |
939 "Nstd c = (Stat c \<noteq> 0 \<or> Left c \<noteq> 0 \<or> |
624 right c \<noteq> 2 ^ (Lg (Suc (right c)) 2) - 1 \<or> |
940 Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> |
625 right c = 0)" |
941 Right c = 0)" |
626 |
942 |
627 |
943 text {* |
628 definition |
944 @{text "Conf m r k"} computes the TM configuration after |
629 "value x = (Lg (Suc x) 2) - 1" |
945 @{text "k"} steps of execution of the TM coded as @{text "m"} |
|
946 starting from the initial configuration where the left number |
|
947 equals @{text "0"} and the right number equals @{text "r"}. |
|
948 *} |
|
949 fun Conf |
|
950 where |
|
951 "Conf m r 0 = Trpl 0 (Suc 0) r" |
|
952 | "Conf m r (Suc t) = Newconf m (Conf m r t)" |
|
953 |
|
954 |
|
955 text{* |
|
956 @{text "Nonstop m r t"} means that afer @{text "t"} steps of |
|
957 execution, the TM coded by @{text "m"} is not at a stardard |
|
958 final configuration. |
|
959 *} |
|
960 fun Nostop |
|
961 where |
|
962 "Nostop m r t = Nstd (Conf m r t)" |
|
963 |
|
964 fun Value where |
|
965 "Value x = (Lg (Suc x) 2) - 1" |
630 |
966 |
631 definition |
967 definition |
632 "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]" |
968 "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]" |
633 |
969 |
634 lemma value_lemma [simp]: |
970 lemma value_lemma [simp]: |
635 "rec_eval rec_value [x] = value x" |
971 "rec_eval rec_value [x] = Value x" |
636 by (simp add: rec_value_def value_def) |
972 by (simp add: rec_value_def) |
637 |
973 |
638 definition |
974 definition |
639 where |
975 "rec_UF = CN rec_value [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]" |
640 "rec_UF = CN rec_valu [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]" |
|
641 |
976 |
642 end |
977 end |
643 |
978 |
644 |
979 |
645 (* |
980 (* |