theory UTM

imports Main uncomputable recursive abacus UF GCD 

begin

section {* Wang coding of input arguments *}

text {*

  The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,

  where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape. 

  (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may

  very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential 

  composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple 

  input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second

  argument. 

  However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive 

  function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into 

  Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.

*}

definition rec_twice :: "recf"

  where

  "rec_twice = Cn 1 rec_mult [id 1 0, constn 2]"

definition rec_fourtimes  :: "recf"

  where

  "rec_fourtimes = Cn 1 rec_mult [id 1 0, constn 4]"

definition abc_twice :: "abc_prog"

  where

  "abc_twice = (let (aprog, ary, fp) = rec_ci rec_twice in 

                       aprog [+] dummy_abc ((Suc 0)))"

definition abc_fourtimes :: "abc_prog"

  where

  "abc_fourtimes = (let (aprog, ary, fp) = rec_ci rec_fourtimes in 

                       aprog [+] dummy_abc ((Suc 0)))"

definition twice_ly :: "nat list"

  where

  "twice_ly = layout_of abc_twice"

definition fourtimes_ly :: "nat list"

  where

  "fourtimes_ly = layout_of abc_fourtimes"

definition t_twice :: "tprog"

  where

  "t_twice = change_termi_state (tm_of (abc_twice) @ (tMp 1 (start_of twice_ly (length abc_twice) - Suc 0)))"

definition t_fourtimes :: "tprog"

  where

  "t_fourtimes = change_termi_state (tm_of (abc_fourtimes) @ 

             (tMp 1 (start_of fourtimes_ly (length abc_fourtimes) - Suc 0)))"

definition t_twice_len :: "nat"

  where

  "t_twice_len = length t_twice div 2"

definition t_wcode_main_first_part:: "tprog"

  where

  "t_wcode_main_first_part \<equiv> 

                   [(L, 1), (L, 2), (L, 7), (R, 3),

                    (R, 4), (W0, 3), (R, 4), (R, 5),

                    (W1, 6), (R, 5), (R, 13), (L, 6),

                    (R, 0), (R, 8), (R, 9), (Nop, 8),

                    (R, 10), (W0, 9), (R, 10), (R, 11), 

                    (W1, 12), (R, 11), (R, t_twice_len + 14), (L, 12)]"

definition t_wcode_main :: "tprog"

  where

  "t_wcode_main = (t_wcode_main_first_part @ tshift t_twice 12 @ [(L, 1), (L, 1)]

                    @ tshift t_fourtimes (t_twice_len + 13) @ [(L, 1), (L, 1)])"

fun bl_bin :: "block list \<Rightarrow> nat"

  where

  "bl_bin [] = 0" 

| "bl_bin (Bk # xs) = 2 * bl_bin xs"

| "bl_bin (Oc # xs) = Suc (2 * bl_bin xs)"

declare bl_bin.simps[simp del]

type_synonym bin_inv_t = "block list \<Rightarrow> nat \<Rightarrow> tape \<Rightarrow> bool"

fun wcode_before_double :: "bin_inv_t"

  where

  "wcode_before_double ires rs (l, r) =

     (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

               r = Oc\<^bsup>(Suc (Suc rs))\<^esup> @ Bk\<^bsup>rn \<^esup>)"

declare wcode_before_double.simps[simp del]

fun wcode_after_double :: "bin_inv_t"

  where

  "wcode_after_double ires rs (l, r) = 

     (\<exists> ln rn. l = Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

         r = Oc\<^bsup>Suc (Suc (Suc 2*rs))\<^esup> @ Bk\<^bsup>rn\<^esup>)"

declare wcode_after_double.simps[simp del]

fun wcode_on_left_moving_1_B :: "bin_inv_t"

  where

  "wcode_on_left_moving_1_B ires rs (l, r) = 

     (\<exists> ml mr rn. l = Bk\<^bsup>ml\<^esup> @ Oc # Oc # ires \<and> 

               r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

               ml + mr > Suc 0 \<and> mr > 0)"

declare wcode_on_left_moving_1_B.simps[simp del]

fun wcode_on_left_moving_1_O :: "bin_inv_t"

  where

  "wcode_on_left_moving_1_O ires rs (l, r) = 

     (\<exists> ln rn.

               l = Oc # ires \<and> 

               r = Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

declare wcode_on_left_moving_1_O.simps[simp del]

fun wcode_on_left_moving_1 :: "bin_inv_t"

  where

  "wcode_on_left_moving_1 ires rs (l, r) = 

          (wcode_on_left_moving_1_B ires rs (l, r) \<or> wcode_on_left_moving_1_O ires rs (l, r))"

declare wcode_on_left_moving_1.simps[simp del]

fun wcode_on_checking_1 :: "bin_inv_t"

  where

   "wcode_on_checking_1 ires rs (l, r) = 

    (\<exists> ln rn. l = ires \<and>

              r = Oc # Oc # Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

fun wcode_erase1 :: "bin_inv_t"

  where

"wcode_erase1 ires rs (l, r) = 

       (\<exists> ln rn. l = Oc # ires \<and> 

                 tl r = Bk\<^bsup>ln\<^esup> @ Bk # Bk # Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup>)"

declare wcode_erase1.simps [simp del]

fun wcode_on_right_moving_1 :: "bin_inv_t"

  where

  "wcode_on_right_moving_1 ires rs (l, r) = 

       (\<exists> ml mr rn.        

             l = Bk\<^bsup>ml\<^esup> @ Oc # ires \<and> 

             r = Bk\<^bsup>mr\<^esup> @ Oc\<^bsup>Suc rs\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

             ml + mr > Suc 0)"

declare wcode_on_right_moving_1.simps [simp del] 

declare wcode_on_right_moving_1.simps[simp del]

fun wcode_goon_right_moving_1 :: "bin_inv_t"

  where

  "wcode_goon_right_moving_1 ires rs (l, r) = 

      (\<exists> ml mr ln rn. 

            l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

            r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

            ml + mr = Suc rs)"

declare wcode_goon_right_moving_1.simps[simp del]

fun wcode_backto_standard_pos_B :: "bin_inv_t"

  where

  "wcode_backto_standard_pos_B ires rs (l, r) = 

          (\<exists> ln rn. l =  Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and> 

               r =  Bk # Oc\<^bsup>(Suc (Suc rs))\<^esup> @ Bk\<^bsup>rn \<^esup>)"

declare wcode_backto_standard_pos_B.simps[simp del]

fun wcode_backto_standard_pos_O :: "bin_inv_t"

  where

   "wcode_backto_standard_pos_O ires rs (l, r) = 

        (\<exists> ml mr ln rn. 

            l = Oc\<^bsup>ml\<^esup> @ Bk # Bk # Bk\<^bsup>ln\<^esup> @ Oc # ires \<and>

            r = Oc\<^bsup>mr\<^esup> @ Bk\<^bsup>rn\<^esup> \<and>

            ml + mr = Suc (Suc rs) \<and> mr > 0)"

declare wcode_backto_standard_pos_O.simps[simp del]

fun wcode_backto_standard_pos :: "bin_inv_t"

  where

  "wcode_backto_standard_pos ires rs (l, r) = (wcode_backto_standard_pos_B ires rs (l, r) \<or>

                                            wcode_backto_standard_pos_O ires rs (l, r))"

declare wcode_backto_standard_pos.simps[simp del]

lemma [simp]: "<0::nat> = [Oc]"

apply(simp add: tape_of_nat_abv exponent_def tape_of_nat_list.simps)

done

lemma tape_of_Suc_nat: "<Suc (a ::nat)> = replicate a Oc @ [Oc, Oc]"

apply(simp add: tape_of_nat_abv exp_ind tape_of_nat_list.simps)

apply(simp only: exp_ind_def[THEN sym])

apply(simp only: exp_ind, simp, simp add: exponent_def)

done

lemma [simp]: "length (<a::nat>) = Suc a"

apply(simp add: tape_of_nat_abv tape_of_nat_list.simps)

done

lemma [simp]: "<[a::nat]> = <a>"

apply(simp add: tape_of_nat_abv tape_of_nl_abv exponent_def

                tape_of_nat_list.simps)

done

lemma bin_wc_eq: "bl_bin xs = bl2wc xs"

proof(induct xs)

  show " bl_bin [] = bl2wc []" 

    apply(simp add: bl_bin.simps)

    done

next

  fix a xs

  assume "bl_bin xs = bl2wc xs"

  thus " bl_bin (a # xs) = bl2wc (a # xs)"

    apply(case_tac a, simp_all add: bl_bin.simps bl2wc.simps)

    apply(simp_all add: bl2nat.simps bl2nat_double)

    done

qed

declare exp_def[simp del]

lemma bl_bin_nat_Suc:  

  "bl_bin (<Suc a>) = bl_bin (<a>) + 2^(Suc a)"

apply(simp add: tape_of_nat_abv bin_wc_eq)

apply(simp add: bl2wc.simps)

done

lemma [simp]: " rev (a\<^bsup>aa\<^esup>) = a\<^bsup>aa\<^esup>"

apply(simp add: exponent_def)

done

declare tape_of_nl_abv_cons[simp del]

lemma tape_of_nl_rev: "rev (<lm::nat list>) = (<rev lm>)"

apply(induct lm rule: list_tl_induct, simp)

apply(case_tac "list = []", simp add: tape_of_nl_abv tape_of_nat_list.simps)

apply(simp add: tape_of_nat_list_butlast_last tape_of_nl_abv_cons)

done

lemma [simp]: "a\<^bsup>Suc 0\<^esup> = [a]" 

by(simp add: exp_def)

lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<^bsup>Suc a\<^esup> @ Bk # (<xs@ [b]>))"

apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps)

apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps)

done

lemma bl_bin_bk_oc[simp]:

  "bl_bin (xs @ [Bk, Oc]) = 

  bl_bin xs + 2*2^(length xs)"

apply(simp add: bin_wc_eq)

using bl2nat_cons_oc[of "xs @ [Bk]"]

apply(simp add: bl2nat_cons_bk bl2wc.simps)

done

lemma tape_of_nat[simp]: "(<a::nat>) = Oc\<^bsup>Suc a\<^esup>"

apply(simp add: tape_of_nat_abv)

done

lemma tape_of_nl_cons_app2: "(<c # xs @ [b]>) = (<c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>)"

proof(induct "length xs" arbitrary: xs c,

  simp add: tape_of_nl_abv  tape_of_nat_list.simps)

  fix x xs c

  assume ind: "\<And>xs c. x = length xs \<Longrightarrow> <c # xs @ [b]> = 

    <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

    and h: "Suc x = length (xs::nat list)" 

  show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

  proof(case_tac xs, simp add: tape_of_nl_abv  tape_of_nat_list.simps)

    fix a list

    assume g: "xs = a # list"

    hence k: "<a # list @ [b]> =  <a # list> @ Bk # Oc\<^bsup>Suc b\<^esup>"

      apply(rule_tac ind)

      using h

      apply(simp)

      done

    from g and k show "<c # xs @ [b]> = <c # xs> @ Bk # Oc\<^bsup>Suc b\<^esup>"

      apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

      done

  qed

qed

lemma [simp]: "length (<aa # a # list>) = Suc (Suc aa) + length (<a # list>)"

apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

done

lemma [simp]: "bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista) @ [Bk, Oc]) =

              bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)) + 

              2* 2^(length (Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)))"

using bl_bin_bk_oc[of "Oc\<^bsup>Suc aa\<^esup> @ Bk # tape_of_nat_list (a # lista)"]

apply(simp)

done

lemma [simp]: 

  "bl_bin (<aa # list>) + (4 * rs + 4) * 2 ^ (length (<aa # list>) - Suc 0)

  = bl_bin (Oc\<^bsup>Suc aa\<^esup> @ Bk # <list @ [0]>) + rs * (2 * 2 ^ (aa + length (<list @ [0]>)))"

apply(case_tac "list", simp add: add_mult_distrib, simp)

apply(simp add: tape_of_nl_cons_app2 add_mult_distrib)

apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)

done

lemma tape_of_nl_app_Suc: "((<list @ [Suc ab]>)) = (<list @ [ab]>) @ [Oc]"

apply(induct list)

apply(simp add: tape_of_nl_abv tape_of_nat_list.simps exp_ind)

apply(case_tac list)

apply(simp_all add:tape_of_nl_abv tape_of_nat_list.simps exp_ind)

done

lemma [simp]: "bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]> @ [Oc])

              = bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>) +

              2^(length (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>))"

apply(simp add: bin_wc_eq)

apply(simp add: bl2nat_cons_oc bl2wc.simps)

using bl2nat_cons_oc[of "Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>"]

apply(simp)

done

lemma [simp]: "bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [ab]>) + (4 * 2 ^ (aa + length (<list @ [ab]>)) +

         4 * (rs * 2 ^ (aa + length (<list @ [ab]>)))) =

       bl_bin (Oc # Oc\<^bsup>aa\<^esup> @ Bk # <list @ [Suc ab]>) +

         rs * (2 * 2 ^ (aa + length (<list @ [Suc ab]>)))"

apply(simp add: tape_of_nl_app_Suc)

done

declare tape_of_nat[simp del]

text{* double case*}

fun wcode_double_case_inv :: "nat \<Rightarrow> bin_inv_t"

  where

  "wcode_double_case_inv st ires rs (l, r) = 

          (if st = Suc 0 then wcode_on_left_moving_1 ires rs (l, r)

          else if st = Suc (Suc 0) then wcode_on_checking_1 ires rs (l, r)

          else if st = 3 then wcode_erase1 ires rs (l, r)

          else if st = 4 then wcode_on_right_moving_1 ires rs (l, r)

          else if st = 5 then wcode_goon_right_moving_1 ires rs (l, r)

          else if st = 6 then wcode_backto_standard_pos ires rs (l, r)

          else if st = 13 then wcode_before_double ires rs (l, r)

          else False)"

declare wcode_double_case_inv.simps[simp del]

fun wcode_double_case_state :: "t_conf \<Rightarrow> nat"

  where

  "wcode_double_case_state (st, l, r) = 

   13 - st"

fun wcode_double_case_step :: "t_conf \<Rightarrow> nat"

  where

  "wcode_double_case_step (st, l, r) = 

      (if st = Suc 0 then (length l)

      else if st = Suc (Suc 0) then (length r)

      else if st = 3 then 

                 if hd r = Oc then 1 else 0

      else if st = 4 then (length r)

      else if st = 5 then (length r)

      else if st = 6 then (length l)

      else 0)"

fun wcode_double_case_measure :: "t_conf \<Rightarrow> nat \<times> nat"

  where

  "wcode_double_case_measure (st, l, r) = 

     (wcode_double_case_state (st, l, r), 

      wcode_double_case_step (st, l, r))"

definition wcode_double_case_le :: "(t_conf \<times> t_conf) set"

  where "wcode_double_case_le \<equiv> (inv_image lex_pair wcode_double_case_measure)"

lemma [intro]: "wf lex_pair"

by(auto intro:wf_lex_prod simp:lex_pair_def)

lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"

by(auto intro:wf_inv_image simp: wcode_double_case_le_def )

term fetch

lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main (Suc 0) Oc = (L, Suc (Suc 0))"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main (Suc (Suc 0)) Oc = (R, 3)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Bk = (R, 4)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done 

lemma [simp]: "fetch t_wcode_main (Suc (Suc (Suc 0))) Oc = (W0, 3)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main 4 Bk = (R, 4)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main 4 Oc = (R, 5)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main 5 Oc = (R, 5)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main 5 Bk = (W1, 6)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main 6 Bk = (R, 13)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [simp]: "fetch t_wcode_main 6 Oc = (L, 6)"

apply(simp add: t_wcode_main_def t_wcode_main_first_part_def

                fetch.simps nth_of.simps)

done

lemma [elim]: "Bk\<^bsup>mr\<^esup> = [] \<Longrightarrow> mr = 0"

apply(case_tac mr, auto simp: exponent_def)

done

lemma [simp]: "wcode_on_left_moving_1 ires rs (b, []) = False"

apply(simp add: wcode_on_left_moving_1.simps wcode_on_left_moving_1_B.simps

                wcode_on_left_moving_1_O.simps, auto)

done

declare wcode_on_checking_1.simps[simp del]

lemmas wcode_double_case_inv_simps = 

  wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps

  wcode_on_left_moving_1_B.simps wcode_on_checking_1.simps

  wcode_erase1.simps wcode_on_right_moving_1.simps

  wcode_goon_right_moving_1.simps wcode_backto_standard_pos.simps

lemma [simp]: "wcode_on_left_moving_1 ires rs (b, r) \<Longrightarrow> b \<noteq> []"

apply(simp add: wcode_double_case_inv_simps, auto)

done

lemma [elim]: "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Bk # list);

                tl b = aa \<and> hd b # Bk # list = ba\<rbrakk> \<Longrightarrow> 

               wcode_on_left_moving_1 ires rs (aa, ba)"

apply(simp only: wcode_on_left_moving_1.simps wcode_on_left_moving_1_O.simps

                wcode_on_left_moving_1_B.simps)

apply(erule_tac disjE)

apply(erule_tac exE)+

apply(case_tac ml, simp)

apply(rule_tac x = "mr - Suc (Suc 0)" in exI, rule_tac x = rn in exI)

apply(case_tac mr, simp, case_tac nat, simp, simp add: exp_ind)

apply(rule_tac disjI1)

apply(rule_tac x = nat in exI, rule_tac x = "Suc mr" in exI, rule_tac x = rn in exI, 

      simp add: exp_ind_def)

apply(erule_tac exE)+

apply(simp)

done

lemma [elim]: 

  "\<lbrakk>wcode_on_left_moving_1 ires rs (b, Oc # list); tl b = aa \<and> hd b # Oc # list = ba\<rbrakk> 

    \<Longrightarrow> wcode_on_checking_1 ires rs (aa, ba)"

apply(simp only: wcode_double_case_inv_simps)

apply(erule_tac disjE)

apply(erule_tac [!] exE)+

apply(case_tac mr, simp, simp add: exp_ind_def)

apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

done

lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False" 

apply(auto simp: wcode_double_case_inv_simps)

done         

lemma [simp]: "wcode_on_checking_1 ires rs (b, Bk # list) = False"

apply(auto simp: wcode_double_case_inv_simps)

done         

lemma [elim]: "\<lbrakk>wcode_on_checking_1 ires rs (b, Oc # ba);Oc # b = aa \<and> list = ba\<rbrakk>

  \<Longrightarrow> wcode_erase1 ires rs (aa, ba)"

apply(simp only: wcode_double_case_inv_simps)

apply(erule_tac exE)+

apply(rule_tac x = ln in exI, rule_tac x = rn in exI, simp)

done

lemma [simp]: "wcode_on_checking_1 ires rs (b, []) = False"

apply(simp add: wcode_double_case_inv_simps)

done

lemma [simp]: "wcode_on_checking_1 ires rs ([], Bk # list) = False"

apply(simp add: wcode_double_case_inv_simps)

done

lemma [simp]: "wcode_erase1 ires rs (b, []) = False"

apply(simp add: wcode_double_case_inv_simps)

done

lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"

apply(simp add: wcode_double_case_inv_simps exp_ind_def)

done

lemma [simp]: "wcode_on_right_moving_1 ires rs (b, []) = False"

apply(simp add: wcode_double_case_inv_simps exp_ind_def)

done

lemma [elim]: "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Bk # ba);  Bk # b = aa \<and> list = b\<rbrakk> \<Longrightarrow> 

  wcode_on_right_moving_1 ires rs (aa, ba)"

apply(simp only: wcode_double_case_inv_simps)

apply(erule_tac exE)+

apply(rule_tac x = "Suc ml" in exI, rule_tac x = "mr - Suc 0" in exI,

      rule_tac x = rn in exI)

apply(simp add: exp_ind_def)

apply(case_tac mr, simp, simp add: exp_ind_def)

done

lemma [elim]: 

  "\<lbrakk>wcode_on_right_moving_1 ires rs (b, Oc # ba); Oc # b = aa \<and> list = ba\<rbrakk> 

  \<Longrightarrow> wcode_goon_right_moving_1 ires rs (aa, ba)"

apply(simp only: wcode_double_case_inv_simps)

apply(erule_tac exE)+

apply(rule_tac x = "Suc 0" in exI, rule_tac x = "rs" in exI,

      rule_tac x = "ml - Suc (Suc 0)" in exI, rule_tac x = rn in exI)