639 section {* Universal Function *}

   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 

   932 

   933 text {*

   934   @{text "Nstd c"} returns true if the configuration coded 

   935   by @{text "c"} is not a stardard final configuration.

   936   *}

   937 fun Nstd :: "nat \<Rightarrow> bool"

   938   where

   939   "Nstd c = (Stat c \<noteq> 0 \<or> Left c \<noteq> 0 \<or> 

   940              Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> 

   941              Right c = 0)"

   942 

   943 text {*

   944   @{text "Conf m r k"} computes the TM configuration after 

   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"

   966 

   967 definition 

   968   "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"

   969 

   970 lemma value_lemma [simp]:

   971   "rec_eval rec_value [x] = Value x"

   972 by (simp add: rec_value_def)

   973 

   974 definition 

   975   "rec_UF = CN rec_value [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]"