1 theory UF_Rec

     2 imports Recs Turing2

     3 begin

     4 

     5 section {* Coding of Turing Machines and tapes*}

     6 

     7 text {*

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

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

    10 

    11 text {* Encoding of actions as numbers *}

    12 

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

    14   where

    15   "action_num W0 = 0"

    16 | "action_num W1 = 1"

    17 | "action_num L  = 2"

    18 | "action_num R  = 3"

    19 | "action_num Nop = 4"

    20 

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

    22   "cell_num Bk = 0"

    23 | "cell_num Oc = 1"

    24 

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

    26   where

    27   "code_tp [] = []"

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

    29 

    30 fun Code_tp where

    31   "Code_tp tp = lenc (code_tp tp)"

    32 

    33 fun Code_conf where

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

    35 

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

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

    38   

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

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

    41 

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

    43   where

    44   "code_tprog [] =  []"

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

    46 

    47 lemma code_tprog_length [simp]:

    48   "length (code_tprog tp) = length tp"

    49 by (induct tp) (simp_all)

    50 

    51 lemma code_tprog_nth [simp]:

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

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

    54 

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

    56   where 

    57   "Code_tprog tm = lenc (code_tprog tm)"

    58 

    59 section {* Universal Function in HOL *}

    60 

    61 

    62 text {* Scanning and writing the right tape *}

    63 

    64 fun Scan where

    65   "Scan r = ldec r 0"

    66 

    67 fun Write where

    68   "Write n r = penc n (pdec2 r)"

    69 

    70 text {* 

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

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

    73   to an action @{text a}.

    74 *}

    75 

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

    77   where

    78   "Newleft p r a = (if a = 0 \<or> a = 1 then p else 

    79                     if a = 2 then pdec2 p else 

    80                     if a = 3 then penc (pdec1 r) p

    81                     else p)"

    82 

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

    84   where

    85   "Newright p r a  = (if a = 0 then Write 0 r

    86                       else if a = 1 then Write 1 r

    87                       else if a = 2 then penc (pdec1 p) r

    88                       else if a = 3 then pdec2 r

    89                       else r)"

    90 

    91 text {*

    92   The @{text "Actn"} function given on page 92 of B book, which is used to 

    93   fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is 

    94   the code of the Turing Machine, @{text "q"} is the current state of 

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

    96 *}

    97 

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

    99   "actn n 0 = pdec1 (pdec1 n)"

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

   101 

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

   103   where

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

   105 

   106 fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   107   "newstat n 0 = pdec2 (pdec1 n)"

   108 | "newstat n _ = pdec2 (pdec2 n)"

   109 

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

   111   where

   112   "Newstat m q r = (if q \<noteq> 0 then (newstat (ldec m (q - 1)) r) else 0)"

   113 

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

   115   where

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

   117 

   118 fun Stat where

   119   (*"Stat c = (if c = 0 then 0 else ldec c 0)"*)

   120   "Stat c = ldec c 0"

   121 

   122 fun Left where

   123   "Left c = ldec c 1"

   124 

   125 fun Right where

   126   "Right c = ldec c 2"

   127 

   128 fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"

   129   where

   130   "Newconf c m = Conf (Newstat m (Stat c) (Scan (Right c)), 

   131                        (Newleft (Left c) (Right c) (Actn m (Stat c) (Scan (Right c))),

   132                         Newright (Left c) (Right c) (Actn m (Stat c) (Scan (Right c)))))"

   133 

   134 text {*

   135   @{text "Step k m r"} computes the TM configuration after @{text "k"} steps of execution

   136   of TM coded as @{text "m"} starting from the initial configuration where the left 

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

   138 

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

   140   where

   141   "Steps cf p 0  = cf"

   142 | "Steps cf p (Suc n) = Steps (Newconf cf p) p n"

   143 

   144 text {*

   145   @{text "Nstd c"} returns true if the configuration coded 

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

   147 

   148 fun Nstd :: "nat \<Rightarrow> bool"

   149   where

   150   "Nstd c = (Stat c \<noteq> 0)"

   151 

   152 -- "tape conditions are missing"

   153 

   154 text{* 

   155   @{text "Nostop t m r"} means that afer @{text "t"} steps of 

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

   157   final configuration. *}

   158 

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

   160   where

   161   "Nostop m l r = Nstd (Conf (m, (l, r)))"

   162 

   163 text{*

   164   @{text "rec_halt"} is the recursive function calculating the steps a TM needs to 

   165   execute before to reach a stardard final configuration. This recursive function is 

   166   the only one using @{text "Mn"} combinator. So it is the only non-primitive recursive 

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

   168 *}

   169 

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

   171   where

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

   173 

   174 (*

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

   176   where

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

   178 *)

   179 

   180 text {* reading the value is missing *}

   181 

   182 section {* The UF can simulate Turing machines *}

   183 

   184 lemma Update_left_simulate:

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

   186 apply(induct a)

   187 apply(simp_all)

   188 apply(case_tac l)

   189 apply(simp_all)

   190 apply(case_tac r)

   191 apply(simp_all)

   192 done

   193 

   194 lemma Update_right_simulate:

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

   196 apply(induct a)

   197 apply(simp_all)

   198 apply(case_tac r)

   199 apply(simp_all)

   200 apply(case_tac r)

   201 apply(simp_all)

   202 apply(case_tac l)

   203 apply(simp_all)

   204 apply(case_tac r)

   205 apply(simp_all)

   206 done

   207 

   208 lemma Fetch_state_simulate:

   209   "\<lbrakk>tm_wf tp\<rbrakk> \<Longrightarrow> Newstat (Code_tprog tp) st (cell_num c) = snd (fetch tp st c)"

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

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

   212 done

   213 

   214 lemma Fetch_action_simulate:

   215   "\<lbrakk>tm_wf tp; st \<le> length tp\<rbrakk> \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"

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

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

   218 done

   219 

   220 lemma Scan_simulate:

   221   "Scan (Code_tp tp) = cell_num (read tp)"

   222 apply(case_tac tp)

   223 apply(simp_all)

   224 done

   225 

   226 lemma misc:

   227   "2 < (3::nat)"

   228   "1 < (3::nat)"

   229   "0 < (3::nat)" 

   230   "length [x] = 1"

   231   "length [x, y] = 2"

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

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

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

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

   236 apply(simp_all)

   237 done

   238 

   239 lemma New_conf_simulate:

   240   assumes "tm_wf tp" "st \<le> length tp"

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

   242 apply(subst step.simps) 

   243 apply(simp only: Let_def)

   244 apply(subst Newconf.simps)

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

   246 apply(simp only: list_encode_inverse)

   247 apply(simp only: misc if_True Code_tp.simps)

   248 apply(simp only: prod_case_beta) 

   249 apply(subst Fetch_state_simulate[OF assms, symmetric])

   250 apply(simp only: Stat.simps)

   251 apply(simp only: list_encode_inverse)

   252 apply(simp only: misc if_True)

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

   254 apply(simp only: Fetch_action_simulate[OF assms])

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

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

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

   258 apply(simp only: Code_conf.simps)

   259 apply(simp only: Conf.simps)

   260 apply(simp)

   261 done

   262 

   263 lemma Step_simulate:

   264   assumes "tm_wf tp" "fst cf \<le> length tp"

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

   266 apply(induct n arbitrary: cf) 

   267 apply(simp)

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

   269 apply(case_tac cf)

   270 apply(simp only: )

   271 apply(subst New_conf_simulate)

   272 apply(rule assms)

   273 defer

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

   275 apply(simp)

   276 

   277 

   278 section {* Coding of Turing Machines *}

   279 

   280 text {*

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

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

   283 

   284 fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat"

   285   where

   286   "bl2nat [] n = 0"

   287 | "bl2nat (Bk # bl) n = bl2nat bl (Suc n)"

   288 | "bl2nat (Oc # bl) n = 2 ^ n + bl2nat bl (Suc n)"

   289 

   290 fun bl2wc :: "cell list \<Rightarrow> nat"

   291   where

   292   "bl2wc xs = bl2nat xs 0"

   293 

   294 lemma bl2nat_double [simp]: 

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

   296 apply(induct xs arbitrary: n)

   297 apply(auto)

   298 apply(case_tac a)

   299 apply(auto)

   300 done

   301 

   302 lemma bl2nat_simps1 [simp]: 

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

   304 by (induct y) (auto)

   305 

   306 lemma bl2nat_simps2 [simp]: 

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

   308 apply(induct y)

   309 apply(auto)

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

   311 apply(auto)

   312 done

   313 

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

   315   where

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

   317 

   318 

   319 

   320 fun block_map :: "cell \<Rightarrow> nat"

   321   where

   322   "block_map Bk = 0"

   323 | "block_map Oc = 1"

   324 

   325 fun Goedel_code' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"

   326   where

   327   "Goedel_code' [] n = 1"

   328 | "Goedel_code' (x # xs) n = (Pi n) ^ x * Goedel_code' xs (Suc n) "

   329 

   330 fun Goedel_code :: "nat list \<Rightarrow> nat"

   331   where

   332   "Goedel_code xs = 2 ^ (length xs) * (Goedel_code' xs 1)"

   333 

   334 

   335 

   336 section {* Universal Function as Recursive Functions *}

   337 

   338 definition 

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

   340 

   341 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"

   342   where

   343   "rec_listsum2 vl 0 = CN Z [Id vl 0]"

   344 | "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"

   345 

   346 fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"

   347   where

   348   "rec_strt' xs 0 = Z"

   349 | "rec_strt' xs (Suc n) = 

   350       (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in

   351        let t1 = CN rec_power [constn 2, dbound] in

   352        let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in

   353        CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"

   354 

   355 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"

   356   where

   357   "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"

   358 

   359 fun rec_strt :: "nat \<Rightarrow> recf"

   360   where

   361   "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"

   362 

   363 definition 

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

   365 

   366 definition

   367     "rec_newleft =

   368        (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in

   369         let cond2 = CN rec_eq [Id 3 2, constn 2] in

   370         let cond3 = CN rec_eq [Id 3 2, constn 3] in

   371         let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], 

   372                                 CN rec_mod [Id 3 1, constn 2]] in

   373         CN rec_if [cond1, Id 3 0, 

   374           CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],

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

   376 

   377 definition

   378     "rec_newright =

   379        (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in

   380         let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in

   381         let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in

   382         let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     

   383                                 CN rec_mod [Id 3 0, constn 2]] in

   384         let case3 = CN rec_quo [Id 2 1, constn 2] in

   385         CN rec_if [condn 0, case0, 

   386           CN rec_if [condn 1, case1,

   387             CN rec_if [condn 2, case2,

   388               CN rec_if [condn 3, case3, Id 3 1]]]])"

   389 

   390 definition 

   391   "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in

   392                let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in

   393                let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]

   394                in CN rec_if [Id 3 1, entry, constn 4])"

   395 

   396 definition rec_newstat :: "recf"

   397   where

   398   "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in

   399                   let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in

   400                   let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]

   401                   in CN rec_if [Id 3 1, entry, Z])"

   402 

   403 definition 

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

   405 

   406 definition

   407   "rec_left = rec_pdec1"

   408 

   409 definition 

   410   "rec_right = CN rec_pdec2 [rec_pdec1]"

   411 

   412 definition 

   413   "rec_stat = CN rec_pdec2 [rec_pdec2]"

   414 

   415 definition 

   416   "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in

   417                   let left = CN rec_left [Id 2 1] in

   418                   let right = CN rec_right [Id 2 1] in

   419                   let stat = CN rec_stat [Id 2 1] in

   420                   let one = CN rec_newleft [left, right, act] in

   421                   let two = CN rec_newstat [Id 2 0, stat, right] in

   422                   let three = CN rec_newright [left, right, act]

   423                   in CN rec_trpl [one, two, three])" 

   424 

   425 definition 

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

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

   428 

   429 definition 

   430   "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in

   431                let disj2 = CN rec_noteq [rec_left, constn 0] in

   432                let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in

   433                let disj3 = CN rec_noteq [rec_right, rhs] in

   434                let disj4 = CN rec_eq [rec_right, constn 0] in

   435                CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"

   436 

   437 definition 

   438   "rec_nostop = CN rec_nstd [rec_conf]"

   439 

   440 definition 

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

   442 

   443 definition 

   444   "rec_halt = MN rec_nostop" 

   445 

   446 definition 

   447   "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"

   448 

   449 

   450 

   451 section {* Correctness Proofs for Recursive Functions *}

   452 

   453 lemma entry_lemma [simp]:

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

   455 by(simp add: rec_entry_def)

   456 

   457 lemma listsum2_lemma [simp]: 

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

   459 by (induct n) (simp_all)

   460 

   461 lemma strt'_lemma [simp]:

   462   "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"

   463 by (induct n) (simp_all add: Let_def)

   464 

   465 lemma map_suc:

   466   "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"

   467 proof -

   468   have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)

   469   then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp

   470   also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp

   471   also have "... = map Suc xs" by (simp add: map_nth)

   472   finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .

   473 qed

   474 

   475 lemma strt_lemma [simp]: 

   476   "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"

   477 by (simp add: comp_def map_suc[symmetric])

   478 

   479 lemma scan_lemma [simp]: 

   480   "rec_eval rec_scan [r] = r mod 2"

   481 by(simp add: rec_scan_def)

   482 

   483 lemma newleft_lemma [simp]:

   484   "rec_eval rec_newleft [p, r, a] = Newleft p r a"

   485 by (simp add: rec_newleft_def Let_def)

   486 

   487 lemma newright_lemma [simp]:

   488   "rec_eval rec_newright [p, r, a] = Newright p r a"

   489 by (simp add: rec_newright_def Let_def)

   490 

   491 lemma actn_lemma [simp]:

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

   493 by (simp add: rec_actn_def)

   494 

   495 lemma newstat_lemma [simp]: 

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

   497 by (simp add: rec_newstat_def)

   498 

   499 lemma trpl_lemma [simp]: 

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

   501 apply(simp)

   502 apply (simp add: rec_trpl_def)

   503 

   504 lemma left_lemma [simp]:

   505   "rec_eval rec_left [c] = Left c" 

   506 by(simp add: rec_left_def)

   507 

   508 lemma right_lemma [simp]:

   509   "rec_eval rec_right [c] = Right c" 

   510 by(simp add: rec_right_def)

   511 

   512 lemma stat_lemma [simp]:

   513   "rec_eval rec_stat [c] = Stat c" 

   514 by(simp add: rec_stat_def)

   515 

   516 lemma newconf_lemma [simp]: 

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

   518 by (simp add: rec_newconf_def Let_def)

   519 

   520 lemma conf_lemma [simp]: 

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

   522 by(induct k) (simp_all add: rec_conf_def)

   523 

   524 lemma nstd_lemma [simp]:

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

   526 by(simp add: rec_nstd_def)

   527 

   528 lemma nostop_lemma [simp]:

   529   "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" 

   530 by (simp add: rec_nostop_def)

   531 

   532 lemma value_lemma [simp]:

   533   "rec_eval rec_value [x] = Value x"

   534 by (simp add: rec_value_def)

   535 

   536 lemma halt_lemma [simp]:

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

   538 by (simp add: rec_halt_def)

   539 

   540 lemma uf_lemma [simp]:

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

   542 by (simp add: rec_uf_def)

   543 

   544 

   545 subsection {* Relating interperter functions to the execution of TMs *}

   546 

   547 lemma rec_step: 

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

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

   550 apply(cases c)

   551 apply(simp only: Trpl_code.simps)

   552 apply(simp only: Let_def step.simps)

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

   554 apply(simp only: prod.cases)

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

   556 apply(simp only: prod.cases)

   557 apply(simp only: Trpl_code.simps)

   558 apply(simp only: Newconf.simps)

   559 apply(simp only: Left.simps)

   560 oops

   561 

   562 lemma rec_steps:

   563   assumes "tm_wf0 tp"

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

   565 apply(induct stp)

   566 apply(simp)

   567 apply(simp)

   568 oops

   569 

   570 

   571 lemma F_correct: 

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

   573   and     wf:  "tm_wf0 tp" "0 < rs"

   574   shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"

   575 proof -

   576   from least_steps[OF tm] 

   577   obtain stp_least where

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

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

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

   581   show ?thesis

   582     apply(simp only: uf_lemma)

   583     apply(simp only: UF.simps)

   584     apply(simp only: Halt.simps)

   585     oops

   586 

   587 

   588 end

   589