header {* 
 {\em abacus} a kind of register machine
*}

theory abacus
imports Main (*StateMonad*)
begin

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


fun splits :: "'a set \<Rightarrow> ('a set \<times> 'a set) \<Rightarrow> bool"
where "splits s (u, v) = (u \<union> v = s \<and> u \<inter> v = {})"

declare splits.simps [simp del]

definition "stimes p q = {s . \<exists> u v. u \<in> p \<and> v \<in> q \<and> splits s (u, v)}"
lemmas st_def = stimes_def[unfolded splits.simps]

notation stimes (infixr "*" 70)

lemma stimes_comm: "(p::('a set set)) * q = q * p"
  by (unfold st_def, auto)

lemma splits_simp: "splits s (u, v) = (v = (s - u) \<and> v \<subseteq> s \<and> u \<subseteq> s)"
  by (unfold splits.simps, auto)

lemma stimes_assoc: "p * q * r = (p * q) * (r::'a set set)"
  by (unfold st_def, blast)

definition
  "emp = {{}}"

lemma emp_unit_r [simp]: "p * emp = p"
  by (unfold st_def emp_def, auto)

lemma emp_unit_l [simp]: "emp * p = p"
  by (metis emp_unit_r stimes_comm)

lemma stimes_mono: "p \<subseteq> q \<Longrightarrow> p * r \<subseteq> q * r"
  by (unfold st_def, auto)

lemma stimes_left_commute:
  "(q * (p * r)) = ((p::'a set set) * (q * r))"
by (metis stimes_assoc stimes_comm)

lemmas stimes_ac = stimes_comm stimes_assoc stimes_left_commute

lemma "x * y * z = z * y * (x::'a set set)"
by (metis stimes_ac)


definition pasrt :: "bool \<Rightarrow> ('a set set)" ("<_>" [71] 71)
where "pasrt b = {s . s = {} \<and> b}"

datatype apg = 
   Instr abc_inst
 | Label nat
 | Seq apg apg
 | Local "(nat \<Rightarrow> apg)"

notation Local (binder "LOCAL " 10)

term "LOCAL a b. Seq (Label a) (Label b)"



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

abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixl ";" 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 "pc l = {pc_set l}"


definition "m a v = {{M a v}}"


declare rset_of.simps[simp del]

type_synonym assert = "aresource set set"

primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" 
  where 
  "assemble_to (Instr ai) i j = ({{C i ai}} * <(j = i + 1)>)" |
  "assemble_to (Seq p1 p2) i j = (\<Union> j'. (assemble_to p1 i j') * (assemble_to p2 j' j))" |
  "assemble_to (Local fp) i j  = (\<Union> l. (assemble_to (fp l) i j))" |
  "assemble_to (Label l) i j = <(i = j \<and> j = l)>"

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: "s \<in> {x} * q \<Longrightarrow> (s - x) \<in> q \<and> x \<subseteq> s"
  apply (unfold st_def, auto)
by (smt Diff_disjoint Un_Diff_cancel2 Un_Int_distrib 
     Un_commute Un_empty_right Un_left_absorb)

lemma pcD: "rset_of (prog, i', mem, fault) \<in> pc i * r
       \<Longrightarrow> i' = i"
proof -
  assume "rset_of (prog, i', mem, fault) \<in> pc i * r"
  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: "rset_of (prog, pos, mem, fault) \<in>  pc i * {{C i inst}} * r
       \<Longrightarrow> prog pos = Some inst"
proof -
  assume h: "rset_of (prog, pos, mem, fault) \<in>  pc i * {{C i inst}} * r" (is "?c \<in> ?X")
  from pcD[OF this] have "i = pos" by simp
  with h show ?thesis
    by (unfold rset_of.simps st_def pc_def prog_set_def 
      pc_set_def mem_set_def faults_set_def, auto)
qed

lemma memD: "rset_of (prog, pos, mem, fault) \<in>  (m a v)  * r \<Longrightarrow> mem a = Some v"
proof -
  assume "rset_of (prog, pos, mem, fault) \<in>  (m a v)  * r"
  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. (rset_of s) \<in> (p*c*r) \<longrightarrow>
    (\<exists> k. ((rset_of (run k s)) \<in> (q*c*r))))" 

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 stimesE:
  assumes h: "s \<in> x * y"
  obtains s1 s2 where "s = s1 \<union> s2" and "s1 \<inter> s2 = {}" and "s1 \<in> x" and "s2 \<in> y"
  by (insert h, auto simp:st_def)

lemma stimesI: 
  "\<lbrakk>s = s1 \<union> s2; s1 \<inter> s2 = {}; s1 \<in> x; s2 \<in> y\<rbrakk> \<Longrightarrow> s \<in> x * y"
  by (auto simp:st_def)

lemma smem_upd: "(rset_of (x, y, mem, f)) \<in> (m a v)*r \<Longrightarrow> 
                    (rset_of (x, y, mem(a := Some v'), f) \<in> (m a v')*r)"
proof -
  assume h: " rset_of (x, y, mem, f) \<in> m a v * r"
  from h[unfolded rset_of.simps m_def]
  have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f \<in> {{M a v}} * r" .
  from stimes_sgD [OF this]
  have h1: "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} \<in> r"
           "{M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f" by auto
  moreover have "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)
  ultimately have h0: "prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f \<in> r" 
    by simp
  from h1(2) and M_in_simp have "{M a v} \<subseteq> mem_set mem" by simp
  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 "mem_set (mem(a \<mapsto> v')) \<union>  prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r"
    proof(rule stimesI[OF _ _ _ h0])
      show "{M a v'} \<in> m a v'" by (unfold m_def, auto)
    next
      show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f =
             {M a v'} \<union> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"
        apply (unfold h2(1))
        by (smt Un_commute Un_insert_left Un_insert_right 
             Un_left_commute 
                  `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`)
    next
      from h2(2)
      show "{M a v'} \<inter> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f) = {}"
        by (unfold cpn_set_def, auto)
    qed
    thus ?thesis 
      apply (unfold rset_of.simps)
      by (metis `mem_set (mem(a \<mapsto> v')) 
            \<union> prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r` 
         stimes_comm sup_commute sup_left_commute)
  qed
qed

lemma spc_upd: "rset_of (x, i, y, z) \<in> pc i' * r \<Longrightarrow> 
                rset_of (x, i'', y, z) \<in> pc i'' * r"
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))
      \<in> pc k * r * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" 
      sorry
    hence "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> pc k * r * (i :[ (c1 ; c2) ]: k) * ra"
    proof -
      have "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> (i :[ (c1 ; c2) ]: k) * (pc k * r * ra)"
      proof -
        from h3 have "rset_of (run (kb + ka) (a, aa, ab, b))
          \<in> ((j' :[ c2 ]: k) * ((i :[ c1 ]: j'))) * (pc k * r *  ra)"
          by (metis stimes_ac)
        then obtain 
          s1 s2 where h4: "rset_of (run (kb + ka) (a, aa, ab, b)) = s1 \<union> s2"
          " s1 \<inter> s2 = {}" "s1 \<in> (j' :[ c2 ]: k) * (i :[ c1 ]: j')"
          "s2 \<in>  pc k * r * ra" by (rule stimesE, blast)
        from h4(3) have "s1 \<in> (i :[ (c1 ; c2) ]: k)"
          sorry
        from stimesI [OF h4(1, 2) this h4(4)]
        show ?thesis .
      qed
      thus ?thesis by (metis stimes_ac)
    qed
    thus "\<exists>ka. rset_of (run ka (a, aa, ab, b)) \<in> (pc k * r) * (i :[ (c1 ; c2) ]: k) * ra"
      by (metis stimes_ac)
  qed
qed
  
lemma hoare_local: 
  "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} 
  \<Longrightarrow> {pc i * p} i:[Local c]:j {pc j * q}"
proof -
  assume h: "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} "
  show "{pc i * p} i:[Local c]:j {pc j * q}"
  proof(unfold assemble_to.simps Hoare_abc_def, clarify)
    fix a aa ab b r
    assume h1: "rset_of (a, aa, ab, b) \<in> (pc i * p) * (\<Union>l. i :[ c l ]: j) * r"
    hence "rset_of (a, aa, ab, b) \<in> (\<Union>l. i :[ c l ]: j) * (pc i * p * r)" 
      by (metis stimes_ac)
    then obtain s1 s2 l 
      where "rset_of (a, aa, ab, b) = s1 \<union> s2"
                "s1 \<inter> s2 = {}"
                "s1 \<in> (i :[ c l ]: j)"
                "s2 \<in> pc i * p * r"
      by (rule stimesE, auto)
    from stimesI[OF this]
    have "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ c l ]: j) * r" 
      by (metis stimes_ac)
    from h[unfolded Hoare_abc_def, rule_format, OF this]
    obtain k where "rset_of (run k (a, aa, ab, b)) \<in> (i :[ c l ]: j) * (pc j * q * r)" 
      sorry
    then obtain s1 s2
      where h3: "rset_of (run k (a, aa, ab, b)) = s1 \<union> s2"
                " s1 \<inter> s2 = {}" "s1 \<in> (\<Union> l. (i :[ c l ]: j))" "s2 \<in> pc j * q * r" 
      by(rule stimesE, auto)
    from stimesI[OF this]
    show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> (pc j * q) * (\<Union>l. i :[ c l ]: j) * r"
      by (metis stimes_ac)
  qed
qed

lemma move_pure: "{p*<b>} c {q} = (b \<longrightarrow> {p} c {q})"
proof(unfold Hoare_abc_def, default, clarify)
  fix prog i' mem ft r
  assume h: "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
            "b" "rset_of (prog, i', mem, ft) \<in> p * c * r"
  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r"
  proof(rule h(1)[rule_format])
    have "(p * <b>) * c * r = <b> * p * c * r" by (metis stimes_ac)
    moreover have "rset_of (prog, i', mem, ft) \<in> \<dots>"
    proof(rule stimesI[OF _ _ _ h(3)])
      from h(2) show "{} \<in> <b>" by (auto simp:pasrt_def)
    qed auto
    ultimately show "rset_of (prog, i', mem, ft) \<in> (p * <b>) * c * r"
      by (simp)
  qed
next
  assume h: "b \<longrightarrow> (\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r))"
  show "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
  proof -
    { fix s r 
      assume "rset_of s \<in> (p * <b>) * c * r"
      hence h1: "rset_of s \<in> <b> * p * c * r" by (metis stimes_ac)
      have "(\<exists>k. rset_of (run k s) \<in> q * c * r)"
      proof(rule h[rule_format])
        from condD[OF h1] show b .
      next
        from condD1[OF h1] show "rset_of s \<in> p * c * r" .
      qed
    } thus ?thesis by blast
  qed
qed

lemma precond_ex: "{\<Union> x. p x} c {q} = (\<forall> x. {p x} c {q})"
proof(unfold Hoare_abc_def, default, clarify)
  fix x prog i' mem ft r
  assume h: "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
            "rset_of (prog, i', mem, ft) \<in> p x * c * r"
  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r"
  proof(rule h[rule_format])
    from h(2) show "rset_of (prog, i', mem, ft) \<in> UNION UNIV p * c * r" by (auto simp:stimes_def)
  qed
next
  assume h: "\<forall>x s r. rset_of s \<in> p x * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
  show "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
  proof -
    { fix s r
      assume "rset_of s \<in> UNION UNIV p * c * r"
      then obtain x where "rset_of s \<in> p x * c * r" 
        by (unfold st_def, auto, metis)
      hence "(\<exists>k. rset_of (run k s) \<in> q * c * r)"
        by(rule h[rule_format])
    } thus ?thesis by blast
  qed
qed

lemma pre_stren: "\<lbrakk>{p} c {q}; r \<subseteq> p\<rbrakk> \<Longrightarrow> {r} c {q}"
proof(unfold Hoare_abc_def, clarify)
  fix prog i' mem ft r'
  assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
            " r \<subseteq> p" " rset_of (prog, i', mem, ft) \<in> r * c * r'"
  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'"
  proof(rule h(1)[rule_format])
    from stimes_mono[OF h(2), of "c * r'"] h(3)
    show "rset_of (prog, i', mem, ft) \<in> p * c * r'" by auto
  qed
qed

lemma post_weaken: "\<lbrakk>{p} c {q}; q \<subseteq> r\<rbrakk> \<Longrightarrow> {p} c {r}"
proof(unfold Hoare_abc_def, clarify)
  fix prog i' mem ft r'
  assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"
            " q \<subseteq> r" "rset_of (prog, i', mem, ft) \<in> p * c * r'"
  show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> r * c * r'"
  proof -
    from h(1)[rule_format, OF h(3)]
    obtain k where "rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'" by auto
    moreover from h(2) have "\<dots> \<subseteq> r * c * r'" by (metis stimes_mono)
    ultimately show ?thesis by auto
  qed
qed

end
