section {* Universal Function in HOL *}

  B book, but this definition generalises the original one in order to deal 

  with multiple input arguments. *}

  Turing Machine, @{text "r"} is the right number of Turing Machine tape. *}

lemma mod_dvd_simp: 

  "(x mod y = (0::nat)) = (y dvd x)"

by(auto simp add: dvd_def)

lemma Trpl_Left [simp]:

  "Left (Trpl p q r) = p"

apply(simp)

apply(subst Lo_def)

apply(subst dvd_eq_mod_eq_0[symmetric])

apply(simp)

apply(auto)

thm Lo_def

thm mod_dvd_simp

apply(simp add: left.simps trpl.simps lo.simps 

              loR.simps mod_dvd_simp, auto simp: conf_decode1)

apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r",

      auto)

apply(erule_tac x = l in allE, auto)

  number equals @{text "0"}, right number equals @{text "r"}. *}

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

  execution the TM coded by @{text "m"} is not at a stardard 

  final configuration. *}

  needs to be used in the construction of the universal function @{text "rec_uf"}. *}

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

  where

  "Halt m r = (LEAST t. \<not> Nostop t m r)"

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

  where

  "UF c m = Value (Right (Conf (Halt c m) c m))"

section {* Coding of Turing Machines *}

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

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

lemma bl2nat_double [simp]: 

  "bl2nat xs (Suc n) = 2 * bl2nat xs n"

apply(induct xs arbitrary: n)

apply(auto)

apply(case_tac a)

apply(auto)

done

lemma bl2nat_simps1 [simp]: 

  shows "bl2nat (Bk \<up> y) n = 0"

by (induct y) (auto)

lemma bl2nat_simps2 [simp]: 

  shows "bl2nat (Oc \<up> y) 0 = 2 ^ y - 1"

apply(induct y)

apply(auto)

apply(case_tac "(2::nat)^ y")

apply(auto)

done

fun Trpl_code :: "config \<Rightarrow> nat"

  "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"

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

definition

  "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"

definition 

  "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"

definition 

  "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"

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

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

section {* Correctness Proofs for Recursive Functions *}

lemma entry_lemma [simp]:

  "rec_eval rec_entry [sr, i] = Entry sr i"

by(simp add: rec_entry_def)

lemma listsum2_lemma [simp]: 

  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"

by (induct n) (simp_all)

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

lemma scan_lemma [simp]: 

  "rec_eval rec_scan [r] = r mod 2"

by(simp add: rec_scan_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 actn_lemma [simp]:

  "rec_eval rec_actn [m, q, r] = Actn m q r"

by (simp add: rec_actn_def)

lemma newstat_lemma [simp]: 

  "rec_eval rec_newstat [m, q, r] = Newstat m q r"

by (simp add: rec_newstat_def)

lemma trpl_lemma [simp]: 

  "rec_eval rec_trpl [p, q, r] = Trpl p q r"

by (simp add: rec_trpl_def)

lemma left_lemma [simp]:

  "rec_eval rec_left [c] = Left c" 

by(simp add: rec_left_def)

lemma right_lemma [simp]:

  "rec_eval rec_right [c] = Right c" 

by(simp add: rec_right_def)

lemma stat_lemma [simp]:

  "rec_eval rec_stat [c] = Stat c" 

by(simp add: rec_stat_def)

lemma newconf_lemma [simp]: 

  "rec_eval rec_newconf [m, c] = Newconf m c"

by (simp add: rec_newconf_def Let_def)

lemma conf_lemma [simp]: 

  "rec_eval rec_conf [k, m, r] = Conf k m r"

by(induct k) (simp_all add: rec_conf_def)

lemma nstd_lemma [simp]:

  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"

by(simp add: rec_nstd_def)

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)

lemma value_lemma [simp]:

  "rec_eval rec_value [x] = Value x"

by (simp add: rec_value_def)

lemma halt_lemma [simp]:

  "rec_eval rec_halt [m, r] = Halt m r"

by (simp add: rec_halt_def)

lemma uf_lemma [simp]:

  "rec_eval rec_uf [m, r] = UF m r"

by (simp add: rec_uf_def)

lemma rec_step: 

  assumes "(\<lambda> (s, l, r). s \<le> length tp div 2) c"

  shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)"

apply(cases c)

apply(simp only: Trpl_code.simps)

apply(simp only: Let_def step.simps)

apply(case_tac "fetch tp (a - 0) (read ca)")

apply(simp only: prod.cases)

apply(case_tac "update aa (b, ca)")

apply(simp only: prod.cases)

apply(simp only: Trpl_code.simps)

apply(simp only: Newconf.simps)

apply(simp only: Left.simps)

oops

lemma rec_steps:

  assumes "tm_wf0 tp"

  shows "Trpl_code (steps0 (1, Bk \<up> l, <lm>) tp stp) = Conf stp (Code tp) (bl2wc (<lm>))"

apply(induct stp)

apply(simp)

apply(simp)

oops

  assumes tm: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"

proof -

  from least_steps[OF tm] 

  obtain stp_least where

    before: "\<forall>stp' < stp_least. \<not> is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" and

    after:  "\<forall>stp' \<ge> stp_least. is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" by blast

  have "Halt (Code tp) (bl2wc (<lm>)) = stp_least" sorry

  show ?thesis

    apply(simp only: uf_lemma)

    apply(simp only: UF.simps)

    apply(simp only: Halt.simps)

    oops