header {* 

  Separation logic for Turing Machines

*}

theory Hoare_tm

imports Hoare_gen My_block Data_slot

begin

ML {*

fun pretty_terms ctxt trms =

  Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms))

*}

ML {*

structure StepRules = Named_Thms

  (val name = @{binding "step"}

   val description = "Theorems for hoare rules for every step")

*}

ML {*

structure FwdRules = Named_Thms

  (val name = @{binding "fwd"}

   val description = "Theorems for fwd derivation of seperation implication")

*}

setup {* StepRules.setup *}

setup {* FwdRules.setup *}

section {* Operational Semantics of TM *}

datatype taction = W0 | W1 | L | R

type_synonym tstate = nat

type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"

datatype Block = Oc | Bk

type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"

fun tstep :: "tconf \<Rightarrow> tconf"

  where "tstep (faults, prog, pc, pos, m) = 

              (case (prog pc) of

                  Some ((action0, pc0), (action1, pc1)) \<Rightarrow> 

                     case (m pos) of

                       Some Bk \<Rightarrow> (faults, prog, pc0, next_tape action0 (pos, m)) |

                       Some Oc \<Rightarrow> (faults, prog, pc1, next_tape action1 (pos, m)) |

                       None \<Rightarrow> (faults + 1, prog, pc, pos, m)

                | None \<Rightarrow> (faults + 1, prog, pc, pos, m))"

lemma tstep_splits: 

  "(P (tstep s)) = ((\<forall> faults prog pc pos m action0 pc0 action1 pc1. 

                          s = (faults, prog, pc, pos, m) \<longrightarrow> 

                          prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> 

                          m pos = Some Bk \<longrightarrow> P (faults, prog, pc0, next_tape action0 (pos, m))) \<and>

                    (\<forall> faults prog pc pos m action0 pc0 action1 pc1. 

                          s = (faults, prog, pc, pos, m) \<longrightarrow> 

                          prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> 

                          m pos = Some Oc \<longrightarrow> P (faults, prog, pc1, next_tape action1 (pos, m))) \<and>

                    (\<forall> faults prog pc pos m action0 pc0 action1 pc1. 

                          s = (faults, prog, pc, pos, m) \<longrightarrow> 

                          prog pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow> 

                          m pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and>

                    (\<forall> faults prog pc pos m . 

                          s =  (faults, prog, pc, pos, m) \<longrightarrow>

                          prog pc  = None \<longrightarrow> P (faults + 1, prog, pc, pos, m))

                   )"

datatype tresource = 

    TM int Block

  | TC nat tm_inst

  | TAt nat

  | TPos int

  | TFaults nat

definition "tprog_set prog = {TC i inst | i inst. prog i = Some inst}"

definition "tpc_set pc = {TAt pc}"

definition "tmem_set m = {TM i n | i n. m (i) = Some n}"

definition "tpos_set pos = {TPos pos}"

definition "tfaults_set faults = {TFaults faults}"

lemmas tpn_set_def = tprog_set_def tpc_set_def tmem_set_def tfaults_set_def tpos_set_def

fun trset_of :: "tconf \<Rightarrow> tresource set"

  where "trset_of (faults, prog, pc, pos, m) = 

               tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults"

interpretation tm: sep_exec tstep trset_of .

section {* Assembly language for TMs and its program logic *}

subsection {* The assembly language *}

datatype tpg = 

   TInstr tm_inst

 | TLabel nat

 | TSeq tpg tpg

 | TLocal "nat \<Rightarrow> tpg"

notation TLocal (binder "TL " 10)

abbreviation tprog_instr :: "tm_inst \<Rightarrow> tpg" ("\<guillemotright> _" [61] 61)

where "\<guillemotright> i \<equiv> TInstr i"

abbreviation tprog_seq :: "tpg \<Rightarrow> tpg \<Rightarrow> tpg" (infixr ";" 52)

where "c1 ; c2 \<equiv> TSeq c1 c2"

definition "sg e = (\<lambda> s. s = e)"

type_synonym tassert = "tresource set \<Rightarrow> bool"

abbreviation t_hoare :: "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

  where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"

abbreviation it_hoare ::

  "('a::sep_algebra \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"

      ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q"

(*

primrec tpg_len :: "tpg \<Rightarrow> nat" where 

  "tpg_len (TInstr ai) = 1" |

  "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " |

  "tpg_len (TLocal fp) = tpg_len (fp 0)" |

  "tpg_len (TLabel l) = 0" 

*)

primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" 

  where 

  "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" |

  "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" |

  "tassemble_to (TLocal fp) i j  = (EXS l. (tassemble_to (fp l) i j))" | 

  "tassemble_to (TLabel l) i j = <(i = j \<and> j = l)>"

declare tassemble_to.simps [simp del]

lemmas tasmp = tassemble_to.simps (2, 3, 4)

abbreviation tasmb_to :: "nat \<Rightarrow> tpg \<Rightarrow> nat \<Rightarrow> tassert" ("_ :[ _ ]: _" [60, 60, 60] 60)

  where "i :[ tpg ]: j \<equiv> tassemble_to tpg i j"

lemma EXS_intro: 

  assumes h: "(P x) s"

  shows "(EXS x. P(x)) s"

  by (smt h pred_ex_def sep_conj_impl)

lemma EXS_elim: 

  assumes "(EXS x. P x) s"

  obtains x where "P x s"

  by (metis assms pred_ex_def)

lemma EXS_eq:

  fixes x

  assumes h: "Q (p x)" 

  and h1: "\<And> y s. \<lbrakk>p y s\<rbrakk> \<Longrightarrow> y = x"

  shows "p x = (EXS x. p x)"

proof

  fix s

  show "p x s = (EXS x. p x) s"

  proof

    assume "p x s"

    thus "(EXS x. p x) s" by (auto simp:pred_ex_def)

  next

    assume "(EXS x. p x) s"

    thus "p x s"

    proof(rule EXS_elim)

      fix y

      assume "p y s"

      from this[unfolded h1[OF this]] show "p x s" .

    qed

  qed

qed

definition "tpg_fold tpgs = foldr TSeq (butlast tpgs) (last tpgs)"

lemma tpg_fold_sg: "tpg_fold [tpg] = tpg"

  by (simp add:tpg_fold_def)

lemma tpg_fold_cons: 

  assumes h: "tpgs \<noteq> []"

  shows "tpg_fold (tpg#tpgs) = (tpg; (tpg_fold tpgs))"

  using h

proof(induct tpgs arbitrary:tpg)

  case (Cons tpg1 tpgs1)

  thus ?case

  proof(cases "tpgs1 = []")

    case True

    thus ?thesis by (simp add:tpg_fold_def)

  next

    case False

    show ?thesis

    proof -

      have eq_1: "butlast (tpg # tpg1 # tpgs1) = tpg # (butlast (tpg1 # tpgs1))"

        by simp

      from False have eq_2: "last (tpg # tpg1 # tpgs1) = last (tpg1 # tpgs1)"

        by simp

      have eq_3: "foldr (op ;) (tpg # butlast (tpg1 # tpgs1)) (last (tpg1 # tpgs1)) = 

            (tpg ; (foldr (op ;) (butlast (tpg1 # tpgs1)) (last (tpg1 # tpgs1))))"

        by simp

      show ?thesis

        apply (subst (1) tpg_fold_def, unfold eq_1 eq_2 eq_3)

        by (fold tpg_fold_def, simp)

    qed

  qed

qed auto

lemmas tpg_fold_simps = tpg_fold_sg tpg_fold_cons

lemma tpg_fold_app:

  assumes h1: "tpgs1 \<noteq> []" 

  and h2: "tpgs2 \<noteq> []"

  shows "i:[(tpg_fold (tpgs1 @ tpgs2))]:j = i:[(tpg_fold (tpgs1); tpg_fold tpgs2)]:j"

  using h1 h2

proof(induct tpgs1 arbitrary: i j tpgs2)

  case (Cons tpg1' tpgs1')

  thus ?case (is "?L = ?R")

  proof(cases "tpgs1' = []")

    case False

    from h2 have "(tpgs1' @ tpgs2) \<noteq> []"

      by (metis Cons.prems(2) Nil_is_append_conv) 

    have "?L = (i :[ tpg_fold (tpg1' # (tpgs1' @ tpgs2)) ]: j )" by simp

    also have "\<dots> =  (i:[(tpg1'; (tpg_fold (tpgs1' @ tpgs2)))]:j )"

      by (simp add:tpg_fold_cons[OF `(tpgs1' @ tpgs2) \<noteq> []`])

    also have "\<dots> = ?R"

    proof -

      have "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) =

              (EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>* 

                               j' :[ tpg_fold tpgs2 ]: j)"

      proof(default+)

        fix s

        assume "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

        thus "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>*

                  j' :[ tpg_fold tpgs2 ]: j) s"

        proof(elim EXS_elim)

          fix j'

          assume "(i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

          from this[unfolded Cons(1)[OF False Cons(3)] tassemble_to.simps]

          show "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>*

                           j' :[ tpg_fold tpgs2 ]: j) s"

          proof(elim sep_conjE EXS_elim)

            fix x y j'a xa ya

            assume h: "(i :[ tpg1' ]: j') x"

                      "x ## y" "s = x + y"

                      "(j' :[ tpg_fold tpgs1' ]: j'a) xa"

                      "(j'a :[ tpg_fold tpgs2 ]: j) ya"

                      " xa ## ya" "y = xa + ya"

            show "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* 

                                j'a :[ tpg_fold tpgs1' ]: j') \<and>* j' :[ tpg_fold tpgs2 ]: j) s"

               (is "(EXS j'. (?P j' \<and>* ?Q j')) s")

            proof(rule EXS_intro[where x = "j'a"])

              from `(j'a :[ tpg_fold tpgs2 ]: j) ya` have "(?Q j'a) ya" .

              moreover have "(?P j'a) (x + xa)" 

              proof(rule EXS_intro[where x = j'])

                have "x + xa = x + xa" by simp

                moreover from `x ## y` `y = xa + ya` `xa ## ya` 

                have "x ## xa" by (metis sep_disj_addD) 

                moreover note `(i :[ tpg1' ]: j') x` `(j' :[ tpg_fold tpgs1' ]: j'a) xa`

                ultimately show "(i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold tpgs1' ]: j'a) (x + xa)"

                  by (auto intro!:sep_conjI)

              qed

              moreover from `x##y` `y = xa + ya` `xa ## ya` 

              have "(x + xa) ## ya"

                by (metis sep_disj_addI1 sep_disj_commuteI)

              moreover from `s = x + y` `y = xa + ya`

              have "s = (x + xa) + ya"

                by (metis h(2) h(6) sep_add_assoc sep_disj_addD1 sep_disj_addD2) 

              ultimately show "(?P j'a \<and>* ?Q j'a) s"

                by (auto intro!:sep_conjI)

            qed

          qed

        qed

      next

        fix s

        assume "(EXS j'. (EXS j'a. i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold tpgs1' ]: j') \<and>*

                                    j' :[ tpg_fold tpgs2 ]: j) s"

        thus "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

        proof(elim EXS_elim sep_conjE)

          fix j' x y j'a xa ya

          assume h: "(j' :[ tpg_fold tpgs2 ]: j) y"

                    "x ## y" "s = x + y" "(i :[ tpg1' ]: j'a) xa"

                    "(j'a :[ tpg_fold tpgs1' ]: j') ya" "xa ## ya" "x = xa + ya"

          show "(EXS j'. i :[ tpg1' ]: j' \<and>* j' :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

          proof(rule EXS_intro[where x = j'a])

            from `(i :[ tpg1' ]: j'a) xa` have "(i :[ tpg1' ]: j'a) xa" .

            moreover have "(j'a :[ tpg_fold (tpgs1' @ tpgs2) ]: j) (ya + y)"

            proof(unfold Cons(1)[OF False Cons(3)] tassemble_to.simps)

              show "(EXS j'. j'a :[ tpg_fold tpgs1' ]: j' \<and>* j' :[ tpg_fold tpgs2 ]: j) (ya + y)"

              proof(rule EXS_intro[where x = "j'"])

                from `x ## y` `x = xa + ya` `xa ## ya`

                have "ya ## y" by (metis sep_add_disjD)

                moreover have "ya + y = ya + y" by simp

                moreover note `(j'a :[ tpg_fold tpgs1' ]: j') ya` 

                               `(j' :[ tpg_fold tpgs2 ]: j) y`

                ultimately show "(j'a :[ tpg_fold tpgs1' ]: j' \<and>* 

                                 j' :[ tpg_fold tpgs2 ]: j) (ya + y)"

                  by (auto intro!:sep_conjI)

              qed

            qed

            moreover from `s = x + y` `x = xa + ya`

            have "s = xa + (ya + y)"

              by (metis h(2) h(6) sep_add_assoc sep_add_disjD)

            moreover from `xa ## ya` `x ## y` `x = xa + ya`

            have "xa ## (ya + y)" by (metis sep_disj_addI3) 

            ultimately show "(i :[ tpg1' ]: j'a \<and>* j'a :[ tpg_fold (tpgs1' @ tpgs2) ]: j) s"

              by (auto intro!:sep_conjI)

          qed

        qed

      qed

      thus ?thesis 

        by (simp add:tassemble_to.simps, unfold tpg_fold_cons[OF False], 

             unfold tassemble_to.simps, simp)

    qed

    finally show ?thesis . 

  next

    case True

    thus ?thesis

      by (simp add:tpg_fold_cons[OF Cons(3)] tpg_fold_sg)

  qed 

qed auto

subsection {* Assertions and program logic for this assembly language *}

definition "st l = sg (tpc_set l)"

definition "ps p = sg (tpos_set p)" 

definition "tm a v =sg ({TM a v})"

definition "one i = tm i Oc"

definition "zero i= tm i Bk"

definition "any i = (EXS v. tm i v)"

declare trset_of.simps[simp del]

lemma stimes_sgD: "(sg x ** q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s"

  apply(erule_tac sep_conjE)

  apply(unfold set_ins_def sg_def)

  by (metis Diff_Int2 Diff_Int_distrib2 Diff_Un Diff_cancel 

    Diff_empty Diff_idemp Diff_triv Int_Diff Un_Diff 

    Un_Diff_cancel inf_commute inf_idem sup_bot_right sup_commute sup_ge2)

lemma stD: "(st i ** r) (trset_of (ft, prog, i', pos, mem))

       \<Longrightarrow> i' = i"

proof -

  assume "(st i ** r) (trset_of (ft, prog, i', pos, mem))"

  from stimes_sgD [OF this[unfolded st_def], unfolded trset_of.simps]

  have "tpc_set i \<subseteq> tprog_set prog \<union> tpc_set i' \<union> tpos_set pos \<union>  

            tmem_set mem \<union> tfaults_set ft" by auto

  thus ?thesis

    by (unfold tpn_set_def, auto)

qed

lemma psD: "(ps p ** r) (trset_of (ft, prog, i', pos, mem))

       \<Longrightarrow> pos = p"

proof -

  assume "(ps p ** r) (trset_of (ft, prog, i', pos, mem))"

  from stimes_sgD [OF this[unfolded ps_def], unfolded trset_of.simps]

  have "tpos_set p \<subseteq> tprog_set prog \<union> tpc_set i' \<union> 

                       tpos_set pos \<union> tmem_set mem \<union> tfaults_set ft"

    by simp

  thus ?thesis

    by (unfold tpn_set_def, auto)

qed

lemma codeD: "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))

       \<Longrightarrow> prog i = Some inst"

proof -

  assume "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))"

  thus ?thesis

    apply(unfold sep_conj_def set_ins_def sg_def trset_of.simps tpn_set_def)

    by auto

qed

lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))  \<Longrightarrow> mem a = Some v"

proof -

  assume "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))"

  from stimes_sgD[OF this[unfolded trset_of.simps tpn_set_def tm_def]]

  have "{TM a v} \<subseteq> {TC i inst |i inst. prog i = Some inst} \<union> {TAt i} \<union> 

    {TPos pos} \<union> {TM i n |i n. mem i = Some n} \<union> {TFaults ft}" by simp

  thus ?thesis by auto

qed

lemma t_hoare_seq: 

  "\<lbrakk>\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>; 

    \<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>\<rbrakk> \<Longrightarrow>  \<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"

proof -

  assume h: "\<And> i j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st j ** q\<rbrace>" 

            "\<And> j k. \<lbrace>st j ** q\<rbrace> j:[c2]:k \<lbrace>st k ** r\<rbrace>"

  show "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k ** r\<rbrace>"

  proof(subst tassemble_to.simps, rule tm.code_exI)

    fix j'

    show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>"

    proof(rule tm.composition)

      from h(1) show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace> st j' \<and>* q \<rbrace>" by auto

    next

      from h(2) show "\<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k \<and>* r\<rbrace>" by auto

    qed

  qed

qed

lemma t_hoare_seq1:

   "\<lbrakk>\<And>j'. \<lbrace>st i ** p\<rbrace> i:[c1]:j' \<lbrace>st j' ** q\<rbrace>;

    \<And>j'. \<lbrace>st j' ** q\<rbrace> j':[c2]:k \<lbrace>st k' ** r\<rbrace>\<rbrakk> \<Longrightarrow>  

           \<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>st k' ** r\<rbrace>"

proof -

  assume h: "\<And>j'. \<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace>st j' \<and>* q\<rbrace>" 

            "\<And>j'. \<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"

  show "\<lbrace>st i \<and>* p\<rbrace>  i :[ (c1 ; c2) ]: k \<lbrace>st k' \<and>* r\<rbrace>"

  proof(subst tassemble_to.simps, rule tm.code_exI)

    fix j'

    show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>"

    proof(rule tm.composition)

      from h(1) show "\<lbrace>st i \<and>* p\<rbrace>  i :[ c1 ]: j' \<lbrace> st j' \<and>* q \<rbrace>" by auto

    next

      from h(2) show " \<lbrace>st j' \<and>* q\<rbrace>  j' :[ c2 ]: k \<lbrace>st k' \<and>* r\<rbrace>" by auto

    qed

  qed

qed

lemma t_hoare_seq2:

 assumes h: "\<And>j. \<lbrace>st i ** p\<rbrace> i:[c1]:j \<lbrace>st k' \<and>* r\<rbrace>"

 shows "\<lbrace>st i ** p\<rbrace> i:[(c1 ; c2)]:j \<lbrace>st k' ** r\<rbrace>"

  apply (unfold tassemble_to.simps, rule tm.code_exI)

  by (rule tm.code_extension, rule h)

lemma t_hoare_local: 

  assumes h: "(\<And>l. \<lbrace>st i \<and>* p\<rbrace>  i :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>)"

  shows "\<lbrace>st i ** p\<rbrace> i:[TLocal c]:j \<lbrace>st k ** q\<rbrace>" using h

  by (unfold tassemble_to.simps, intro tm.code_exI, simp)

lemma t_hoare_label: 

      "(\<And>l. l = i \<Longrightarrow> \<lbrace>st l \<and>* p\<rbrace>  l :[ c l ]: j \<lbrace>st k \<and>* q\<rbrace>) \<Longrightarrow>

             \<lbrace>st i \<and>* p \<rbrace> 

               i:[(TLabel l; c l)]:j

             \<lbrace>st k \<and>* q\<rbrace>"

by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)

primrec t_split_cmd :: "tpg \<Rightarrow> (tpg \<times> tpg option)"

  where "t_split_cmd (\<guillemotright>inst) = (\<guillemotright>inst, None)" |

        "t_split_cmd (TLabel l) = (TLabel l, None)" |

        "t_split_cmd (TSeq c1 c2) = (case (t_split_cmd c2) of

                                      (c21, Some c22) \<Rightarrow> (TSeq c1 c21, Some c22) |

                                      (c21, None) \<Rightarrow> (c1, Some c21))" |

        "t_split_cmd (TLocal c) = (TLocal c, None)"

definition "t_last_cmd tpg = (snd (t_split_cmd tpg))"

declare t_last_cmd_def [simp]

definition "t_blast_cmd tpg = (fst (t_split_cmd tpg))"

declare t_blast_cmd_def [simp]

lemma "t_last_cmd (c1; c2; (TLabel l)) = (Some (TLabel l))"

  by simp

lemma "t_blast_cmd (c1; c2; TLabel l) = (c1; c2)"

  by simp

lemma t_split_cmd_eq:

  assumes "t_split_cmd c = (c1, Some c2)"

  shows "(i:[c]:j) = (i:[(c1; c2)]:j)"

  using assms

proof(induct c arbitrary: c1 c2 i j)

  case (TSeq cx cy)

  from `t_split_cmd (cx ; cy) = (c1, Some c2)`

  show ?case

    apply (simp split:prod.splits option.splits)

    apply (cases cy, auto split:prod.splits option.splits)

    proof -

      fix a

      assume h: "t_split_cmd cy = (a, Some c2)"

      show "i :[ (cx ; cy) ]: j = i :[ ((cx ; a) ; c2) ]: j"

        apply (simp only: tassemble_to.simps(2) TSeq(2)[OF h] sep_conj_exists)

        apply (simp add:sep_conj_ac)

        by (simp add:pred_ex_def, default, auto)

    qed

qed auto

lemma t_hoare_label_last_pre: 

  fixes l

  assumes h1: "t_split_cmd c = (c', Some (TLabel l))"

  and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[c']:j \<lbrace>q\<rbrace>"

  shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"

by (unfold t_split_cmd_eq[OF h1], 

    simp only:tassemble_to.simps sep_conj_cond, 

    intro tm.code_exI tm.code_condI, insert h2, auto)

lemma t_hoare_label_last: 

  fixes l

  assumes h1: "t_last_cmd c = Some (TLabel l)"

  and h2: "l = j \<Longrightarrow> \<lbrace>p\<rbrace> i:[t_blast_cmd c]:j \<lbrace>q\<rbrace>"

  shows "\<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"

proof -

    have "t_split_cmd c = (t_blast_cmd c, t_last_cmd c)"

      by simp

  from t_hoare_label_last_pre[OF this[unfolded h1]] h2

  show ?thesis by auto