
diff -r 6e7244ae43b8 -r 745547bdc1c7 thys/UF_Rec.thy
--- a/thys/UF_Rec.thy	Thu May 02 13:19:50 2013 +0100
+++ b/thys/UF_Rec.thy	Thu May 09 18:16:36 2013 +0100
@@ -2,11 +2,11 @@
 imports Recs Turing_Hoare
 begin
 
-section {* Universal Function *}
 
 
 
-text{* coding of the configuration *}
+
+section {* Universal Function in HOL *}
 
 text {*
   @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural 
@@ -15,33 +15,16 @@
 fun Entry where
   "Entry sr i = Lo sr (Pi (Suc i))"
 
-definition 
-  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
-
-lemma entry_lemma [simp]:
-  "rec_eval rec_entry [sr, i] = Entry sr i"
-by(simp add: rec_entry_def)
-
-
 fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Listsum2 xs 0 = 0"
 | "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"
 
-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]"
-
-lemma listsum2_lemma [simp]: 
-  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
-by (induct n) (simp_all)
-
 text {*
   @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the 
-  B book, but this definition generalises the original one to deal with multiple 
-  input arguments.
-  *}
+  B book, but this definition generalises the original one in order to deal 
+  with multiple input arguments. *}
+
 fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Strt' xs 0 = 0"
@@ -52,55 +35,11 @@
   where
   "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"
 
-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)"
-
-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])
-
-
 text {* The @{text "Scan"} function on page 90 of B book. *}
 fun Scan :: "nat \<Rightarrow> nat"
   where
   "Scan r = r mod 2"
 
-definition 
-  "rec_scan = CN rec_mod [Id 1 0, constn 2]"
-
-lemma scan_lemma [simp]: 
-  "rec_eval rec_scan [r] = r mod 2"
-by(simp add: rec_scan_def)
-
 text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *}
 
 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -118,119 +57,52 @@
                       else if a = 3 then r div 2
                       else r)"
 
-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]]]])"
-
-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)
-
 text {*
   The @{text "Actn"} function given on page 92 of B book, which is used to 
   fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is 
   the Goedel coding of a Turing Machine, @{text "q"} is the current state of 
-  Turing Machine, @{text "r"} is the right number of Turing Machine tape.
-  *}
+  Turing Machine, @{text "r"} is the right number of Turing Machine tape. *}
+
 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)"
 
-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])"
-
-lemma actn_lemma [simp]:
-  "rec_eval rec_actn [m, q, r] = Actn m q r"
-by (simp add: rec_actn_def)
-
 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)"
 
-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])"
-
-lemma newstat_lemma [simp]: 
-  "rec_eval rec_newstat [m, q, r] = Newstat m q r"
-by (simp add: rec_newstat_def)
-
-
 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
 
-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]]"
-
-lemma trpl_lemma [simp]: 
-  "rec_eval rec_trpl [p, q, r] = Trpl p q r"
-by (simp add: rec_trpl_def)
-
-
-
 fun Left where
   "Left c = Lo c (Pi 0)"
 
-definition
-  "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"
-
-lemma left_lemma [simp]:
-  "rec_eval rec_left [c] = Left c" 
-by(simp add: rec_left_def)
-
 fun Right where
   "Right c = Lo c (Pi 2)"
 
-definition 
-  "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"
-
-lemma right_lemma [simp]:
-  "rec_eval rec_right [c] = Right c" 
-by(simp add: rec_right_def)
-
 fun Stat where
   "Stat c = Lo c (Pi 1)"
 
-definition 
-  "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"
+lemma mod_dvd_simp: 
+  "(x mod y = (0::nat)) = (y dvd x)"
+by(auto simp add: dvd_def)
 
-lemma stat_lemma [simp]:
-  "rec_eval rec_stat [c] = Stat c" 
-by(simp add: rec_stat_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)
+
 
 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
   where
@@ -242,43 +114,20 @@
                       (Newstat m (Stat c) (Right c)) 
                       (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))"
 
-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])" 
-
-lemma newconf_lemma [simp]: 
-  "rec_eval rec_newconf [m, c] = Newconf m c"
-by (simp add: rec_newconf_def Let_def)
-
 text {*
   @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution
   of TM coded as @{text "m"} starting from the initial configuration where the left 
-  number equals @{text "0"}, right number equals @{text "r"}. 
-  *}
+  number equals @{text "0"}, right number equals @{text "r"}. *}
+
 fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
   "Conf 0 m r  = Trpl 0 1 r"
 | "Conf (Suc k) m r = Newconf m (Conf k m r)"
 
-definition 
-  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
-                 (CN rec_newconf [Id 4 2 , Id 4 1])"
-
-lemma conf_lemma [simp]: 
-  "rec_eval rec_conf [k, m, r] = Conf k m r"
-by(induct k) (simp_all add: rec_conf_def)
-
-
 text {*
   @{text "Nstd c"} returns true if the configuration coded 
-  by @{text "c"} is not a stardard final configuration.
-  *}
+  by @{text "c"} is not a stardard final configuration. *}
+
 fun Nstd :: "nat \<Rightarrow> bool"
   where
   "Nstd c = (Stat c \<noteq> 0 \<or> 
@@ -286,70 +135,39 @@
              Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> 
              Right c = 0)"
 
-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])"
-
-lemma nstd_lemma [simp]:
-  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
-by(simp add: rec_nstd_def)
-
 
 text{* 
   @{text "Nostop t m r"} means that afer @{text "t"} steps of 
-  execution, the TM coded by @{text "m"} is not at a stardard 
-  final configuration.
-  *}
+  execution the TM coded by @{text "m"} is not at a stardard 
+  final configuration. *}
+
 fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   where
   "Nostop t m r = Nstd (Conf t m r)"
 
-definition 
-  "rec_nostop = CN rec_nstd [rec_conf]"
-
-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)
-
-
 fun Value where
   "Value x = (Lg (Suc x) 2) - 1"
 
-definition 
-  "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
-
-lemma value_lemma [simp]:
-  "rec_eval rec_value [x] = Value x"
-by (simp add: rec_value_def)
-
 text{*
   @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before
   to reach a stardard final configuration. This recursive function is the only one
   using @{text "Mn"} combinator. So it is the only non-primitive recursive function 
-  needs to be used in the construction of the universal function @{text "rec_uf"}.
-  *}
+  needs to be used in the construction of the universal function @{text "rec_uf"}. *}
 
-definition 
-  "rec_halt = MN rec_nostop" 
+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))"
 
 
-definition 
-  "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
+section {* Coding of Turing Machines *}
 
 text {*
-  The correctness of @{text "rec_uf"}, nonhalt case.
-  *}
-
-subsection {* Coding function of TMs *}
-
-text {*
-  The purpose of this section is to get the coding function of Turing Machine, 
-  which is going to be named @{text "code"}.
-  *}
+  The purpose of this section is to construct the coding function of Turing 
+  Machine, which is going to be named @{text "code"}. *}
 
 fun bl2nat :: "cell list \<Rightarrow> nat \<Rightarrow> nat"
   where
@@ -361,9 +179,29 @@
   where
   "bl2wc xs = bl2nat xs 0"
 
-fun trpl_code :: "config \<Rightarrow> nat"
+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"
   where
-  "trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
+  "Trpl_code (st, l, r) = Trpl (bl2wc l) st (bl2wc r)"
 
 fun action_map :: "action \<Rightarrow> nat"
   where
@@ -405,13 +243,259 @@
   where 
   "Code tp = Goedel_code (modify_tprog tp)"
 
+
+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)
+
+
 subsection {* Relating interperter functions to the execution of TMs *}
 
+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
+
 
 lemma F_correct: 
-  assumes tp: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"
+  assumes tm: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"
   and     wf:  "tm_wf0 tp" "0 < rs"
   shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"
+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
 
 
 end




