theory UF_Rec+
−
imports Recs Turing_Hoare+
−
begin+
−
+
−
section {* Universal Function *}+
−
+
−
+
−
+
−
text{* coding of the configuration *}+
−
+
−
text {*+
−
  @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural +
−
  numbers encoded by number @{text "sr"} using Godel's coding.+
−
  *}+
−
fun Entry where+
−
  "Entry sr i = Lo sr (Pi (Suc i))"+
−
+
−
definition +
−
  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"+
−
+
−
lemma entry_lemma [simp]:+
−
  "rec_eval rec_entry [sr, i] = Entry sr i"+
−
by(simp add: rec_entry_def)+
−
+
−
+
−
fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Listsum2 xs 0 = 0"+
−
| "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"+
−
+
−
fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"+
−
  where+
−
  "rec_listsum2 vl 0 = CN Z [Id vl 0]"+
−
| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"+
−
+
−
lemma listsum2_lemma [simp]: +
−
  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"+
−
by (induct n) (simp_all)+
−
+
−
text {*+
−
  @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the +
−
  B book, but this definition generalises the original one to deal with multiple +
−
  input arguments.+
−
  *}+
−
fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Strt' xs 0 = 0"+
−
| "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n +
−
                       in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))"+
−
+
−
fun Strt :: "nat list \<Rightarrow> nat"+
−
  where+
−
  "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"+
−
+
−
fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"+
−
  where+
−
  "rec_strt' xs 0 = Z"+
−
| "rec_strt' xs (Suc n) = +
−
      (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in+
−
       let t1 = CN rec_power [constn 2, dbound] in+
−
       let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in+
−
       CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"+
−
+
−
fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"+
−
  where+
−
  "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"+
−
+
−
fun rec_strt :: "nat \<Rightarrow> recf"+
−
  where+
−
  "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"+
−
+
−
lemma strt'_lemma [simp]:+
−
  "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"+
−
by (induct n) (simp_all add: Let_def)+
−
+
−
+
−
lemma map_suc:+
−
  "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"+
−
proof -+
−
  have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)+
−
  then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp+
−
  also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp+
−
  also have "... = map Suc xs" by (simp add: map_nth)+
−
  finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .+
−
qed+
−
+
−
lemma strt_lemma [simp]: +
−
  "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"+
−
by (simp add: comp_def map_suc[symmetric])+
−
+
−
+
−
text {* The @{text "Scan"} function on page 90 of B book. *}+
−
fun Scan :: "nat \<Rightarrow> nat"+
−
  where+
−
  "Scan r = r mod 2"+
−
+
−
definition +
−
  "rec_scan = CN rec_rem [Id 1 0, constn 2]"+
−
+
−
lemma scan_lemma [simp]: +
−
  "rec_eval rec_scan [r] = r mod 2"+
−
by(simp add: rec_scan_def)+
−
+
−
text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *}+
−
+
−
fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Newleft p r a = (if a = 0 \<or> a = 1 then p +
−
                    else if a = 2 then p div 2+
−
                    else if a = 3 then 2 * p + r mod 2+
−
                    else p)"+
−
+
−
fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Newright p r a  = (if a = 0 then r - Scan r+
−
                      else if a = 1 then r + 1 - Scan r+
−
                      else if a = 2 then 2 * r + p mod 2+
−
                      else if a = 3 then r div 2+
−
                      else r)"+
−
+
−
definition+
−
    "rec_newleft =+
−
       (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in+
−
        let cond2 = CN rec_eq [Id 3 2, constn 2] in+
−
        let cond3 = CN rec_eq [Id 3 2, constn 3] in+
−
        let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], +
−
                                CN rec_rem [Id 3 1, constn 2]] in+
−
        CN rec_if [cond1, Id 3 0, +
−
          CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],+
−
            CN rec_if [cond3, case3, Id 3 0]]])"+
−
+
−
definition+
−
    "rec_newright =+
−
       (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in+
−
        let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in+
−
        let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in+
−
        let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     +
−
                                CN rec_rem [Id 3 0, constn 2]] in+
−
        let case3 = CN rec_quo [Id 2 1, constn 2] in+
−
        CN rec_if [condn 0, case0, +
−
          CN rec_if [condn 1, case1,+
−
            CN rec_if [condn 2, case2,+
−
              CN rec_if [condn 3, case3, Id 3 1]]]])"+
−
+
−
lemma newleft_lemma [simp]:+
−
  "rec_eval rec_newleft [p, r, a] = Newleft p r a"+
−
by (simp add: rec_newleft_def Let_def)+
−
+
−
lemma newright_lemma [simp]:+
−
  "rec_eval rec_newright [p, r, a] = Newright p r a"+
−
by (simp add: rec_newright_def Let_def)+
−
+
−
text {*+
−
  The @{text "Actn"} function given on page 92 of B book, which is used to +
−
  fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is +
−
  the Goedel coding of a Turing Machine, @{text "q"} is the current state of +
−
  Turing Machine, @{text "r"} is the right number of Turing Machine tape.+
−
  *}+
−
fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)"+
−
+
−
definition +
−
  "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in+
−
               let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in+
−
               let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]+
−
               in CN rec_if [Id 3 1, entry, constn 4])"+
−
+
−
lemma actn_lemma [simp]:+
−
  "rec_eval rec_actn [m, q, r] = Actn m q r"+
−
by (simp add: rec_actn_def)+
−
+
−
fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)"+
−
+
−
definition rec_newstat :: "recf"+
−
  where+
−
  "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in+
−
                  let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in+
−
                  let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]+
−
                  in CN rec_if [Id 3 1, entry, Z])"+
−
+
−
lemma newstat_lemma [simp]: +
−
  "rec_eval rec_newstat [m, q, r] = Newstat m q r"+
−
by (simp add: rec_newstat_def)+
−
+
−
+
−
fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"+
−
+
−
definition +
−
  "rec_trpl = CN rec_mult [CN rec_mult +
−
       [CN rec_power [constn (Pi 0), Id 3 0], +
−
        CN rec_power [constn (Pi 1), Id 3 1]],+
−
        CN rec_power [constn (Pi 2), Id 3 2]]"+
−
+
−
lemma trpl_lemma [simp]: +
−
  "rec_eval rec_trpl [p, q, r] = Trpl p q r"+
−
by (simp add: rec_trpl_def)+
−
+
−
+
−
+
−
fun Left where+
−
  "Left c = Lo c (Pi 0)"+
−
+
−
definition+
−
  "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"+
−
+
−
lemma left_lemma [simp]:+
−
  "rec_eval rec_left [c] = Left c" +
−
by(simp add: rec_left_def)+
−
+
−
fun Right where+
−
  "Right c = Lo c (Pi 2)"+
−
+
−
definition +
−
  "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"+
−
+
−
lemma right_lemma [simp]:+
−
  "rec_eval rec_right [c] = Right c" +
−
by(simp add: rec_right_def)+
−
+
−
fun Stat where+
−
  "Stat c = Lo c (Pi 1)"+
−
+
−
definition +
−
  "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"+
−
+
−
lemma stat_lemma [simp]:+
−
  "rec_eval rec_stat [c] = Stat c" +
−
by(simp add: rec_stat_def)+
−
+
−
fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"+
−
  where+
−
  "Inpt m xs = Trpl 0 1 (Strt xs)"+
−
+
−
fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Newconf m c = Trpl (Newleft (Left c) (Right c) (Actn m (Stat c) (Right c)))+
−
                      (Newstat m (Stat c) (Right c)) +
−
                      (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))"+
−
+
−
definition +
−
  "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in+
−
                  let left = CN rec_left [Id 2 1] in+
−
                  let right = CN rec_right [Id 2 1] in+
−
                  let stat = CN rec_stat [Id 2 1] in+
−
                  let one = CN rec_newleft [left, right, act] in+
−
                  let two = CN rec_newstat [Id 2 0, stat, right] in+
−
                  let three = CN rec_newright [left, right, act]+
−
                  in CN rec_trpl [one, two, three])" +
−
+
−
lemma newconf_lemma [simp]: +
−
  "rec_eval rec_newconf [m, c] = Newconf m c"+
−
by (simp add: rec_newconf_def Let_def)+
−
+
−
text {*+
−
  @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution+
−
  of TM coded as @{text "m"} starting from the initial configuration where the left +
−
  number equals @{text "0"}, right number equals @{text "r"}. +
−
  *}+
−
fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Conf 0 m r  = Trpl 0 1 r"+
−
| "Conf (Suc k) m r = Newconf m (Conf k m r)"+
−
+
−
definition +
−
  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])+
−
                 (CN rec_newconf [Id 4 2 , Id 4 1])"+
−
+
−
lemma conf_lemma [simp]: +
−
  "rec_eval rec_conf [k, m, r] = Conf k m r"+
−
by(induct k) (simp_all add: rec_conf_def)+
−
+
−
+
−
text {*+
−
  @{text "Nstd c"} returns true if the configuration coded +
−
  by @{text "c"} is not a stardard final configuration.+
−
  *}+
−
fun Nstd :: "nat \<Rightarrow> bool"+
−
  where+
−
  "Nstd c = (Stat c \<noteq> 0 \<or> +
−
             Left c \<noteq> 0 \<or> +
−
             Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> +
−
             Right c = 0)"+
−
+
−
definition +
−
  "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in+
−
               let disj2 = CN rec_noteq [rec_left, constn 0] in+
−
               let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in+
−
               let disj3 = CN rec_noteq [rec_right, rhs] in+
−
               let disj4 = CN rec_eq [rec_right, constn 0] in+
−
               CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"+
−
+
−
lemma nstd_lemma [simp]:+
−
  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"+
−
by(simp add: rec_nstd_def)+
−
+
−
+
−
text{* +
−
  @{text "Nostop t m r"} means that afer @{text "t"} steps of +
−
  execution, the TM coded by @{text "m"} is not at a stardard +
−
  final configuration.+
−
  *}+
−
fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"+
−
  where+
−
  "Nostop t m r = Nstd (Conf t m r)"+
−
+
−
definition +
−
  "rec_nostop = CN rec_nstd [rec_conf]"+
−
+
−
lemma nostop_lemma [simp]:+
−
  "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" +
−
by (simp add: rec_nostop_def)+
−
+
−
+
−
fun Value where+
−
  "Value x = (Lg (Suc x) 2) - 1"+
−
+
−
definition +
−
  "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"+
−
+
−
lemma value_lemma [simp]:+
−
  "rec_eval rec_value [x] = Value x"+
−
by (simp add: rec_value_def)+
−
+
−
text{*+
−
  @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before+
−
  to reach a stardard final configuration. This recursive function is the only one+
−
  using @{text "Mn"} combinator. So it is the only non-primitive recursive function +
−
  needs to be used in the construction of the universal function @{text "rec_uf"}.+
−
  *}+
−
+
−
definition +
−
  "rec_halt = MN rec_nostop" +
−
+
−
+
−
definition +
−
  "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"+
−
+
−
text {*+
−
  The correctness of @{text "rec_uf"}, nonhalt case.+
−
  *}+
−
+
−
subsection {* Coding function of TMs *}+
−
+
−
text {*+
−
  The purpose of this section is to get the coding function of Turing Machine, +
−
  which is going to be named @{text "code"}.+
−
  *}+
−
+
−
fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "bl2nat [] n = 0"+
−
| "bl2nat (Bk # bl) n = bl2nat bl (Suc n)"+
−
| "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)"+
−
+
−
fun bl2wc :: "cell list \<Rightarrow> nat"+
−
  where+
−
  "bl2wc xs = bl2nat xs 0"+
−
+
−
fun trpl_code :: "config \<Rightarrow> nat"+
−
  where+
−
  "trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"+
−
+
−
fun action_map :: "action \<Rightarrow> nat"+
−
  where+
−
  "action_map W0 = 0"+
−
| "action_map W1 = 1"+
−
| "action_map L = 2"+
−
| "action_map R = 3"+
−
| "action_map Nop = 4"+
−
+
−
fun action_map_iff :: "nat \<Rightarrow> action"+
−
  where+
−
  "action_map_iff (0::nat) = W0"+
−
| "action_map_iff (Suc 0) = W1"+
−
| "action_map_iff (Suc (Suc 0)) = L"+
−
| "action_map_iff (Suc (Suc (Suc 0))) = R"+
−
| "action_map_iff n = Nop"+
−
+
−
fun block_map :: "cell \<Rightarrow> nat"+
−
  where+
−
  "block_map Bk = 0"+
−
| "block_map Oc = 1"+
−
+
−
fun Goedel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"+
−
  where+
−
  "Goedel_code' [] n = 1"+
−
| "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) "+
−
+
−
fun Goedel_code :: "nat list \<Rightarrow> nat"+
−
  where+
−
  "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)"+
−
+
−
fun modify_tprog :: "instr list \<Rightarrow> nat list"+
−
  where+
−
  "modify_tprog [] =  []"+
−
| "modify_tprog ((a, s) # nl) = action_map a # s # modify_tprog nl"+
−
+
−
text {* @{text "Code tp"} gives the Goedel coding of TM program @{text "tp"}. *}+
−
fun Code :: "instr list \<Rightarrow> nat"+
−
  where +
−
  "Code tp = Goedel_code (modify_tprog tp)"+
−
+
−
subsection {* Relating interperter functions to the execution of TMs *}+
−
+
−
+
−
lemma F_correct: +
−
  assumes tp: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"+
−
  and     wf:  "tm_wf0 tp" "0 < rs"+
−
  shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"+
−
+
−
+
−
end+
−
+
−