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 {* Reading and writing the encoded tape *}

    63 

    64 fun Read where

    65   "Read tp = ldec tp 0"

    66 

    67 fun Write where

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

    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 l r a = (if a = 0 then l else 

    79                     if a = 1 then l else 

    80                     if a = 2 then pdec2 l else 

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

    82                     else l)"

    83 

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

    85   where

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

    87                       else if a = 1 then Write 1 r

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

    89                       else if a = 3 then pdec2 r

    90                       else r)"

    91 

    92 text {*

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

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

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

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

    97 *}

    98 

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

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

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

   102 

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

   104   where

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

   106 

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

   108   "newstate n 0 = pdec2 (pdec1 n)"

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

   110 

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

   112   where

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

   114 

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

   116   where

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

   118 

   119 fun State where

   120   "State cf = ldec cf 0"

   121 

   122 fun Left where

   123   "Left cf = ldec cf 1"

   124 

   125 fun Right where

   126   "Right cf = ldec cf 2"

   127 

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

   129   where

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

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

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

   133 

   134 text {*

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

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

   137 *}

   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 (Step cf p) p n"

   143 

   144 text {*

   145   Decoding tapes into binary or stroke numbers.

   146 *}

   147 

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

   149   where

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

   151 

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

   153   where

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

   155 

   156 lemma Binnum_simulate1:

   157   "(Binnum z = 0) \<longleftrightarrow> (\<forall>i \<in> {..<enclen z}. ldec z i = 0)"

   158 by(auto simp add: Binnum_def)

   159 

   160 lemma Binnum_simulate2:

   161   "(\<forall>i \<in> {..<enclen (Code_tp tp)}. ldec (Code_tp tp) i = 0) \<longleftrightarrow> (\<exists>k. tp = Bk \<up> k)"

   162 apply(induct tp)

   163 apply(simp)

   164 apply(simp)

   165 apply(simp add: lessThan_Suc)

   166 apply(case_tac a)

   167 apply(simp)

   168 defer

   169 apply(simp)

   170 oops

   171 

   172 apply(simp add: Binnum_def)

   173 

   174 text {*

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

   176   is a stardard tape. 

   177 *}

   178 

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

   180   where

   181   "Std cf = (Binnum (Left cf) = 0 \<and> 

   182             (\<exists>x\<le>(enclen (Right cf)). Binnum (Right cf) = 2 ^ x))"

   183 

   184 text{* 

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

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

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

   188 

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

   190   where

   191     "Final cf = (State cf = 0)"

   192 

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

   194   where

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

   196 

   197 text{*

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

   199   execute before reaching a stardard final configuration. This recursive 

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

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

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

   203 *}

   204 

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

   206   where

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

   208 

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

   210   where

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

   212 

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

   214 

   215 lemma Update_left_simulate:

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

   217 apply(induct a)

   218 apply(simp_all)

   219 apply(case_tac l)

   220 apply(simp_all)

   221 apply(case_tac r)

   222 apply(simp_all)

   223 done

   224 

   225 lemma Update_right_simulate:

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

   227 apply(induct a)

   228 apply(simp_all)

   229 apply(case_tac r)

   230 apply(simp_all)

   231 apply(case_tac r)

   232 apply(simp_all)

   233 apply(case_tac l)

   234 apply(simp_all)

   235 apply(case_tac r)

   236 apply(simp_all)

   237 done

   238 

   239 lemma Fetch_state_simulate:

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

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

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

   243 done

   244 

   245 lemma Fetch_action_simulate:

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

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

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

   249 done

   250 

   251 lemma Read_simulate:

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

   253 apply(case_tac tp)

   254 apply(simp_all)

   255 done

   256 

   257 lemma misc:

   258   "2 < (3::nat)"

   259   "1 < (3::nat)"

   260   "0 < (3::nat)" 

   261   "length [x] = 1"

   262   "length [x, y] = 2"

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

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

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

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

   267 apply(simp_all)

   268 done

   269 

   270 lemma Step_simulate:

   271   assumes "tm_wf tp"

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

   273 apply(subst step.simps) 

   274 apply(simp only: Let_def)

   275 apply(subst Step.simps)

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

   277 apply(simp only: list_encode_inverse)

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

   279 apply(simp only: prod_case_beta) 

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

   281 apply(simp only: State.simps)

   282 apply(simp only: list_encode_inverse)

   283 apply(simp only: misc if_True)

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

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

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

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

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

   289 apply(simp only: Code_conf.simps)

   290 apply(simp only: Conf.simps)

   291 apply(simp)

   292 done

   293 

   294 lemma Steps_simulate:

   295   assumes "tm_wf tp" 

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

   297 apply(induct n arbitrary: cf) 

   298 apply(simp)

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

   300 apply(case_tac cf)

   301 apply(simp only: )

   302 apply(subst Step_simulate)

   303 apply(rule assms)

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

   305 apply(simp)

   306 done

   307 

   308 lemma Final_simulate:

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

   310 by (case_tac cf) (simp)

   311 

   312 lemma Std_simulate:

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

   314 apply(case_tac cf)

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

   316 apply(subst Std.simps)

   317 

   318 (* UNTIL HERE *)

   319 

   320 

   321 section {* Universal Function as Recursive Functions *}

   322 

   323 definition 

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

   325 

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

   327   where

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

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

   330 

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

   332   where

   333   "rec_strt' xs 0 = Z"

   334 | "rec_strt' xs (Suc n) = 

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

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

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

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

   339 

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

   341   where

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

   343 

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

   345   where

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

   347 

   348 definition 

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

   350 

   351 definition

   352     "rec_newleft =

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

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

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

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

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

   358         CN rec_if [cond1, Id 3 0, 

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

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

   361 

   362 definition

   363     "rec_newright =

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

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

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

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

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

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

   370         CN rec_if [condn 0, case0, 

   371           CN rec_if [condn 1, case1,

   372             CN rec_if [condn 2, case2,

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

   374 

   375 definition 

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

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

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

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

   380 

   381 definition rec_newstat :: "recf"

   382   where

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

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

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

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

   387 

   388 definition 

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

   390 

   391 definition

   392   "rec_left = rec_pdec1"

   393 

   394 definition 

   395   "rec_right = CN rec_pdec2 [rec_pdec1]"

   396 

   397 definition 

   398   "rec_stat = CN rec_pdec2 [rec_pdec2]"

   399 

   400 definition 

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

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

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

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

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

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

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

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

   409 

   410 definition 

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

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

   413 

   414 definition 

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

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

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

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

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

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

   421 

   422 definition 

   423   "rec_nostop = CN rec_nstd [rec_conf]"

   424 

   425 definition 

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

   427 

   428 definition 

   429   "rec_halt = MN rec_nostop" 

   430 

   431 definition 

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

   433 

   434 

   435 

   436 section {* Correctness Proofs for Recursive Functions *}

   437 

   438 lemma entry_lemma [simp]:

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

   440 by(simp add: rec_entry_def)

   441 

   442 lemma listsum2_lemma [simp]: 

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

   444 by (induct n) (simp_all)

   445 

   446 lemma strt'_lemma [simp]:

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

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

   449 

   450 lemma map_suc:

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

   452 proof -

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

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

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

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

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

   458 qed

   459 

   460 lemma strt_lemma [simp]: 

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

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

   463 

   464 lemma scan_lemma [simp]: 

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

   466 by(simp add: rec_scan_def)

   467 

   468 lemma newleft_lemma [simp]:

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

   470 by (simp add: rec_newleft_def Let_def)

   471 

   472 lemma newright_lemma [simp]:

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

   474 by (simp add: rec_newright_def Let_def)

   475 

   476 lemma actn_lemma [simp]:

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

   478 by (simp add: rec_actn_def)

   479 

   480 lemma newstat_lemma [simp]: 

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

   482 by (simp add: rec_newstat_def)

   483 

   484 lemma trpl_lemma [simp]: 

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

   486 apply(simp)

   487 apply (simp add: rec_trpl_def)

   488 

   489 lemma left_lemma [simp]:

   490   "rec_eval rec_left [c] = Left c" 

   491 by(simp add: rec_left_def)

   492 

   493 lemma right_lemma [simp]:

   494   "rec_eval rec_right [c] = Right c" 

   495 by(simp add: rec_right_def)

   496 

   497 lemma stat_lemma [simp]:

   498   "rec_eval rec_stat [c] = Stat c" 

   499 by(simp add: rec_stat_def)

   500 

   501 lemma newconf_lemma [simp]: 

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

   503 by (simp add: rec_newconf_def Let_def)

   504 

   505 lemma conf_lemma [simp]: 

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

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

   508 

   509 lemma nstd_lemma [simp]:

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

   511 by(simp add: rec_nstd_def)

   512 

   513 lemma nostop_lemma [simp]:

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

   515 by (simp add: rec_nostop_def)

   516 

   517 lemma value_lemma [simp]:

   518   "rec_eval rec_value [x] = Value x"

   519 by (simp add: rec_value_def)

   520 

   521 lemma halt_lemma [simp]:

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

   523 by (simp add: rec_halt_def)

   524 

   525 lemma uf_lemma [simp]:

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

   527 by (simp add: rec_uf_def)

   528 

   529 

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

   531 

   532 lemma rec_step: 

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

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

   535 apply(cases c)

   536 apply(simp only: Trpl_code.simps)

   537 apply(simp only: Let_def step.simps)

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

   539 apply(simp only: prod.cases)

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

   541 apply(simp only: prod.cases)

   542 apply(simp only: Trpl_code.simps)

   543 apply(simp only: Newconf.simps)

   544 apply(simp only: Left.simps)

   545 oops

   546 

   547 lemma rec_steps:

   548   assumes "tm_wf0 tp"

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

   550 apply(induct stp)

   551 apply(simp)

   552 apply(simp)

   553 oops

   554 

   555 

   556 lemma F_correct: 

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

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

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

   560 proof -

   561   from least_steps[OF tm] 

   562   obtain stp_least where

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

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

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

   566   show ?thesis

   567     apply(simp only: uf_lemma)

   568     apply(simp only: UF.simps)

   569     apply(simp only: Halt.simps)

   570     oops

   571 

   572 

   573 end

   574