theory UF_Rec
imports Recs Hoare_tm3
begin

section {* Coding of Turing Machines and Tapes*}


fun actenc :: "action \<Rightarrow> nat"
  where
  "actenc W0 = 0"
| "actenc W1 = 1"
| "actenc L  = 2"
| "actenc R  = 3"

fun cellenc :: "Block \<Rightarrow> nat" where
  "cellenc Bk = 0"
| "cellenc Oc = 1"


text {* Coding tapes *}

definition 
  "intenc i \<equiv> (if (0 \<le> i) then penc 0 (nat i) else penc 1 (nat (-i)))" 

definition
  "intdec n \<equiv> (if (0 = pdec1 n) then (int (pdec2 n)) else -(int (pdec2 n)))"

definition 
  tapeenc :: "(int f\<rightharpoonup> Block) \<Rightarrow> nat"
where
  "tapeenc tp = lenc (map (\<lambda>(x, y). penc (intenc x) (cellenc y)) (fmap_to_alist tp))"

fun 
  instenc :: "tm_inst \<Rightarrow> nat"
where
  "instenc ((a1, s1), (a2, s2)) = lenc [actenc a1, s1, actenc a2, s2]"

definition 
  progenc :: "(nat f\<rightharpoonup> tm_inst) \<Rightarrow> nat"
where
  "progenc p = lenc (map (\<lambda>(x, y). penc x (instenc y)) (fmap_to_alist p))"

text {* Coding Configurations of TMs *}

fun confenc where
  "confenc (faults, prog, s, pos, tp) = lenc [faults, progenc prog, s, intenc pos, tapeenc tp]"

section {* A Universal Function in HOL *}

fun Step :: "nat \<Rightarrow> nat"
  where
  "Step cf = 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))))"


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]
                   in CN rec_if [cond, if_branch, Z])"

definition
  "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]"

definition 
  "rec_state = CN rec_ldec [Id 1 0, Z]"

definition
  "rec_left = CN rec_ldec [Id 1 0, constn 1]"

definition 
  "rec_right = CN rec_ldec [Id 1 0, constn 2]"

definition 
  "rec_step = (let left = CN rec_left [Id 2 0] in
               let right = CN rec_right [Id 2 0] in
               let state = CN rec_state [Id 2 0] in
               let read = CN rec_read [right] in
               let action = CN rec_action [Id 2 1, state, read] in
               let newstate = CN rec_newstate [Id 2 1, state, read] in
               let newleft = CN rec_newleft [left, right, action] in
               let newright = CN rec_newright [left, right, action] 
               in CN rec_conf [newstate, newleft, newright])" 

definition 
  "rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])"

definition
  "rec_stknum = CN rec_minus 
                  [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
                   CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"

definition
  "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
                    let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in
                    let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
                    let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
                    let cond3 = CN (rec_all2_less 
                                     (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) 
                                [bound2, Id 2 0, Id 2 1] in
                    CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])"

definition
  "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
                   in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"

definition
  "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
                          CN rec_right_std [CN rec_right [Id 1 0]]]"

definition 
  "rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]"

definition 
  "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
               CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"

definition
  "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"

definition 
  "rec_uf = CN rec_pred 
              [CN rec_stknum 
                  [CN rec_right 
                     [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"

lemma read_lemma [simp]:
  "rec_eval rec_read [x] = Read x"
by (simp add: rec_read_def)

lemma write_lemma [simp]:
  "rec_eval rec_write [x, y] = Write x y"
by (simp add: rec_write_def)

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)

lemma act_lemma [simp]:
  "rec_eval rec_actn [n, c] = Actn n c"
apply(simp add: rec_actn_def)
apply(case_tac c)
apply(simp_all)
done

lemma action_lemma [simp]:
  "rec_eval rec_action [m, q, c] = Action m q c"
by (simp add: rec_action_def)

lemma newstat_lemma [simp]:
  "rec_eval rec_newstat [n, c] = Newstat n c"
apply(simp add: rec_newstat_def)
apply(case_tac c)
apply(simp_all)
done

lemma newstate_lemma [simp]:
  "rec_eval rec_newstate [m, q, r] = Newstate m q r"
by (simp add: rec_newstate_def)

lemma conf_lemma [simp]:
  "rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
by(simp add: rec_conf_def)

lemma state_lemma [simp]:
  "rec_eval rec_state [cf] = State cf"
by (simp add: rec_state_def)

lemma left_lemma [simp]:
  "rec_eval rec_left [cf] = Left cf"
by (simp add: rec_left_def)

lemma right_lemma [simp]:
  "rec_eval rec_right [cf] = Right cf"
by (simp add: rec_right_def)

lemma step_lemma [simp]:
  "rec_eval rec_step [cf, m] = Step cf m"
by (simp add: Let_def rec_step_def)

lemma steps_lemma [simp]:
  "rec_eval rec_steps [n, cf, p] = Steps cf p n"
by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)

lemma stknum_lemma [simp]:
  "rec_eval rec_stknum [z] = Stknum z"
by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])

lemma left_std_lemma [simp]:
  "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
by (simp add: Let_def rec_left_std_def left_std_def)

lemma right_std_lemma [simp]:
  "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
by (simp add: Let_def rec_right_std_def right_std_def)

lemma std_lemma [simp]:
  "rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
by (simp add: rec_std_def)

lemma final_lemma [simp]:
  "rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
by (simp add: rec_final_def)

lemma stop_lemma [simp]:
  "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
by (simp add: Let_def rec_stop_def)

lemma halt_lemma [simp]:
  "rec_eval rec_halt [m, cf] = Halt m cf"
by (simp add: rec_halt_def del: Stop.simps)

lemma uf_lemma [simp]:
  "rec_eval rec_uf [m, cf] = UF m cf"
by (simp add: rec_uf_def)

(* value "size rec_uf" *)
end