header {* 

 {\em abacus} a kind of register machine

*}

theory abacus

imports Main "../Separation_Algebra/Sep_Tactics"

begin

instantiation set :: (type)sep_algebra

begin

definition set_zero_def: "0 = {}"

definition plus_set_def: "s1 + s2 = s1 \<union> s2"

definition sep_disj_set_def: "sep_disj s1 s2 = (s1 \<inter> s2 = {})"

lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def

instance

  apply(default)

  apply(simp add:set_ins_def)

  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)

  apply (metis inf_commute)

  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)

  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)

  apply (metis sup_commute)

  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)

  apply (metis (lifting) Un_assoc)

  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)

  apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff)

  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)

  by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff)

end

text {*

  {\em Abacus} instructions:

*}

datatype abc_inst =

  -- {* @{text "Inc n"} increments the memory cell (or register) 

         with address @{text "n"} by one.

     *}

     Inc nat

  -- {*

     @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. 

      If cell @{text "n"} is already zero, no decrements happens and the executio jumps to

      the instruction labeled by @{text "label"}.

     *}

   | Dec nat nat

  -- {*

  @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.

  *}

   | Goto nat

datatype apg = 

   Instr abc_inst

 | Label nat

 | Seq apg apg

 | Local "(nat \<Rightarrow> apg)"

notation Local (binder "L " 10)

abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61)

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

abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixr ";" 52)

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

type_synonym aconf = "((nat \<rightharpoonup> abc_inst) \<times> nat \<times> (nat \<rightharpoonup> nat) \<times> nat)"

fun astep :: "aconf \<Rightarrow> aconf"

  where "astep (prog, pc, m, faults) = 

              (case (prog pc) of

                  Some (Inc i) \<Rightarrow> 

                         case m(i) of

                           Some n \<Rightarrow> (prog, pc + 1, m(i:= Some (n + 1)), faults)

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

                | Some (Dec i e) \<Rightarrow> 

                         case m(i) of

                           Some n \<Rightarrow> if (n = 0) then (prog, e, m, faults)

                                     else (prog, pc + 1, m(i:= Some (n - 1)), faults)

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

                | Some (Goto pc') \<Rightarrow> (prog, pc', m, faults)

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

definition "run n = astep ^^ n"

datatype aresource = 

    M nat nat

  | C nat abc_inst

  | At nat

  | Faults nat

definition "prog_set prog = {C i inst | i inst. prog i = Some inst}"

definition "pc_set pc = {At pc}"

definition "mem_set m = {M i n | i n. m (i) = Some n} "

definition "faults_set faults = {Faults faults}"

lemmas cpn_set_def = prog_set_def pc_set_def mem_set_def faults_set_def

fun rset_of :: "aconf \<Rightarrow> aresource set"

  where "rset_of (prog, pc, m, faults) = 

               prog_set prog \<union> pc_set pc \<union> mem_set m \<union> faults_set faults"

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

definition "pc l = sg (pc_set l)"

definition "m a v =sg ({M a v})"

declare rset_of.simps[simp del]

type_synonym assert = "aresource set \<Rightarrow> bool"

primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" 

  where 

  "assemble_to (Instr ai) i j = (sg ({C i ai}) ** \<langle>(j = i + 1)\<rangle>)" |

  "assemble_to (Seq p1 p2) i j = (EXS j'. (assemble_to p1 i j') ** (assemble_to p2 j' j))" |

  "assemble_to (Local fp) i j  = (EXS l. (assemble_to (fp l) i j))" | 

  "assemble_to (Label l) i j = \<langle>(i = j \<and> j = l)\<rangle>"

abbreviation asmb_to :: "nat \<Rightarrow> apg \<Rightarrow> nat \<Rightarrow> assert" ("_ :[ _ ]: _" [60, 60, 60] 60)

  where "i :[ apg ]: j \<equiv> assemble_to apg i j"

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 pcD: "(pc i ** r) (rset_of (prog, i', mem, fault))

       \<Longrightarrow> i' = i"

proof -

  assume "(pc i ** r) (rset_of (prog, i', mem, fault))"

  from stimes_sgD [OF this[unfolded pc_def], unfolded rset_of.simps]

  have "pc_set i \<subseteq> prog_set prog \<union> pc_set i' \<union> mem_set mem \<union> faults_set fault" by auto

  thus ?thesis 

    by (unfold cpn_set_def, auto)

qed

lemma codeD: "(pc i ** sg {C i inst} ** r) (rset_of (prog, pos, mem, fault))

       \<Longrightarrow> prog pos = Some inst"

proof -

  assume "(pc i ** sg {C i inst} ** r) (rset_of (prog, pos, mem, fault))" 

  thus ?thesis

    apply(sep_subst pcD)

    apply(unfold sep_conj_def set_ins_def sg_def rset_of.simps cpn_set_def)

    by auto

qed

lemma memD: "((m a v) ** r) (rset_of (prog, pos, mem, fault))  \<Longrightarrow> mem a = Some v"

proof -

  assume "((m a v) ** r) (rset_of (prog, pos, mem, fault))"

  from stimes_sgD[OF this[unfolded rset_of.simps cpn_set_def m_def]]

  have "{M a v} \<subseteq> {C i inst |i inst. prog i = Some inst} \<union> 

            {At pos} \<union> {M i n |i n. mem i = Some n} \<union> {Faults fault}" by auto

  thus ?thesis by auto

qed

definition

  Hoare_abc :: "assert \<Rightarrow> assert  \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)

where

  "{p} c {q} \<equiv> (\<forall> s r. (p**c**r) (rset_of s) \<longrightarrow>

    (\<exists> k. ((q ** c ** r) (rset_of (run k s)))))" 

definition "dec_fun v j e = (if (v = 0) then (e, v) else (j, v - 1))"

lemma disj_Diff: "a \<inter> b = {} \<Longrightarrow> a \<union> b - b = a"

by (metis (lifting) Diff_cancel Un_Diff Un_Diff_Int)

lemma diff_pc_set: "prog_set aa \<union> pc_set i \<union> mem_set ab \<union> faults_set b - pc_set i = 

         prog_set aa \<union> mem_set ab \<union> faults_set b"  (is "?L = ?R")

proof -

  have "?L = (prog_set aa \<union> mem_set ab \<union> faults_set b \<union> pc_set i)  - pc_set i"

    by auto

  also have "\<dots> = ?R"

  proof(rule disj_Diff)

    show " (prog_set aa \<union> mem_set ab \<union> faults_set b) \<inter> pc_set i = {}"

      by (unfold cpn_set_def, auto)

  qed

  finally show ?thesis .

qed

lemma M_in_simp: "({M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f) = 

        ({M a v} \<subseteq> mem_set mem)"

  by (unfold cpn_set_def, auto)

lemma mem_set_upd: 

  "{M a v} \<subseteq> mem_set mem \<Longrightarrow> mem_set (mem(a:=Some v')) = ((mem_set mem) - {M a v}) \<union> {M a v'}"

  by (unfold cpn_set_def, auto)

lemma mem_set_disj: "{M a v} \<subseteq> mem_set mem \<Longrightarrow> {M a v'} \<inter>  (mem_set mem - {M a v}) = {}"

  by (unfold cpn_set_def, auto)

lemma smem_upd: "((m a v) ** r) (rset_of (x, y, mem, f))  \<Longrightarrow> 

                    ((m a v') ** r) (rset_of (x, y, mem(a := Some v'), f))"

proof -

  have eq_s:"

    (prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v}) =

    (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"

    by (unfold cpn_set_def, auto)

  assume "(m a v \<and>* r) (rset_of (x, y, mem, f))"

  from this[unfolded rset_of.simps m_def]

  have h: "(sg {M a v} \<and>* r) (prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f)" .

  hence h0: "r (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"

    by(sep_drule stimes_sgD, clarify, unfold eq_s, auto)

  from h M_in_simp have "{M a v} \<subseteq> mem_set mem"

    by(sep_drule stimes_sgD, auto)

  from mem_set_upd [OF this] mem_set_disj[OF this]

  have h2: "mem_set (mem(a \<mapsto> v')) = {M a v'} \<union> (mem_set mem - {M a v})" 

           "{M a v'} \<inter> (mem_set mem - {M a v}) = {}" by auto

  show ?thesis

  proof -

    have "(m a v' ** r) (mem_set (mem(a \<mapsto> v')) \<union>  prog_set x \<union> pc_set y \<union> faults_set f)"

    proof(rule sep_conjI)

      from h0 show "r (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)" .

    next

      show "m a v' ({M a v'})" by (unfold m_def sg_def, simp)

    next

      show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f =

            {M a v'} + (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"

        by (unfold h2(1) set_ins_def eq_s, auto)

    next

      from h2(2)

      show " {M a v'} ## prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f"

        by (unfold cpn_set_def set_ins_def, auto)

    qed

    thus ?thesis 

      apply (unfold rset_of.simps)

      by (metis sup_commute sup_left_commute)

  qed

qed

lemma pc_dest: "(pc i') (pc_set i) \<Longrightarrow> i = i'"

  sorry

lemma spc_upd: "(pc i' ** r) (rset_of (x, i, y, z))  \<Longrightarrow> 

                (pc i'' ** r) (rset_of (x, i'', y, z))"

proof -

  assume h: "rset_of (x, i, y, z) \<in> pc i' * r"

  from stimes_sgD [OF h[unfolded rset_of.simps pc_set_def pc_def]]

  have h1: "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} \<in> r" 

           "{At i'} \<subseteq> prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z" by auto

  from h1(2) have eq_i: "i' = i" by (unfold cpn_set_def, auto)

  have "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} =

        prog_set x  \<union> mem_set y \<union> faults_set z "

    apply (unfold eq_i)

    by (metis (full_types) Un_insert_left Un_insert_right 

         diff_pc_set faults_set_def insert_commute insert_is_Un 

          pc_set_def sup_assoc sup_bot_left sup_commute)

  with h1(1) have in_r: "prog_set x \<union>  mem_set y \<union> faults_set z \<in> r" by auto

  show ?thesis

  proof(unfold rset_of.simps, rule stimesI[OF _ _ _ in_r])

    show "{At i''} \<in> pc i''" by (unfold pc_def pc_set_def, simp)

  next

    show "prog_set x \<union> pc_set i'' \<union> mem_set y \<union> faults_set z =

    {At i''} \<union> (prog_set x \<union> mem_set y \<union> faults_set z)"

      by (unfold pc_set_def, auto)

  next

    show "{At i''} \<inter> (prog_set x \<union> mem_set y \<union> faults_set z) = {}"

      by (auto simp:cpn_set_def)

  qed

qed

lemma condD: "s \<in> <b>*r \<Longrightarrow> b"

  by (unfold st_def pasrt_def, auto)

lemma condD1: "s \<in> <b>*r \<Longrightarrow> s \<in> r"

  by (unfold st_def pasrt_def, auto)

lemma hoare_dec_suc: "{(pc i * m a v) * <(v > 0)>} 

                          i:[\<guillemotright>(Dec a e) ]:j  

                      {pc j * m a (v - 1)}"

proof(unfold Hoare_abc_def, clarify)

  fix prog i' ab b r 

  assume h: "rset_of (prog, i', ab, b) \<in> ((pc i * m a v) * <(0 < v)>) * (i :[ \<guillemotright>Dec a e ]: j) * r"

                           (is "?r \<in> ?S")

  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"

  proof -

    from h [unfolded assemble_to.simps]

    have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a v * <(0 < v)> *  <(j = i + 1)> * r"

             "?r \<in>  m a v * pc i * {{C i (Dec a e)}} * <(0 < v)> *  <(j = i + 1)> * r"

             "?r \<in>   <(0 < v)> *  <(j = i + 1)> * m a v * pc i * {{C i (Dec a e)}} * r"

             "?r \<in>   <(j = i + 1)> * <(0 < v)> *   m a v * pc i * {{C i (Dec a e)}} * r"

      by ((metis stimes_ac)+)

    note h2 =  condD [OF h1(3)] condD[OF h1(4)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]

    hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> v - Suc 0), b)" (is "?x = ?y")

      by (unfold run_def, auto)

    have "rset_of ?x \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"

    proof -

      have "rset_of ?y \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"

      proof -

        from spc_upd[OF h1(1), of "Suc i"]

        have "rset_of (prog, (Suc i), ab, b) \<in> 

                m a v * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" 

          by (metis stimes_ac)

        from smem_upd[OF this, of "v - (Suc 0)"]

        have "rset_of ?y \<in> 

           m a (v - Suc 0) * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" .

        hence "rset_of ?y \<in> <(0 < v)> *

                (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r"

          by (metis stimes_ac)

        from condD1[OF this] 

        have "rset_of ?y \<in> (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r" .

        thus ?thesis

          by (unfold h2(2) assemble_to.simps, simp)

      qed

      with stp show ?thesis by simp

    qed

    thus ?thesis by blast

  qed

qed

lemma hoare_dec_fail: "{pc i * m a 0} 

                          i:[ \<guillemotright>(Dec a e) ]:j   

                       {pc e * m a 0}"

proof(unfold Hoare_abc_def, clarify)

  fix prog i' ab b r 

  assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"

                           (is "?r \<in> ?S")

  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"

  proof -

    from h [unfolded assemble_to.simps]

    have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a 0  *  <(j = i + 1)> * r"

             "?r \<in>  m a 0 * pc i * {{C i (Dec a e)}} *  <(j = i + 1)> * r"

             "?r \<in> <(j = i + 1)> * m a 0 * pc i * {{C i (Dec a e)}} * r"

      by ((metis stimes_ac)+)

    note h2 =  condD [OF h1(3)]  pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]

    hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y")

      by (unfold run_def, auto)

    have "rset_of ?x \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"

    proof -

      have "rset_of ?y \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"

      proof -

        from spc_upd[OF h1(1), of "e"]

        have "rset_of ?y \<in> pc e * {{C i (Dec a e)}} * m a 0 * <(j = i + 1)> * r" .

        thus ?thesis

          by (unfold assemble_to.simps, metis stimes_ac)

      qed

      with stp show ?thesis by simp

    qed

    thus ?thesis by blast

  qed

qed

lemma pasrtD_p: "\<lbrakk>{p*<b>} c {q}\<rbrakk> \<Longrightarrow> (b \<longrightarrow> {p} c {q})"

  apply (unfold Hoare_abc_def pasrt_def, auto)

  by (fold emp_def, simp add:emp_unit_r)

lemma hoare_dec: "dec_fun v j e = (pc', v') \<Longrightarrow> 

                    {pc i * m a v} 

                       i:[ \<guillemotright>(Dec a e) ]:j   

                    {pc pc' * m a v'}"

proof -

  assume "dec_fun v j e = (pc', v')"

  thus  "{pc i * m a v} 

                       i:[ \<guillemotright>(Dec a e) ]:j   

                    {pc pc' * m a v'}"

    apply (auto split:if_splits simp:dec_fun_def)

    apply (insert hoare_dec_fail, auto)[1]

    apply (insert hoare_dec_suc, auto)

    apply (atomize)

    apply (erule_tac x = i in allE, erule_tac x = a in allE,

           erule_tac x = v in allE, erule_tac x = e in allE, erule_tac x = pc' in allE)

    by (drule_tac pasrtD_p, clarify)

qed

lemma hoare_inc: "{pc i * m a v} 

                      i:[ \<guillemotright>(Inc a) ]:j   

                  {pc j * m a (v + 1)}"

proof(unfold Hoare_abc_def, clarify)

  fix prog i' ab b r 

  assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a v) * (i :[ \<guillemotright>Inc a ]: j) * r"

                           (is "?r \<in> ?S")

  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r"

  proof -

    from h [unfolded assemble_to.simps]

    have h1: "?r \<in> pc i * {{C i (Inc a)}} * m a v *  <(j = i + 1)> * r"

             "?r \<in>  m a v * pc i * {{C i (Inc a)}} * <(j = i + 1)> * r"

             "?r \<in>   <(j = i + 1)> * m a v * pc i * {{C i (Inc a)}} * r"

      by ((metis stimes_ac)+)

    note h2 =  condD [OF h1(3)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]

    hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> Suc v), b)" (is "?x = ?y")

      by (unfold run_def, auto)

    have "rset_of ?x \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a]: j) * r"

    proof -

      have "rset_of ?y \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r"

      proof -

        from spc_upd[OF h1(1), of "Suc i"]

        have "rset_of (prog, (Suc i), ab, b) \<in> 

                m a v * pc (Suc i) * {{C i (Inc a)}} * <(j = i + 1)> * r" 

          by (metis stimes_ac)

        from smem_upd[OF this, of "Suc v"]

        have "rset_of ?y \<in> 

           m a (v + 1) * pc (i + 1) * {{C i (Inc a)}} * <(j = i + 1)> * r" by simp

        thus ?thesis

          by (unfold h2(1) assemble_to.simps, metis stimes_ac)

      qed

      with stp show ?thesis by simp

    qed

    thus ?thesis by blast

  qed

qed

lemma hoare_goto: "{pc i} 

                      i:[ \<guillemotright>(Goto e) ]:j   

                   {pc e}"

proof(unfold Hoare_abc_def, clarify)

  fix prog i' ab b r 

  assume h: "rset_of (prog, i', ab, b) \<in> pc i * (i :[ \<guillemotright>Goto e ]: j) * r"

                           (is "?r \<in> ?S")

  show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> pc e * (i :[ \<guillemotright>Goto e ]: j) * r"

  proof -

    from h [unfolded assemble_to.simps]

    have h1: "?r \<in> pc i * {{C i (Goto e)}} *  <(j = i + 1)> * r"

      by ((metis stimes_ac)+)

    note h2 = pcD[OF h1(1)] codeD[OF h1(1)] 

    hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y")

      by (unfold run_def, auto)

    have "rset_of ?x \<in> pc e * (i :[ \<guillemotright>Goto e]: j) * r"

    proof -

      from spc_upd[OF h1(1), of "e"] 

      show ?thesis

        by (unfold stp assemble_to.simps, metis stimes_ac)

    qed

    thus ?thesis by blast

  qed

qed

no_notation stimes (infixr "*" 70)

interpretation foo: comm_monoid_mult 

  "stimes :: 'a set set => 'a set set => 'a set set" "emp::'a set set"

apply(default)

apply(simp add: stimes_assoc)

apply(simp add: stimes_comm)

apply(simp add: emp_def[symmetric])

done

notation stimes (infixr "*" 70)

(*used by simplifier for numbers *)

thm mult_cancel_left

(*

interpretation foo: comm_ring_1 "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set" 

apply(default)

*)

lemma frame: "{p} c {q} \<Longrightarrow>  \<forall> r. {p * r} c {q * r}"

apply (unfold Hoare_abc_def, clarify)

apply (erule_tac x = "(a, aa, ab, b)" in allE)

apply (erule_tac x = "r * ra" in allE) 

apply(metis stimes_ac)

done

lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})"

  apply (unfold Hoare_abc_def, clarify)

  apply (erule_tac x = "(a, aa, ab, b)" in allE)

  apply (erule_tac x = "e * r" in allE)

  apply(metis stimes_ac)

  done

lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"

apply (unfold run_def)

by (metis funpow_add o_apply)

lemma composition: "\<lbrakk>{p} c1 {q}; {q} c2 {r}\<rbrakk> \<Longrightarrow> {p} c1 * c2 {r}"

proof -

  assume h: "{p} c1 {q}" "{q} c2 {r}"

  from code_extension [OF h(1), rule_format, of "c2"] 

  have "{p} c1 * c2 {q}" .

  moreover from code_extension [OF h(2), rule_format, of "c1"] and stimes_comm

  have "{q} c1 * c2 {r}" by metis

  ultimately show "{p} c1 * c2 {r}"

    apply (unfold Hoare_abc_def, clarify)

    proof -

      fix a aa ab b ra

      assume h1: "\<forall>s r. rset_of s \<in> p * (c1 * c2) * r \<longrightarrow>

                       (\<exists>k. rset_of (run k s) \<in> q * (c1 * c2) * r)"

        and h2: "\<forall>s ra. rset_of s \<in> q * (c1 * c2) * ra \<longrightarrow>

                       (\<exists>k. rset_of (run k s) \<in> r * (c1 * c2) * ra)"

        and h3: "rset_of (a, aa, ab, b) \<in> p * (c1 * c2) * ra"

      show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> r * (c1 * c2) * ra"

      proof -

        let ?s = "(a, aa, ab, b)"

        from h1 [rule_format, of ?s, OF h3]

        obtain n1 where "rset_of (run n1 ?s) \<in> q * (c1 * c2) * ra" by blast

        from h2 [rule_format, OF this]

        obtain n2 where "rset_of (run n2 (run n1 ?s)) \<in> r * (c1 * c2) * ra" by blast

        with run_add show ?thesis by metis

      qed

    qed

qed

lemma stimes_simp: "s \<in> x * y = (\<exists> s1 s2. (s = s1 \<union> s2 \<and> s1 \<inter> s2 = {} \<and> s1 \<in> x \<and> s2 \<in> y))"

by (metis (lifting) stimesE stimesI)

lemma hoare_seq: 

  "\<lbrakk>\<forall> i j. {pc i * p} i:[c1]:j {pc j * q}; 

    \<forall> j k. {pc j * q} j:[c2]:k {pc k * r}\<rbrakk> \<Longrightarrow>  {pc i * p} i:[(c1 ; c2)]:k {pc k *r}"

proof -

  assume h: "\<forall>i j. {pc i * p} i :[ c1 ]: j {pc j * q}" "\<forall> j k. {pc j * q} j:[c2]:k {pc k * r}"

  show "{pc i * p} i:[(c1 ; c2)]:k {pc k *r}"

  proof(subst Hoare_abc_def, clarify)

    fix a aa ab b ra

    assume "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ (c1 ; c2) ]: k) * ra"

    hence "rset_of (a, aa, ab, b) \<in> (i :[ (c1 ; c2) ]: k) * (pc i * p * ra)" (is "?s \<in> ?X * ?Y")

      by (metis stimes_ac)

    from stimesE[OF this] obtain s1 s2 where

      sp: "rset_of(a, aa, ab, b) = s1 \<union> s2" "s1 \<inter> s2 = {}" "s1 \<in> ?X" "s2 \<in> ?Y" by blast

    from sp (3) obtain j' where 

      "s1 \<in> (i:[c1]:j') * (j':[c2]:k)" (is "s1 \<in> ?Z")

      by (auto simp:assemble_to.simps)

    from stimesI[OF sp(1, 2) this sp(4)]

    have "?s \<in>  (pc i * p) * (i :[ c1 ]: j') * (j' :[ c2 ]: k) * ra" by (metis stimes_ac)

    from h(1)[unfolded Hoare_abc_def, rule_format, OF this]

    obtain ka where 

      "rset_of (run ka (a, aa, ab, b)) \<in> (pc j' * q) * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" 

      sorry

    from h(2)[unfolded Hoare_abc_def, rule_format, OF this]

    obtain kb where 

      "rset_of (run kb (run ka (a, aa, ab, b)))

      \<in>  (pc k * r) * (j' :[ c2 ]: k) * (i :[ c1 ]: j') * ra" by blast

    hence h3: "rset_of (run (kb + ka) (a, aa, ab, b))