(* Title: Turing machine's definition and its charater

   Author: XuJian <xujian817@hotmail.com>

   Maintainer: Xujian

*)

header {* Undeciablity of the {\em Halting problem} *}

theory uncomputable

imports Main turing_hoare

begin

declare tm_comp.simps [simp del] 

declare adjust.simps[simp del] 

declare shift.simps[simp del]

declare tm_wf.simps[simp del]

declare step.simps[simp del]

declare steps.simps[simp del]

lemma numeral:

  shows "1 = Suc 0"

  and "2 = Suc 1"

  and "3 = Suc 2"

  and "4 = Suc 3" 

  and "5 = Suc 4" 

  and "6 = Suc 5" by arith+

text {*

  The {\em Copying} TM, which duplicates its input. 

*}

definition 

  tcopy_begin :: "instr list"

where

  "tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),

                 (W1, 3), (L, 4), (L, 4), (L, 0)]"

definition 

  tcopy_loop :: "instr list"

where

  "tcopy_loop \<equiv> [(R, 0), (R, 2),  (R, 3), (W0, 2),

                 (R, 3), (R, 4), (W1, 5), (R, 4),

                 (L, 6), (L, 5), (L, 6), (L, 1)]"

definition 

  tcopy_end :: "instr list"

where

  "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),

                (R, 2), (R, 2), (L, 5), (W0, 4),

                (R, 0), (L, 5)]"

  tcopy :: "instr list"

where

  "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"

(* tcopy_begin *)

fun 

  inv_begin0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_begin1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

where

  "inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   

                         (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"

| "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"

| "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"

| "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"

| "inv_begin4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"

fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"

  where

  "inv_begin n (s, l, r) = 

        (if s = 0 then inv_begin0 n (l, r) else

         if s = 1 then inv_begin1 n (l, r) else

         if s = 2 then inv_begin2 n (l, r) else

         if s = 3 then inv_begin3 n (l, r) else

         if s = 4 then inv_begin4 n (l, r) 

         else False)"

lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 

  \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"

apply(rule_tac x = "Suc i" in exI, simp)

done

lemma inv_begin_step: 

  "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"

unfolding tcopy_begin_def

apply(case_tac cf)

apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)

apply(case_tac "hd c", auto simp: inv_begin.simps)

apply(case_tac c, simp_all)

done

lemma inv_begin_steps: 

  "\<lbrakk>inv_begin x (s, l, r); x > 0\<rbrakk>

 \<Longrightarrow> inv_begin x (steps (s, l, r) (tcopy_begin, 0) stp)"

apply(induct stp, simp add: steps.simps)

apply(auto simp: step_red)

apply(rule_tac inv_begin_step, simp_all)

done

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

  where

  "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"

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

  where

  "init_step (s, l, r) = 

        (if s = 2 then length r else

         if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else

         if s = 4 then length l 

         else 0)"

fun init_measure :: "config \<Rightarrow> nat \<times> nat"

  where

  "init_measure c = (init_state c, init_step c)"

definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"

  where

  "lex_pair \<equiv> less_than <*lex*> less_than"

definition init_LE :: "(config \<times> config) set"

  where

  "init_LE \<equiv> (inv_image lex_pair init_measure)"

lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"

by (case_tac r, auto, case_tac a, auto)

lemma wf_begin_le: "wf init_LE"

by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)

lemma init_halt: 

  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"

  show "wf init_LE" by(simp add: wf_begin_le)

next

  assume h: "0 < x"

  show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>

        (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 

            steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"

  proof(rule_tac allI, rule_tac impI)

    fix n

    assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"

    have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"

      apply(rule_tac inv_begin_steps)

      apply(simp_all add: inv_begin.simps h)

      done 

    obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"

      apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto)

      done

    moreover hence "inv_begin x (s, l, r)" 

      using c b by simp

    ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 

      steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"

      using a 

    proof(simp del: inv_begin.simps)

      assume "inv_begin x (s, l, r)" "0 < s"

      thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> init_LE"

        apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)

        apply(case_tac r, auto, case_tac a, auto)

        done

    qed

  qed

qed

lemma init_correct: 

  "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"

proof(rule_tac Hoare_haltI)

  fix l r

  assume h: "0 < x" "inv_begin1 x (l, r)"

  hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"

    by (rule_tac init_halt)    

  then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..

  moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"

    apply(rule_tac inv_begin_steps)

    using h by(simp_all add: inv_begin.simps)

  ultimately show

    "\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and> 

    inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n"

    using h

    apply(rule_tac x = stp in exI)

    apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)

    done

qed

(* tcopy_loop *)

fun 

  inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"

where

  "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"

| "inv_loop1_exit x (l, r) = ((l, r) = ([], Bk#Oc#Bk\<up>x @ Oc\<up>x) \<and> x > 0)"

| "inv_loop5_loop x (l, r) = 

     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> (l, r) = (Oc\<up>k@Bk\<up>j@Oc\<up>i, Oc\<up>t))"

| "inv_loop5_exit x (l, r) = 

     (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Bk\<up>(j - 1)@Oc\<up>i, Bk # Oc\<up>j))"

| "inv_loop6_loop x (l, r) = 

     (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> (l, r) = (Bk\<up>k @ Oc\<up>i, Bk\<up>(Suc t) @ Oc\<up>j))"

| "inv_loop6_exit x (l, r) = 

     (\<exists> i j. i + j = x \<and> j > 0 \<and> (l, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"

fun 

  inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and

  inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

where

  "inv_loop0 x (l, r) =  ((l, r) = ([Bk], Oc # Bk\<up>x @ Oc\<up>x) \<and> x > 0)"

| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"

| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"

| "inv_loop3 x (l, r) = 

     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = Suc j \<and> (l, r) = (Bk\<up>k@Oc\<up>i, Bk\<up>t@Oc\<up>j))"

| "inv_loop4 x (l, r) = 

     (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and>  k + t = j \<and> (l, r) = (Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i, Oc\<up>t))"

| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"

| "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"

fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"

  where

  "inv_loop x (s, l, r) = 

         (if s = 0 then inv_loop0 x (l, r)

          else if s = 1 then inv_loop1 x (l, r)

          else if s = 2 then inv_loop2 x (l, r)

          else if s = 3 then inv_loop3 x (l, r)

          else if s = 4 then inv_loop4 x (l, r)

          else if s = 5 then inv_loop5 x (l, r)

          else if s = 6 then inv_loop6 x (l, r)

          else False)"

declare inv_loop.simps[simp del] inv_loop1.simps[simp del]

        inv_loop2.simps[simp del] inv_loop3.simps[simp del] 

        inv_loop4.simps[simp del] inv_loop5.simps[simp del] 

        inv_loop6.simps[simp del]

lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"

by (case_tac t, auto)

lemma [simp]: "inv_loop1 x (b, []) = False"

by (simp add: inv_loop1.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"

by (auto simp: inv_loop2.simps inv_loop3.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"

by (auto simp: inv_loop3.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"

apply(auto simp: inv_loop4.simps inv_loop5.simps)

apply(rule_tac [!] x = i in exI, 

      rule_tac [!] x  = "Suc j" in exI, simp_all)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"

by (auto simp: inv_loop4.simps inv_loop5.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"

by (auto simp: inv_loop4.simps inv_loop5.simps)

lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"

by (auto simp: inv_loop6.simps)

lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR" 

by (auto simp: inv_loop6.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"

by (auto simp: inv_loop1.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"

by (auto simp: inv_loop1.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"

apply(auto simp: inv_loop2.simps inv_loop3.simps)

apply(rule_tac [!] x = i  in exI, rule_tac [!] x = j in exI, simp_all)

done

lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"

by (case_tac j, simp_all)

lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"

apply(auto simp: inv_loop3.simps)

apply(rule_tac [!] x = i in exI, 

      rule_tac [!] x = j in exI, simp_all)

apply(case_tac [!] t, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"

by (auto simp: inv_loop4.simps inv_loop5.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"

by (auto simp: inv_loop6.simps inv_loop5.simps)

lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"

by (auto simp: inv_loop5.simps)

lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"

by (auto simp: inv_loop6.simps)

declare inv_loop5_loop.simps[simp del]  inv_loop5_exit.simps[simp del]

       inv_loop6_loop.simps[simp del]  inv_loop6_exit.simps[simp del]

lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk> 

          \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"

apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )

apply(erule_tac exE)+

apply(rule_tac x = i in exI, 

      rule_tac x = j in exI,

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

      rule_tac x = "Suc 0" in exI, auto)

apply(case_tac [!] j, simp_all)

apply(case_tac [!] nat, simp_all)

done

lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"

by (auto simp: inv_loop6_loop.simps)

lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow> 

  inv_loop6_exit x (tl b, Oc # Bk # list)"

apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)

apply(erule_tac exE)+

apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)

apply(case_tac j, auto)

apply(case_tac [!] nat, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"

apply(simp add: inv_loop5.simps inv_loop6.simps)

apply(case_tac "hd b", simp_all, auto)

done

lemma  [simp]: "inv_loop6 x ([], Bk # xs) = False"

apply(simp add: inv_loop6.simps inv_loop6_loop.simps

                inv_loop6_exit.simps)

apply(auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"

by (simp)

lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"

by (simp add: inv_loop6_exit.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>

              \<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"

apply(simp only: inv_loop6_loop.simps)

apply(erule_tac exE)+

apply(rule_tac x = i in exI, rule_tac x = j in exI, 

      rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)

apply(case_tac [!] k, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> 

        \<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"

apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)

apply(erule_tac exE)+

apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)

apply(case_tac [!] k, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"

apply(simp add: inv_loop6.simps)

apply(case_tac "hd b", simp_all, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"

apply(auto simp: inv_loop1.simps inv_loop2.simps)

apply(rule_tac x = "Suc i" in exI, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"

by (auto simp: inv_loop2.simps)

lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"

apply(auto simp: inv_loop3.simps inv_loop4.simps)

apply(rule_tac [!] x = i in exI, auto)

apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)

apply(case_tac [!] t, auto)

apply(case_tac [!] j, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"

apply(auto simp: inv_loop4.simps)

apply(rule_tac [!] x = "i" in exI, auto)

apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)

apply(case_tac [!] t, simp_all)

done

lemma [simp]: "inv_loop5 x ([], list) = False"

by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)

lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"

by (auto simp: inv_loop5_exit.simps)

lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>

  \<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"

apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)

apply(erule_tac exE)+

apply(rule_tac x = i in exI, auto)

apply(case_tac [!] k, auto)

done

lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> 

           \<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"

apply(simp only:  inv_loop5_loop.simps)

apply(erule_tac exE)+

apply(rule_tac x = i in exI, rule_tac x = j in exI)

apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)

apply(case_tac [!] k, auto)

done

lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"

apply(simp add: inv_loop5.simps)

apply(case_tac "hd b", simp_all, auto)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"

apply(auto simp: inv_loop6.simps inv_loop1.simps 

  inv_loop6_loop.simps inv_loop6_exit.simps)

done

lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk> 

           \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"

apply(auto simp: inv_loop6.simps inv_loop1.simps 

  inv_loop6_loop.simps inv_loop6_exit.simps)

done

lemma inv_loop_step: 

  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"

apply(case_tac cf, case_tac c, case_tac [2] aa)

apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)

done

lemma inv_loop_steps:

  "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>

  \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"

apply(induct stp, simp add: steps.simps, simp)

apply(erule_tac inv_loop_step, simp)

done

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

  where

  "loop_stage (s, l, r) = (if s = 0 then 0

                           else (Suc (length (takeWhile (\<lambda>a. a = Oc) (rev l @ r)))))"

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

  where

  "loop_state (s, l, r) = (if s = 2 \<and> hd r = Oc then 0

                           else if s = 1 then 1

                           else 10 - s)"

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

  where

  "loop_step (s, l, r) = (if s = 3 then length r

                          else if s = 4 then length r

                          else if s = 5 then length l 

                          else if s = 6 then length l

                          else 0)"

definition lex_triple :: 

 "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"

  where

  "lex_triple \<equiv> less_than <*lex*> lex_pair"

lemma wf_lex_triple: "wf lex_triple"

  by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)

fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat"

  where

  "loop_measure c = 

   (loop_stage c, loop_state c, loop_step c)"

definition loop_LE :: "(config \<times> config) set"

  where

   "loop_LE \<equiv> (inv_image lex_triple loop_measure)"

lemma wf_loop_le: "wf loop_LE"

by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)

lemma [simp]: "inv_loop2 x ([], b) = False"

by (auto simp: inv_loop2.simps)

lemma  [simp]: "inv_loop2 x (l', []) = False"

by (auto simp: inv_loop2.simps)

lemma [simp]: "inv_loop3 x (b, []) = False"

by (auto simp: inv_loop3.simps)

lemma [simp]: "inv_loop4 x ([], b) = False"

by (auto simp: inv_loop4.simps)