theory UF_Rec

imports Recs Turing2

begin

section {* Coding of Turing Machines and tapes*}

text {*

  The purpose of this section is to construct the coding function of Turing 

  Machine, which is going to be named @{text "code"}. *}

text {* Encoding of actions as numbers *}

fun action_num :: "action \<Rightarrow> nat"

  where

  "action_num W0 = 0"

| "action_num W1 = 1"

| "action_num L  = 2"

| "action_num R  = 3"

| "action_num Nop = 4"

fun cell_num :: "cell \<Rightarrow> nat" where

  "cell_num Bk = 0"

| "cell_num Oc = 1"

fun code_tp :: "cell list \<Rightarrow> nat list"

  where

  "code_tp [] = []"

| "code_tp (c # tp) = (cell_num c) # code_tp tp"

fun Code_tp where

  "Code_tp tp = lenc (code_tp tp)"

fun Code_conf where

  "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"

fun code_instr :: "instr \<Rightarrow> nat" where

  "code_instr i = penc (action_num (fst i)) (snd i)"

fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where

  "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"

fun code_tprog :: "tprog \<Rightarrow> nat list"

  where

  "code_tprog [] =  []"

| "code_tprog (i # tm) = Code_instr i # code_tprog tm"

lemma code_tprog_length [simp]:

  "length (code_tprog tp) = length tp"

by (induct tp) (simp_all)

lemma code_tprog_nth [simp]:

  "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)"

by (induct tp arbitrary: n) (simp_all add: nth_Cons')

fun Code_tprog :: "tprog \<Rightarrow> nat"

  where 

  "Code_tprog tm = lenc (code_tprog tm)"

section {* Universal Function in HOL *}

text {* Reading and writing the encoded tape *}

fun Read where

  "Read tp = ldec tp 0"

fun Write where

  "Write n tp = penc (Suc n) (pdec2 tp)"

text {* 

  The @{text Newleft} and @{text Newright} functions on page 91 of B book. 

  They calculate the new left and right tape (@{text p} and @{text r}) according 

  to an action @{text a}.

*}

fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Newleft l r a = (if a = 0 then l else 

                    if a = 1 then l else 

                    if a = 2 then pdec2 l else 

                    if a = 3 then penc (Suc (Read r)) l

                    else l)"

fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Newright l r a  = (if a = 0 then Write 0 r

                      else if a = 1 then Write 1 r

                      else if a = 2 then penc (Suc (Read l)) r

                      else if a = 3 then pdec2 r

                      else r)"

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 code of the Turing Machine, @{text "q"} is the current state of 

  Turing Machine, and @{text "r"} is the scanned cell of is the right tape. 

*}

fun actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

  "actn n 0 = pdec1 (pdec1 n)"

| "actn n _ = pdec1 (pdec2 n)"

fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Actn m q r = (if q \<noteq> 0 \<and> within m (q - 1) then (actn (ldec m (q - 1)) r) else 4)"

fun newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

  "newstate n 0 = pdec2 (pdec1 n)"

| "newstate n _ = pdec2 (pdec2 n)"

fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Newstate m q r = (if q \<noteq> 0 then (newstate (ldec m (q - 1)) r) else 0)"

fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"

  where

  "Conf (q, (l, r)) = lenc [q, l, r]"

fun State where

  "State cf = ldec cf 0"

fun Left where

  "Left cf = ldec cf 1"

fun Right where

  "Right cf = ldec cf 2"

fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 

                    (Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))),

                     Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf)))))"

text {*

  @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution

  of TM coded as @{text "m"}. 

*}

fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Steps cf p 0  = cf"

| "Steps cf p (Suc n) = Steps (Step cf p) p n"

text {*

  Decoding tapes into binary or stroke numbers.

*}

definition Binnum :: "nat \<Rightarrow> nat"

  where

  "Binnum z \<equiv> (\<Sum>i < enclen z. ldec z i * 2 ^ i)"

definition Stknum :: "nat \<Rightarrow> nat"

  where

  "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1"

apply(induct tp)

apply(simp)

apply(simp)

apply(case_tac a)

text {*

  @{text "Std cf"} returns true, if the  configuration  @{text "cf"} 

  is a stardard tape. 

*}

fun Std :: "nat \<Rightarrow> bool"

  where

text{* 

  @{text "Nostop m cf k"} means that afer @{text k} steps of 

  execution the TM coded by @{text m} and started in configuration

  @{text cf} is not at a stardard final configuration. *}

fun Final :: "nat \<Rightarrow> bool"

  where

    "Final cf = (State cf = 0)"

fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"

  where

  "Nostop m cf k = (Final (Steps cf m k) \<and> \<not> Std (Steps cf m k))"

text{*

  @{text "Halt"} is the function calculating the steps a TM needs to 

  execute before reaching a stardard final configuration. This recursive 

  function is the only one that uses unbounded minimization. So it is the 

  only non-primitive recursive function needs to be used in the construction 

  of the universal function @{text "UF"}. 

*}

fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "Halt m cf = (LEAST k. \<not> Nostop m cf k)"

fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "UF m cf = Stknum (Right (Steps m cf (Halt m cf)))"

section {* The UF can simulate Turing machines *}

lemma Update_left_simulate:

  shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))"

apply(induct a)

apply(simp_all)

apply(case_tac l)

apply(simp_all)

apply(case_tac r)

apply(simp_all)

done

lemma Update_right_simulate:

  shows "Newright (Code_tp l) (Code_tp r) (action_num a) = Code_tp (snd (update a (l, r)))"

apply(induct a)

apply(simp_all)

apply(case_tac r)

apply(simp_all)

apply(case_tac r)

apply(simp_all)

apply(case_tac l)

apply(simp_all)

apply(case_tac r)

apply(simp_all)

done

lemma Fetch_state_simulate:

  "tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cell_num c) = snd (fetch tp st c)"

apply(induct tp st c rule: fetch.induct)

apply(simp_all add: list_encode_inverse split: cell.split)

done

lemma Fetch_action_simulate:

  "tm_wf tp \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"

apply(induct tp st c rule: fetch.induct)

apply(simp_all add: list_encode_inverse split: cell.split)

done

lemma Read_simulate:

  "Read (Code_tp tp) = cell_num (read tp)"

apply(case_tac tp)

apply(simp_all)

done

lemma misc:

  "2 < (3::nat)"

  "1 < (3::nat)"

  "0 < (3::nat)" 

  "length [x] = 1"

  "length [x, y] = 2"

  "length [x, y , z] = 3"

  "[x, y, z] ! 0 = x"

  "[x, y, z] ! 1 = y"

  "[x, y, z] ! 2 = z"

apply(simp_all)

done

lemma Step_simulate:

  assumes "tm_wf tp"

  shows "Step (Conf (Code_conf (st, l, r))) (Code_tprog tp) = Conf (Code_conf (step (st, l, r) tp))"

apply(subst step.simps) 

apply(simp only: Let_def)

apply(subst Step.simps)

apply(simp only: Conf.simps Code_conf.simps Right.simps Left.simps)

apply(simp only: list_encode_inverse)

apply(simp only: misc if_True Code_tp.simps)

apply(simp only: prod_case_beta) 

apply(subst Fetch_state_simulate[OF assms, symmetric])

apply(simp only: State.simps)

apply(simp only: list_encode_inverse)

apply(simp only: misc if_True)

apply(simp only: Read_simulate[simplified Code_tp.simps])

apply(simp only: Fetch_action_simulate[OF assms])

apply(simp only: Update_left_simulate[simplified Code_tp.simps])

apply(simp only: Update_right_simulate[simplified Code_tp.simps])

apply(case_tac "update (fst (fetch tp st (read r))) (l, r)")

apply(simp only: Code_conf.simps)

apply(simp only: Conf.simps)

apply(simp)

done

lemma Steps_simulate:

  assumes "tm_wf tp" 

  shows "Steps (Conf (Code_conf cf)) (Code_tprog tp) n = Conf (Code_conf (steps cf tp n))"

apply(induct n arbitrary: cf) 

apply(simp)

apply(simp only: Steps.simps steps.simps)

apply(case_tac cf)

apply(simp only: )

apply(subst Step_simulate)

apply(rule assms)

apply(drule_tac x="step (a, b, c) tp" in meta_spec)

apply(simp)

done

lemma Final_simulate:

  "Final (Conf (Code_conf cf)) = is_final cf"

by (case_tac cf) (simp)

lemma Std_simulate:

  "Std (Conf (Code_conf cf)) = std_tape (snd cf)" 

apply(case_tac cf)

apply(simp add: std_tape_def del: Std.simps)

apply(subst Std.simps)

(* UNTIL HERE *)

section {* Universal Function as Recursive Functions *}

definition 

  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"

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]"

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)"

definition 

  "rec_scan = CN rec_mod [Id 1 0, constn 2]"

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_mod [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_mod [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]]]])"

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])"

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])"

definition 

  "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"

definition

  "rec_left = rec_pdec1"

definition 

  "rec_right = CN rec_pdec2 [rec_pdec1]"

definition 

  "rec_stat = CN rec_pdec2 [rec_pdec2]"

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])" 

definition 

  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])

                 (CN rec_newconf [Id 4 2 , Id 4 1])"

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])"

definition 

  "rec_nostop = CN rec_nstd [rec_conf]"

definition 

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