theory UF_Rec

begin

section {* Coding of Turing Machines and Tapes*}

fun actnum :: "taction \<Rightarrow> nat"

  where

  "actnum W0 = 0"

| "actnum W1 = 1"

| "actnum L  = 2"

| "actnum R  = 3"

fun cellnum :: "Block \<Rightarrow> nat" where

  "cellnum Bk = 0"

| "cellnum Oc = 1"

text {* Coding tapes *}

  where

  "code_tp [] = []"

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

fun Code_tp where

  "Code_tp tp = lenc (code_tp tp)"

lemma code_tp_append [simp]:

  "code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2"

by(induct tp1) (simp_all)

lemma code_tp_length [simp]:

  "length (code_tp tp) = length tp"

by (induct tp) (simp_all)

lemma code_tp_nth [simp]:

  "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"

apply(induct n arbitrary: tp) 

apply(simp_all)

apply(case_tac [!] tp)

apply(simp_all)

done

lemma code_tp_replicate [simp]:

  "code_tp (c \<up> n) = (cellnum c) \<up> n"

by(induct n) (simp_all)

text {* Coding Configurations and TMs *}

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 (actnum (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 {* An 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}. Adapted to our encoding functions.

*}

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 "Action"} function given on page 92 of B book, which is used to 

  fetch Turing Machine intructions. In @{text "Action 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 Action :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

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

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

  "Newstat n 0 = pdec2 (pdec1 n)"

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

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

  where

  "Newstate m q r = (if q \<noteq> 0 then Newstat (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"

text {*

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

  execution of TM coded as @{text "m"}. @{text Step} is a single step of the TM.

*}

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

  where

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

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

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

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"

lemma Step_Steps_comm:

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

by (induct n arbitrary: cf) (simp_all only: Steps.simps)

text {* Decoding tapes back into numbers. *}

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

  where

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

lemma Stknum_append:

  "Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)"

apply(simp only: Code_tp.simps)

apply(simp only: code_tp_append)

apply(simp only: Stknum_def)

apply(simp only: enclen_length length_append code_tp_length)

apply(simp only: list_encode_inverse)

apply(simp only: enclen_length length_append code_tp_length)

apply(simp)

apply(subgoal_tac "{..<length tp1 + length tp2} = {..<length tp1} \<union> {length tp1 ..<length tp1 + length tp2}")

prefer 2

apply(auto)[1]

apply(simp only:)

apply(subst setsum_Un_disjoint)

apply(auto)[2]

apply (metis ivl_disj_int_one(2))

apply(simp add: nth_append)

apply(subgoal_tac "{length tp1..<length tp1 + length tp2} = (\<lambda>x. x + length tp1) ` {0..<length tp2}")

prefer 2

apply(simp only: image_add_atLeastLessThan)

apply (metis comm_monoid_add_class.add.left_neutral nat_add_commute)

apply(simp only:)

apply(subst setsum_reindex)

prefer 2

apply(simp add: comp_def)

apply (metis atLeast0LessThan)

apply(simp add: inj_on_def)

done

lemma Stknum_up:

  "Stknum (lenc (a \<up> n)) = n * a"

apply(induct n)

apply(simp_all add: Stknum_def list_encode_inverse del: replicate.simps)

done

lemma result:

  "Stknum (Code_tp (<n> @ Bk \<up> l)) - 1 = n"

apply(simp only: Stknum_append)

apply(simp only: tape_of_nat.simps)

apply(simp only: Code_tp.simps)

apply(simp only: code_tp_replicate)

apply(simp only: cellnum.simps)

apply(simp only: Stknum_up)

apply(simp)

done

section  {* Standard Tapes *}

definition

  "right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"

definition

  "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"

lemma ww:

 "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> 

  (\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"

apply(rule iffI)

apply(erule exE)+

apply(simp)

apply(rule_tac x="k" in exI)

apply(auto)[1]

apply(simp add: nth_append)

apply(simp add: nth_append)

apply(erule exE)

apply(rule_tac x="i" in exI)

apply(rule_tac x="length tp - i" in exI)

apply(auto)

apply(rule sym)

apply(subst append_eq_conv_conj)

apply(simp)

apply(rule conjI)

apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)

by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)

lemma right_std:

  "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"

apply(simp only: ww)

apply(simp add: right_std_def)

apply(simp only: list_encode_inverse)

apply(simp)

apply(auto)

apply(rule_tac x="i" in exI)

apply(simp)

apply(rule conjI)

apply (metis Suc_eq_plus1 Suc_neq_Zero cellnum.cases cellnum.simps(1) leD less_trans linorder_neqE_nat)

apply(auto)

by (metis One_nat_def cellnum.cases cellnum.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)

lemma left_std:

  "(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"

apply(simp add: left_std_def)

apply(simp only: list_encode_inverse)

apply(simp)

apply(auto)

apply(rule_tac x="length tp" in exI)

apply(induct tp)

apply(simp)

apply(simp)

apply(auto)

apply(case_tac a)

apply(auto)

apply(case_tac a)

apply(auto)

by (metis Suc_less_eq nth_Cons_Suc)

section {* Standard- and Final Configurations, the Universal Function *}

text {*

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

  is a stardard tape. 

*}

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

  where

  "Std cf = (left_std (Left cf) \<and> right_std (Right cf))"

text{* 

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

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

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

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

  where

    "Final cf = (State cf = 0)"

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

  where

  "Stop m cf k = (Final (Steps cf m k) \<and> 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. Stop m cf k)"

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

  where

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

section {* The UF simulates Turing machines *}

lemma Update_left_simulate:

  shows "Newleft (Code_tp l) (Code_tp r) (actnum 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) (actnum 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 (cellnum 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> Action (Code_tprog tp) st (cellnum c) = actnum (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) = cellnum (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 cf" 

apply(case_tac cf)

apply(simp only: std_tape_def)

apply(simp only: Code_conf.simps)

apply(simp only: Conf.simps)

apply(simp only: Std.simps)

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

apply(simp only: list_encode_inverse)

apply(simp only: misc if_True)

apply(simp only: left_std[symmetric] right_std[symmetric])

apply(simp)

by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc)

lemma UF_simulate:

  assumes "tm_wf tm"

  shows "UF (Code_tprog tm) (Conf (Code_conf cf)) = 

  Stknum (Right (Conf 

  (Code_conf (steps cf tm (LEAST n. is_final (steps cf tm n) \<and> std_tape (steps cf tm n)))))) - 1" 

apply(simp only: UF.simps)

apply(subst Steps_simulate[symmetric, OF assms])

apply(subst Final_simulate[symmetric])

apply(subst Std_simulate[symmetric])

apply(simp only: Halt.simps)

apply(simp only: Steps_simulate[symmetric, OF assms])

apply(simp only: Stop.simps[symmetric])

done

section {* Universal Function as Recursive Functions *}

definition 

  "rec_read = CN rec_ldec [Id 1 0, constn 0]"

definition 

  "rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]"

definition

    "rec_newleft =

       (let cond0 = CN rec_eq [Id 3 2, constn 0] in 

        let cond1 = 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_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in

        CN rec_if [cond0, Id 3 0,

          CN rec_if [cond1, Id 3 0,  

            CN rec_if [cond2, CN rec_pdec2 [Id 3 0],

              CN rec_if [cond3, case3, Id 3 0]]]])"

definition

    "rec_newright =

       (let cond0 = CN rec_eq [Id 3 2, constn 0] in

        let cond1 = 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 case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in

        CN rec_if [cond0, CN rec_write [constn 0, Id 3 1], 

          CN rec_if [cond1, CN rec_write [constn 1, Id 3 1],

            CN rec_if [cond2, case2,

              CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])"

definition

  "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]])

                           (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))"

definition 

  "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in 

                 let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in

                 let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]

                 in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])"

definition

  "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]])

                              (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))"

definition

  "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in

                   let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]