tm2: thys/Hoare_abc.thy@192672a6fff4

header {* 
 {\em Abacus} defined as macros of TM
 *}

theory Hoare_abc
imports Hoare_tm Finite_Set
begin


text {*
  {\em Abacus} instructions
*}

(*
text {* The following Abacus instructions will be replaced by TM macros. *}
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 aresource = 
    M nat nat
  (* | C nat abc_inst *) (* C resource is not needed because there is no Abacus code any more *)  
  | At nat
  | Faults nat


section {* An interpretation from Abacus to Turing Machine *}

fun recse_map :: "nat list \<Rightarrow> aresource \<Rightarrow> tassert" where
  "recse_map ks (M a v) = <(a < length ks \<and> ks!a = v \<or> a \<ge> length ks \<and> v = 0)>" |
  "recse_map ks (At l) = st l" |
  "recse_map ks (Faults n) = sg {TFaults n}"

definition "IA ars = (EXS ks i. ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* (reps 2 i ks) \<and>* 
                                     fam_conj {i<..} zero \<and>* 
                                fam_conj ars (recse_map ks))"


section {* A virtually defined Abacus *}

text {* The following Abacus instructions are to be defined as TM macros *}

definition "pc l = sg {At l}"

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

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

lemma tm_hoare_inc1:
  assumes h: "a < length ks \<and> ks ! a = v \<or> length ks \<le> a \<and> v = 0"
  shows "
    \<lbrace>st i \<and>* ps u \<and>* zero (u - 2) \<and>* zero (u - 1) \<and>* reps u ia ks \<and>* fam_conj {ia<..} zero\<rbrace> 
    i :[Inc a ]: j
    \<lbrace>st j \<and>*
     ps u \<and>*
     zero (u - 2) \<and>*
     zero (u - 1) \<and>*
     reps u (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>*
     fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero\<rbrace>"
  using h
proof
  assume hh: "a < length ks \<and> ks ! a = v"
  hence "a < length ks" by simp 
  from list_ext_lt [OF this] tm_hoare_inc00[OF hh]
  show ?thesis by simp
next
  assume "length ks \<le> a \<and> v = 0"
  from tm_hoare_inc01[OF this]
  show ?thesis by simp
qed

lemma tm_hoare_inc2: 
  assumes "mm a v sr"
  shows "
    \<lbrace> (fam_conj sr (recse_map ks) \<and>*
       st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<rbrace> 
          i:[ (Inc a) ]:j   
    \<lbrace> (fam_conj {M a (Suc v)} (recse_map (list_ext a ks[a := Suc v])) \<and>*
           st j \<and>*
           ps 2 \<and>*
           zero 0 \<and>*
           zero 1 \<and>*
           reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>*
           fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero)\<rbrace>"
proof -
  from `mm a v sr` have eq_sr: "sr = {M a v}" by (auto simp:mm_def sg_def)
  from tm_hoare_inc1[where u = 2]
  have "a < length ks \<and> ks ! a = v \<or> length ks \<le> a \<and> v = 0 \<Longrightarrow>
        \<lbrace>st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero\<rbrace> 
             i :[Inc a ]: j
        \<lbrace>(st j \<and>*
           ps 2 \<and>*
           zero 0 \<and>*
           zero 1 \<and>*
           reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1) ((list_ext a ks)[a := Suc v]) \<and>*
           fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1<..} zero)\<rbrace>" by simp
  thus ?thesis
    apply (unfold eq_sr)
    apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)
    by (rule tm.pre_condI, blast)
qed

locale IA_disjoint = 
  fixes s s' s1 cnf
  assumes h_IA: "IA (s + s') s1"
  and h_disj: "s ## s'"
  and h_conf: "s1 \<subseteq> trset_of cnf"
begin

lemma at_disj1: 
  assumes at_in: "At i \<in> s"
  shows "At j \<notin> s'"
proof
  from h_IA[unfolded IA_def]
  obtain ks idx
    where "((ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* 
              reps 2 idx ks \<and>* fam_conj {idx<..} zero) \<and>* 
              fam_conj (s + s') (recse_map ks)) s1" (is "(?P \<and>* ?Q) s1")
    by (auto elim!:EXS_elim simp:sep_conj_ac)
  then obtain ss1 ss2 where "s1 = ss1 + ss2" "ss1 ## ss2" "?P ss1" "?Q ss2"
    by (auto elim:sep_conjE)
  from `?Q ss2`[unfolded fam_conj_disj_simp[OF h_disj]]
  obtain tt1 tt2
    where "ss2 = tt1 + tt2" "tt1 ## tt2" 
            "(fam_conj s (recse_map ks)) tt1"
            "(fam_conj s' (recse_map ks)) tt2"
    by (auto elim:sep_conjE)
  assume "At j \<in> s'"
  from `(fam_conj s' (recse_map ks)) tt2` [unfolded fam_conj_elm_simp[OF this]]
       `ss2 = tt1 + tt2` `s1 = ss1 + ss2` h_conf
  have "TAt j \<in> trset_of cnf"
    by (auto elim!:sep_conjE simp: st_def sg_def tpn_set_def set_ins_def)
  moreover from `(fam_conj s (recse_map ks)) tt1` [unfolded fam_conj_elm_simp[OF at_in]]
                `ss2 = tt1 + tt2` `s1 = ss1 + ss2` h_conf
  have "TAt i \<in> trset_of cnf"
    by (auto elim!:sep_conjE simp: st_def sg_def tpn_set_def set_ins_def)
  ultimately have "i = j"
    by (cases cnf, simp add:trset_of.simps tpn_set_def)
  from at_in `At j \<in> s'` h_disj
  show False 
    by (unfold `i = j`, auto simp:set_ins_def)
qed

lemma at_disj2: "At i \<in> s' \<Longrightarrow> At j \<notin> s"
  by (metis at_disj1)

lemma m_disj1: 
  assumes m_in: "M a v \<in> s"
  shows "M a v' \<notin> s'"
proof
  from h_IA[unfolded IA_def]
  obtain ks idx
    where "((ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* 
              reps 2 idx ks \<and>* fam_conj {idx<..} zero) \<and>* 
              fam_conj (s + s') (recse_map ks)) s1" (is "(?P \<and>* ?Q) s1")
    by (auto elim!:EXS_elim simp:sep_conj_ac)
  then obtain ss1 ss2 where "s1 = ss1 + ss2" "ss1 ## ss2" "?P ss1" "?Q ss2"
    by (auto elim:sep_conjE)
  from `?Q ss2`[unfolded fam_conj_disj_simp[OF h_disj]]
  obtain tt1 tt2
    where "ss2 = tt1 + tt2" "tt1 ## tt2" 
            "(fam_conj s (recse_map ks)) tt1"
            "(fam_conj s' (recse_map ks)) tt2"
    by (auto elim:sep_conjE)
  assume "M a v' \<in> s'"
  from `(fam_conj s' (recse_map ks)) tt2` [unfolded fam_conj_elm_simp[OF this]
        recse_map.simps]
  have "(a < length ks \<and> ks ! a = v' \<or> length ks \<le> a \<and> v' = 0)"
    by (auto simp:pasrt_def)
  moreover from `(fam_conj s (recse_map ks)) tt1` [unfolded fam_conj_elm_simp[OF m_in]
                         recse_map.simps]
  have "a < length ks \<and> ks ! a = v \<or> length ks \<le> a \<and> v = 0"
    by (auto simp:pasrt_def)
  moreover note m_in `M a v' \<in> s'` h_disj
  ultimately show False
    by (auto simp:set_ins_def)
qed

lemma m_disj2: "M a v \<in> s' \<Longrightarrow> M a v' \<notin> s"
  by (metis m_disj1)

end

lemma EXS_elim1: 
  assumes "((EXS x. P(x)) \<and>* r) s"
  obtains x where "(P(x) \<and>* r) s"
  by (metis EXS_elim assms sep_conj_exists1)

lemma hoare_inc[step]: "IA. \<lbrace> pc i ** mm a v \<rbrace> 
                        i:[ (Inc a) ]:j   
                      \<lbrace> pc j ** mm a (Suc v)\<rbrace>"
                      (is "IA. \<lbrace> pc i ** ?P \<rbrace> 
                        i:[ ?code ?e ]:j   
                      \<lbrace> pc ?e ** ?Q\<rbrace>")
proof(induct rule:tm.IHoareI)
  case (IPre s' s r cnf)
  let ?cnf = "(trset_of cnf)"
  from IPre
  have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"
    by (metis condD)+
  from h(1) obtain sr where
      eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"
    by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def)
  hence "At i \<in> s" by auto
  from h(3) obtain s1 s2 s3
    where hh: "?cnf = s1 + s2 + s3"
              "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 
              "IA (s + s') s1" 
              "(i :[ ?code ?e ]: j) s2"
              "r s3"
    apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
    by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)
  interpret ia_disj: IA_disjoint s s' s1 cnf
  proof
    from `IA (s + s') s1` show "IA (s + s') s1" .
  next
    from `s ## s'` show "s ## s'" .
  next
    from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  qed
  from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  from hh(3)
  have "(EXS ks ia.
         ps 2 \<and>*
         zero 0 \<and>*
         zero 1 \<and>*
         reps 2 ia ks \<and>*
         fam_conj {ia<..} zero \<and>*
         (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))
        s1"
    apply (unfold IA_def fam_conj_disj_simp[OF h(2)])
    apply (unfold eq_s)
    by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)
  then obtain ks ia
    where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*
             reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 
    (is "(?PP \<and>* ?QQ) s1")
    by (unfold pred_ex_def, auto simp:sep_conj_ac)
  then obtain ss1 ss2 where pres:
        "s1 = ss1 + ss2" "ss1 ## ss2"
        "?PP ss1"
        "?QQ ss2"
    by (auto elim!:sep_conjE intro!:sep_conjI)
  from ia_disj.at_disj1 [OF `At i \<in> s`]
  have at_fresh_s': "At ?e \<notin>  s'" .
  have at_fresh_sr: "At ?e \<notin> sr"
  proof
    assume at_in: "At ?e \<in> sr"
    from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]
    have "TAt ?e \<in> trset_of cnf"
      apply (elim EXS_elim1)
      apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]
             fam_conj_elm_simp[OF at_in])
      apply (erule_tac sep_conjE, unfold set_ins_def)+
      by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)
    moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 
      apply(erule_tac sep_conjE)
      apply(erule_tac sep_conjE)
      by (auto simp:st_def tpc_set_def sg_def set_ins_def)
    ultimately have "i = ?e"
      by (cases cnf, auto simp:tpn_set_def trset_of.simps)
    from eq_s[unfolded this] at_in
    show "False" by (auto simp:set_ins_def)
  qed
  from pres(3) and hh(2, 4, 5) pres(2, 4)
  have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))
         (trset_of cnf)"
    apply (unfold hh(1) pres(1))
    apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)
    by (auto simp:set_ins_def)
  (*****************************************************************************)
  let ?ks_f = "\<lambda> sr ks. list_ext a ks[a := Suc v]"
  let ?elm_f = "\<lambda> sr. {M a (Suc v)}"
  let ?idx_f = "\<lambda> sr ks ia. (ia + int (reps_len (list_ext a ks)) - int (reps_len ks) + 1)"
  (*----------------------------------------------------------------------------*)
  (******************************************************************************)
  from tm_hoare_inc2 [OF eq_s(3), unfolded tm.Hoare_gen_def, rule_format, OF pres1]
  obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*
        st ?e \<and>*
        ps 2 \<and>*
        zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 
        fam_conj {?idx_f sr ks ia<..} zero) \<and>*
       i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))
       (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast
  (*----------------------------------------------------------------------------*)
  moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"
  proof -
    have "pc ?e {At ?e}" by (simp add:pc_def sg_def)
  (******************************************************************************)
    moreover have "?Q (?elm_f sr)" 
      by (simp add:mm_def sg_def)
  (*----------------------------------------------------------------------------*)
    moreover 
  (******************************************************************************)
    have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)
  (*----------------------------------------------------------------------------*)
    ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)
  qed
  moreover 
  (******************************************************************************)
  from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 
  have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)
  (*----------------------------------------------------------------------------*)
  with at_fresh_s' 
  have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)
  moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 
                           (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
  proof -
    fix elm
    assume elm_in: "elm \<in> s'"
    show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
    proof(cases elm)
      (*******************************************************************)
      case (M a' v')
      from eq_s have "M a v \<in> s" by (auto simp:set_ins_def mm_def sg_def)
      with elm_in ia_disj.m_disj1[OF this] M
      have "a \<noteq> a'" by auto
      thus ?thesis
        apply (auto simp:M recse_map.simps pasrt_def list_ext_len)
        apply (case_tac "a < length ks", auto simp:list_ext_len_eq list_ext_lt)
        apply (case_tac "a' < Suc a", auto simp:list_ext_len_eq list_ext_lt)
        by (metis (full_types) bot_nat_def 
              leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)
      (*-----------------------------------------------------------------*)
    qed auto
  qed
  ultimately show ?case 
    apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
    apply (unfold IA_def, intro condI, assumption+)
    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
    apply (unfold fam_conj_disj_simp[OF fresh_atm])
    apply (auto simp:sep_conj_ac fam_conj_simps)
    (***************************************************************************)
    (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *)
    (*-------------------------------------------------------------------------*)
    apply (sep_cancel)+
    by (simp add: fam_conj_ext_eq[where I = "s'", OF eq_map])
qed

lemma tm_hoare_dec_fail:
  assumes "mm a 0 sr"
  shows 
  "\<lbrace> fam_conj sr (recse_map ks) \<and>*
    st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace> 
       i:[ (Dec a e) ]:j 
   \<lbrace> fam_conj {M a 0} (recse_map (list_ext a ks[a := 0])) \<and>*
     st e \<and>*
     ps 2 \<and>*
     zero 0 \<and>*
     zero 1 \<and>*
     reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>*
     fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks) <..} zero\<rbrace>"
proof - 
  from `mm a 0 sr` have eq_sr: "sr = {M a 0}" by (auto simp:mm_def sg_def)
  { assume h: "a < length ks \<and> ks ! a = 0 \<or> length ks \<le> a"
    from tm_hoare_dec_fail1[where u = 2, OF this]
    have "\<lbrace>st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero\<rbrace>  
                  i :[ Dec a e ]: j
          \<lbrace>st e \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*
            reps 2 (ia + int (reps_len (list_ext a ks)) - int (reps_len ks)) (list_ext a ks[a := 0]) \<and>*
            fam_conj {ia + int (reps_len (list_ext a ks)) - int (reps_len ks)<..} zero\<rbrace>"
    by (simp)
  }
  thus ?thesis
    apply (unfold eq_sr)
    apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)
    by (rule tm.pre_condI, blast)
qed

lemma hoare_dec_fail: "IA. \<lbrace> pc i ** mm a 0 \<rbrace>
                              i:[ (Dec a e) ]:j   
                           \<lbrace> pc e ** mm a 0 \<rbrace>"
                      (is "IA. \<lbrace> pc i ** ?P \<rbrace> 
                                i:[ ?code ?e]:j   
                               \<lbrace> pc ?e ** ?Q\<rbrace>")
proof(induct rule:tm.IHoareI)
  case (IPre s' s r cnf)
  let ?cnf = "(trset_of cnf)"
  from IPre
  have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"
    by (metis condD)+
  from h(1) obtain sr where
      eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"
    by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def)
  hence "At i \<in> s" by auto
  from h(3) obtain s1 s2 s3
    where hh: "?cnf = s1 + s2 + s3"
              "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 
              "IA (s + s') s1" 
              "(i :[ ?code ?e ]: j) s2"
              "r s3"
    apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
    by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)
  interpret ia_disj: IA_disjoint s s' s1 cnf
  proof
    from `IA (s + s') s1` show "IA (s + s') s1" .
  next
    from `s ## s'` show "s ## s'" .
  next
    from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  qed
  from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  from hh(3)
  have "(EXS ks ia.
         ps 2 \<and>*
         zero 0 \<and>*
         zero 1 \<and>*
         reps 2 ia ks \<and>*
         fam_conj {ia<..} zero \<and>*
         (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))
        s1"
    apply (unfold IA_def fam_conj_disj_simp[OF h(2)])
    apply (unfold eq_s)
    by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)
  then obtain ks ia
    where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*
             reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 
    (is "(?PP \<and>* ?QQ) s1")
    by (unfold pred_ex_def, auto simp:sep_conj_ac)
  then obtain ss1 ss2 where pres:
        "s1 = ss1 + ss2" "ss1 ## ss2"
        "?PP ss1"
        "?QQ ss2"
    by (auto elim!:sep_conjE intro!:sep_conjI)
  from ia_disj.at_disj1 [OF `At i \<in> s`]
  have at_fresh_s': "At ?e \<notin>  s'" .
  have at_fresh_sr: "At ?e \<notin> sr"
  proof
    assume at_in: "At ?e \<in> sr"
    from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]
    have "TAt ?e \<in> trset_of cnf"
      apply (elim EXS_elim1)
      apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]
             fam_conj_elm_simp[OF at_in])
      apply (erule_tac sep_conjE, unfold set_ins_def)+
      by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)
    moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 
      apply(erule_tac sep_conjE)
      apply(erule_tac sep_conjE)
      by (auto simp:st_def tpc_set_def sg_def set_ins_def)
    ultimately have "i = ?e"
      by (cases cnf, auto simp:tpn_set_def trset_of.simps)
    from eq_s[unfolded this] at_in
    show "False" by (auto simp:set_ins_def)
  qed
  from pres(3) and hh(2, 4, 5) pres(2, 4)
  have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))
         (trset_of cnf)"
    apply (unfold hh(1) pres(1))
    apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)
    by (auto simp:set_ins_def)
  (*****************************************************************************)
  let ?ks_f = "\<lambda> sr ks. list_ext a ks[a:=0]"
  let ?elm_f = "\<lambda> sr. {M a 0}"
  let ?idx_f = "\<lambda> sr ks ia. (ia + int (reps_len (list_ext a ks)) - int (reps_len ks))"
  (*----------------------------------------------------------------------------*)
  (******************************************************************************)
  from tm_hoare_dec_fail[OF `?P sr`, unfolded tm.Hoare_gen_def, rule_format, OF pres1]
  obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*
        st ?e \<and>*
        ps 2 \<and>*
        zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 
        fam_conj {?idx_f sr ks ia<..} zero) \<and>*
       i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))
       (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast
  (*----------------------------------------------------------------------------*)
  moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"
  proof -
    have "pc ?e {At ?e}" by (simp add:pc_def sg_def)
  (******************************************************************************)
    moreover have "?Q (?elm_f sr)" 
      by (simp add:mm_def sg_def)
  (*----------------------------------------------------------------------------*)
    moreover 
  (******************************************************************************)
    have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)
  (*----------------------------------------------------------------------------*)
    ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)
  qed
  moreover 
  (******************************************************************************)
  from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 
  have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)
  (*----------------------------------------------------------------------------*)
  with at_fresh_s' 
  have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)
  moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 
                           (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
  proof -
    fix elm
    assume elm_in: "elm \<in> s'"
    show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
    proof(cases elm)
      (*******************************************************************)
      case (M a' v')
      from eq_s have "M a 0 \<in> s" by (auto simp:set_ins_def mm_def sg_def)
      with elm_in ia_disj.m_disj1[OF this] M
      have "a \<noteq> a'" by auto
      thus ?thesis
        apply (auto simp:M recse_map.simps pasrt_def list_ext_len)
        apply (case_tac "a < length ks", auto simp:list_ext_len_eq list_ext_lt)
        apply (case_tac "a' < Suc a", auto simp:list_ext_len_eq list_ext_lt)
        by (metis (full_types) bot_nat_def 
              leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)
      (*-----------------------------------------------------------------*)
    qed auto
  qed
  ultimately show ?case 
    apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
    apply (unfold IA_def, intro condI, assumption+)
    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
    apply (unfold fam_conj_disj_simp[OF fresh_atm])
    apply (auto simp:sep_conj_ac fam_conj_simps)
    (***************************************************************************)
    (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *)
    (*-------------------------------------------------------------------------*)
    apply (sep_cancel)+
    by (simp add: fam_conj_ext_eq[where I = "s'", OF eq_map])
qed

lemma hoare_dec_fail_gen[step]: 
  assumes "v = 0"
  shows 
  "IA. \<lbrace> pc i ** mm a v \<rbrace>
       i:[ (Dec a e) ]:j   
       \<lbrace> pc e ** mm a v \<rbrace>"
  by (unfold assms, rule hoare_dec_fail)


lemma tm_hoare_dec_suc2:
  assumes "mm a (Suc v) sr"
  shows "\<lbrace> fam_conj sr (recse_map ks) \<and>*
           st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace>
             i:[(Dec a e)]:j
         \<lbrace> fam_conj {M a v} (recse_map (list_ext a ks[a := v])) \<and>*
           st j \<and>*
           ps 2 \<and>*
           zero 0 \<and>*
           zero 1 \<and>*
           reps 2 (ia  - 1) (list_ext a ks[a := v]) \<and>*
           fam_conj {ia  - 1<..} zero\<rbrace>"
proof -
  from `mm a (Suc v) sr` have eq_sr: "sr = {M a (Suc v)}" by (auto simp:mm_def sg_def)
  thus ?thesis
    apply (unfold eq_sr)
    apply (simp add:fam_conj_simps list_ext_get_upd list_ext_len)
    apply (rule tm.pre_condI)
    by (drule tm_hoare_dec_suc1[where u = "2"], simp)
qed

lemma hoare_dec_suc2: 
  "IA. \<lbrace>(pc i \<and>* mm a (Suc v))\<rbrace>  
          i :[ Dec a e ]: j 
       \<lbrace>pc j \<and>* mm a v\<rbrace>"
       (is "IA. \<lbrace> pc i ** ?P \<rbrace> 
                   i:[ ?code ?e]:j   
                \<lbrace> pc ?e ** ?Q\<rbrace>")
proof(induct rule:tm.IHoareI)
  case (IPre s' s r cnf)
  let ?cnf = "(trset_of cnf)"
  from IPre
  have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"
    by (metis condD)+
  from h(1) obtain sr where
      eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"
    by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def)
  hence "At i \<in> s" by auto
  from h(3) obtain s1 s2 s3
    where hh: "?cnf = s1 + s2 + s3"
              "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 
              "IA (s + s') s1" 
              "(i :[ ?code ?e ]: j) s2"
              "r s3"
    apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
    by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)
  interpret ia_disj: IA_disjoint s s' s1 cnf
  proof
    from `IA (s + s') s1` show "IA (s + s') s1" .
  next
    from `s ## s'` show "s ## s'" .
  next
    from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  qed
  from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  from hh(3)
  have "(EXS ks ia.
         ps 2 \<and>*
         zero 0 \<and>*
         zero 1 \<and>*
         reps 2 ia ks \<and>*
         fam_conj {ia<..} zero \<and>*
         (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))
        s1"
    apply (unfold IA_def fam_conj_disj_simp[OF h(2)])
    apply (unfold eq_s)
    by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)
  then obtain ks ia
    where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*
             reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 
    (is "(?PP \<and>* ?QQ) s1")
    by (unfold pred_ex_def, auto simp:sep_conj_ac)
  then obtain ss1 ss2 where pres:
        "s1 = ss1 + ss2" "ss1 ## ss2"
        "?PP ss1"
        "?QQ ss2"
    by (auto elim!:sep_conjE intro!:sep_conjI)
  from ia_disj.at_disj1 [OF `At i \<in> s`]
  have at_fresh_s': "At ?e \<notin>  s'" .
  have at_fresh_sr: "At ?e \<notin> sr"
  proof
    assume at_in: "At ?e \<in> sr"
    from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]
    have "TAt ?e \<in> trset_of cnf"
      apply (elim EXS_elim1)
      apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]
             fam_conj_elm_simp[OF at_in])
      apply (erule_tac sep_conjE, unfold set_ins_def)+
      by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)
    moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 
      apply(erule_tac sep_conjE)
      apply(erule_tac sep_conjE)
      by (auto simp:st_def tpc_set_def sg_def set_ins_def)
    ultimately have "i = ?e"
      by (cases cnf, auto simp:tpn_set_def trset_of.simps)
    from eq_s[unfolded this] at_in
    show "False" by (auto simp:set_ins_def)
  qed
  from pres(3) and hh(2, 4, 5) pres(2, 4)
  have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))
         (trset_of cnf)"
    apply (unfold hh(1) pres(1))
    apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)
    by (auto simp:set_ins_def)
  (*****************************************************************************)
  let ?ks_f = "\<lambda> sr ks. list_ext a ks[a:=v]"
  let ?elm_f = "\<lambda> sr. {M a v}"
  let ?idx_f = "\<lambda> sr ks ia. ia  - 1"
  (*----------------------------------------------------------------------------*)
  (******************************************************************************)
  from tm_hoare_dec_suc2[OF `?P sr`, unfolded tm.Hoare_gen_def, rule_format, OF pres1]
  obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*
        st ?e \<and>*
        ps 2 \<and>*
        zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 
        fam_conj {?idx_f sr ks ia<..} zero) \<and>*
       i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))
       (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast
  (*----------------------------------------------------------------------------*)
  moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"
  proof -
    have "pc ?e {At ?e}" by (simp add:pc_def sg_def)
  (******************************************************************************)
    moreover have "?Q (?elm_f sr)" 
      by (simp add:mm_def sg_def)
  (*----------------------------------------------------------------------------*)
    moreover 
  (******************************************************************************)
    have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)
  (*----------------------------------------------------------------------------*)
    ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)
  qed
  moreover 
  (******************************************************************************)
  from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 
  have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)
  (*----------------------------------------------------------------------------*)
  with at_fresh_s' 
  have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)
  moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 
                           (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
  proof -
    fix elm
    assume elm_in: "elm \<in> s'"
    show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
    proof(cases elm)
      (*******************************************************************)
      case (M a' v')
      from eq_s have "M a (Suc v) \<in> s" by (auto simp:set_ins_def mm_def sg_def)
      with elm_in ia_disj.m_disj1[OF this] M
      have "a \<noteq> a'" by auto
      thus ?thesis
        apply (auto simp:M recse_map.simps pasrt_def list_ext_len)
        apply (case_tac "a < length ks", auto simp:list_ext_len_eq list_ext_lt)
        apply (case_tac "a' < Suc a", auto simp:list_ext_len_eq list_ext_lt)
        by (metis (full_types) bot_nat_def 
              leI le_trans less_Suc_eq_le list_ext_lt_get list_ext_tail set_zero_def)
      (*-----------------------------------------------------------------*)
    qed auto
  qed
  ultimately show ?case 
    apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
    apply (unfold IA_def, intro condI, assumption+)
    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
    apply (unfold fam_conj_disj_simp[OF fresh_atm])
    apply (auto simp:sep_conj_ac fam_conj_simps)
    (***************************************************************************)
    (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *)
    (*-------------------------------------------------------------------------*)
    apply (sep_cancel)+
    by (simp add: fam_conj_ext_eq[where I = "s'", OF eq_map])
qed

lemma hoare_dec_suc2_gen[step]: 
  assumes "v > 0"
  shows 
  "IA. \<lbrace>pc i \<and>* mm a v\<rbrace>  
          i :[ Dec a e ]: j 
       \<lbrace>pc j \<and>* mm a (v - 1)\<rbrace>"
proof -
  from assms obtain v' where "v = Suc v'"
    by (metis gr_implies_not0 nat.exhaust)
  show ?thesis
    apply (unfold `v = Suc v'`, simp)
    by (rule hoare_dec_suc2)
qed

definition "Goto e = jmp e"

lemma hoare_jmp_reps2:
      "\<lbrace> st i \<and>* ps u \<and>* reps u v ks \<and>* tm (v + 1) x \<rbrace>
                 i:[(jmp e)]:j
       \<lbrace> st e \<and>* ps u \<and>* reps u v ks \<and>* tm (v + 1) x \<rbrace>"
proof(cases "ks")
  case Nil
  thus ?thesis
    by (simp add:sep_conj_cond reps.simps, intro tm.pre_condI, simp, hsteps)
next
  case (Cons k ks')
  thus ?thesis
  proof(cases "ks' = []")
    case True with Cons
    show ?thesis
      apply(simp add:sep_conj_cond reps.simps, intro tm.pre_condI, simp add:ones_simps)
      by (hgoto hoare_jmp[where p = u])
  next
    case False
    show ?thesis
      apply (unfold `ks = k#ks'` reps_simp3[OF False], simp add:ones_simps)
      by (hgoto hoare_jmp[where p = u])
  qed
qed

lemma tm_hoare_goto_pre: (* ccc *)
  assumes "(<True>) sr"
  shows "\<lbrace> fam_conj sr (recse_map ks) \<and>*
           st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace>
             i:[(Goto e)]:j
         \<lbrace> fam_conj {} (recse_map ks) \<and>*
           st e \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>* reps 2 ia ks \<and>* fam_conj {ia<..} zero \<rbrace>"
  apply (unfold Goto_def)
  apply (subst (1 2) fam_conj_interv_simp)
  apply (unfold zero_def)
  apply (hstep hoare_jmp_reps2)
  apply (simp add:sep_conj_ac)
  my_block
    from assms have "sr = {}"
      by (simp add:pasrt_def set_ins_def)
  my_block_end
  by (unfold this, sep_cancel+)
  
lemma hoare_goto_pre: 
  "IA. \<lbrace> pc i \<and>* <True> \<rbrace> 
        i:[ (Goto e) ]:j   
       \<lbrace> pc e \<and>* <True> \<rbrace>"
  (is "IA. \<lbrace> pc i ** ?P \<rbrace> 
              i:[ ?code ?e]:j   
           \<lbrace> pc ?e ** ?Q\<rbrace>")
proof(induct rule:tm.IHoareI)
  case (IPre s' s r cnf)
  let ?cnf = "(trset_of cnf)"
  from IPre
  have h: "(pc i \<and>* ?P) s" "(s ## s')" "(IA (s + s') \<and>* i :[ ?code(?e) ]: j \<and>* r) ?cnf"
    by (metis condD)+
  from h(1) obtain sr where
      eq_s: "s = {At i} \<union>  sr" "{At i} ##  sr" "?P sr"
    by (auto dest!:sep_conjD simp:set_ins_def pc_def sg_def pasrt_def)
  hence "At i \<in> s" by auto
  from h(3) obtain s1 s2 s3
    where hh: "?cnf = s1 + s2 + s3"
              "s1 ## s2 \<and> s2 ## s3 \<and> s1 ## s3" 
              "IA (s + s') s1" 
              "(i :[ ?code ?e ]: j) s2"
              "r s3"
    apply (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
    by (metis sep_add_commute sep_disj_addD1 sep_disj_addD2 sep_disj_commuteI)
  interpret ia_disj: IA_disjoint s s' s1 cnf
  proof
    from `IA (s + s') s1` show "IA (s + s') s1" .
  next
    from `s ## s'` show "s ## s'" .
  next
    from hh(1) show "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  qed
  from hh(1) have s1_belong: "s1 \<subseteq> ?cnf" by (auto simp:set_ins_def)
  from hh(3)
  have "(EXS ks ia.
         ps 2 \<and>*
         zero 0 \<and>*
         zero 1 \<and>*
         reps 2 ia ks \<and>*
         fam_conj {ia<..} zero \<and>*
         (st i \<and>* fam_conj sr (recse_map ks)) \<and>* fam_conj s' (recse_map ks))
        s1"
    apply (unfold IA_def fam_conj_disj_simp[OF h(2)])
    apply (unfold eq_s)
    by (insert eq_s(2), simp add: fam_conj_disj_simp[OF eq_s(2)] fam_conj_simps set_ins_def)
  then obtain ks ia
    where "((fam_conj sr (recse_map ks) \<and>* st i \<and>* ps 2 \<and>* zero 0 \<and>* zero 1 \<and>*
             reps 2 ia ks \<and>* fam_conj {ia<..} zero) \<and>* fam_conj s' (recse_map ks)) s1" 
    (is "(?PP \<and>* ?QQ) s1")
    by (unfold pred_ex_def, auto simp:sep_conj_ac)
  then obtain ss1 ss2 where pres:
        "s1 = ss1 + ss2" "ss1 ## ss2"
        "?PP ss1"
        "?QQ ss2"
    by (auto elim!:sep_conjE intro!:sep_conjI)
  from ia_disj.at_disj1 [OF `At i \<in> s`]
  have at_fresh_s': "At ?e \<notin>  s'" .
  have at_fresh_sr: "At ?e \<notin> sr"
  proof
    assume at_in: "At ?e \<in> sr"
    from h(3)[unfolded IA_def fam_conj_disj_simp[OF h(2)]]
    have "TAt ?e \<in> trset_of cnf"
      apply (elim EXS_elim1)
      apply (unfold eq_s fam_conj_disj_simp[OF eq_s(2), unfolded set_ins_def]
             fam_conj_elm_simp[OF at_in])
      apply (erule_tac sep_conjE, unfold set_ins_def)+
      by (auto simp:sep_conj_ac fam_conj_simps st_def sg_def tpn_set_def)
    moreover from pres(1, 3) hh(1) have "TAt i \<in> trset_of cnf" 
      apply(erule_tac sep_conjE)
      apply(erule_tac sep_conjE)
      by (auto simp:st_def tpc_set_def sg_def set_ins_def)
    ultimately have "i = ?e"
      by (cases cnf, auto simp:tpn_set_def trset_of.simps)
    from eq_s[unfolded this] at_in
    show "False" by (auto simp:set_ins_def)
  qed
  from pres(3) and hh(2, 4, 5) pres(2, 4)
  have pres1: "(?PP \<and>* i :[ ?code(?e)]: j \<and>*  (r \<and>* (fam_conj s' (recse_map ks))))
         (trset_of cnf)"
    apply (unfold hh(1) pres(1))
    apply (rule sep_conjI[where x=ss1 and y = "ss2 + s2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s2" and y = "ss2 + s3"], assumption+)
    apply (rule sep_conjI[where x="s3" and y = ss2], assumption+)
    by (auto simp:set_ins_def)
  (*****************************************************************************)
  let ?ks_f = "\<lambda> sr ks. ks"
  let ?elm_f = "\<lambda> sr. {}"
  let ?idx_f = "\<lambda> sr ks ia. ia"
  (*----------------------------------------------------------------------------*)
  (******************************************************************************)
  from tm_hoare_goto_pre[OF `?P sr`, unfolded tm.Hoare_gen_def, rule_format, OF pres1]
  obtain k where "((fam_conj (?elm_f sr) (recse_map (?ks_f sr ks)) \<and>*
        st ?e \<and>*
        ps 2 \<and>*
        zero 0 \<and>* zero 1 \<and>* reps 2 (?idx_f sr ks ia) (?ks_f sr ks) \<and>* 
        fam_conj {?idx_f sr ks ia<..} zero) \<and>*
       i :[ ?code ?e ]: j \<and>* r \<and>* fam_conj s' (recse_map ks))
       (trset_of (sep_exec.run tstep (Suc k) cnf))" by blast
  (*----------------------------------------------------------------------------*)
  moreover have "(pc ?e \<and>* ?Q) ({At ?e} \<union> ?elm_f sr)"
  proof -
    have "pc ?e {At ?e}" by (simp add:pc_def sg_def)
  (******************************************************************************)
    moreover have "?Q (?elm_f sr)" 
     by (simp add:pasrt_def set_ins_def)
  (*----------------------------------------------------------------------------*)
    moreover 
  (******************************************************************************)
    have "{At ?e} ## ?elm_f sr" by (simp add:set_ins_def)
  (*----------------------------------------------------------------------------*)
    ultimately show ?thesis by (auto intro!:sep_conjI simp:set_ins_def)
  qed
  moreover 
  (******************************************************************************)
  from ia_disj.m_disj1 `?P sr` `s = {At i} \<union> sr` 
  have "?elm_f sr ## s'" by (auto simp:set_ins_def mm_def sg_def)
  (*----------------------------------------------------------------------------*)
  with at_fresh_s' 
  have fresh_atm: "{At ?e} \<union> ?elm_f sr ## s'" by (auto simp:set_ins_def)
  moreover have eq_map: "\<And> elm. elm \<in> s' \<Longrightarrow> 
                           (recse_map ks elm) = (recse_map (?ks_f sr ks) elm)"
  proof -
    fix elm
    assume elm_in: "elm \<in> s'"
    show "(recse_map ks elm) = (recse_map (?ks_f sr ks) elm)" 
      by simp
  qed
  ultimately show ?case 
    apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
    apply (unfold IA_def, intro condI, assumption+)
    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
    apply (unfold fam_conj_disj_simp[OF fresh_atm])
    by (auto simp:sep_conj_ac fam_conj_simps)
qed

lemma hoare_goto[step]: "IA. \<lbrace> pc i \<rbrace> 
                          i:[ (Goto e) ]:j   
                       \<lbrace> pc e \<rbrace>"
proof(rule tm.I_hoare_adjust [OF hoare_goto_pre])
  fix s assume "pc i s" thus "(pc i \<and>* <True>) s"
    by (metis cond_true_eq2)
next
  fix s assume "(pc e \<and>* <True>) s" thus "pc e s"
    by (metis cond_true_eq2)
qed

lemma I_hoare_sequence: 
  assumes h1: "\<And> i j. I. \<lbrace>pc i ** p\<rbrace> i:[c1]:j \<lbrace>pc j ** q\<rbrace>"
  and h2: "\<And> j k. I. \<lbrace>pc j ** q\<rbrace> j:[c2]:k \<lbrace>pc k ** r\<rbrace>"
  shows "I. \<lbrace>pc i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>pc k ** r\<rbrace>"
proof(unfold tassemble_to.simps, intro tm.I_code_exI)
  fix j'
  show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k \<and>* r\<rbrace>"
  proof(rule tm.I_sequencing)
    from tm.I_code_extension[OF h1 [of i j'], of" j' :[ c2 ]: k"]
    show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc j' \<and>* q\<rbrace>" .
  next
    from tm.I_code_extension[OF h2 [of j' k], of" i :[ c1 ]: j'"]
    show "I.\<lbrace>pc j' \<and>* q\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k \<and>* r\<rbrace>"
      by (auto simp:sep_conj_ac)
  qed
qed

lemma I_hoare_seq1:
  assumes h1: "\<And>j'. I. \<lbrace>pc i ** p\<rbrace> i:[c1]:j' \<lbrace>pc j' ** q\<rbrace>"
  and h2: "\<And>j' . I. \<lbrace>pc j' ** q\<rbrace> j':[c2]:k \<lbrace>pc k' ** r\<rbrace>"
  shows "I. \<lbrace>pc i ** p\<rbrace> i:[(c1 ; c2)]:k \<lbrace>pc k' ** r\<rbrace>"
proof(unfold tassemble_to.simps, intro tm.I_code_exI)
  fix j'
  show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k' \<and>* r\<rbrace>"
  proof(rule tm.I_sequencing)
    from tm.I_code_extension[OF h1 [of j'], of "j' :[ c2 ]: k "]
    show "I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc j' \<and>* q\<rbrace>" .
  next
    from tm.I_code_extension[OF h2 [of j'], of" i :[ c1 ]: j'"]
    show "I.\<lbrace>pc j' \<and>* q\<rbrace>  i :[ c1 ]: j' \<and>* j' :[ c2 ]: k \<lbrace>pc k' \<and>* r\<rbrace>"
      by (auto simp:sep_conj_ac)
  qed
qed

lemma t_hoare_local1: 
  "(\<And>l. \<lbrace>p\<rbrace>  i :[ c l ]: j \<lbrace>q\<rbrace>) \<Longrightarrow>
    \<lbrace>p\<rbrace> i:[TLocal c]:j \<lbrace>q\<rbrace>"
by (unfold tassemble_to.simps, rule tm.code_exI, auto)

lemma I_hoare_local:
  assumes h: "(\<And>l. I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c l ]: j \<lbrace>pc k \<and>* q\<rbrace>)"
  shows "I. \<lbrace>pc i ** p\<rbrace> i:[TLocal c]:j \<lbrace>pc k ** q\<rbrace>"
proof(unfold tassemble_to.simps, rule tm.I_code_exI)
  fix l
  from h[of l]
  show " I.\<lbrace>pc i \<and>* p\<rbrace>  i :[ c l ]: j \<lbrace>pc k \<and>* q\<rbrace>" .
qed

lemma t_hoare_label1: 
      "(\<And>l. l = i \<Longrightarrow> \<lbrace>p\<rbrace>  l :[ c l ]: j \<lbrace>q\<rbrace>) \<Longrightarrow>
             \<lbrace>p \<rbrace> 
               i:[(TLabel l; c l)]:j
             \<lbrace>q\<rbrace>"
by (unfold tassemble_to.simps, intro tm.code_exI tm.code_condI, clarify, auto)

lemma I_hoare_label: 
  assumes h:"\<And>l. l = i \<Longrightarrow> I. \<lbrace>pc l \<and>* p\<rbrace>  l :[ c l ]: j \<lbrace>pc k \<and>* q\<rbrace>"
  shows "I. \<lbrace>pc i \<and>* p \<rbrace> 
               i:[(TLabel l; c l)]:j
             \<lbrace>pc k \<and>* q\<rbrace>"
proof(unfold tm.IHoare_def, default)
  fix s'
  show " \<lbrace>EXS s. <(pc i \<and>* p) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  i :[ (TLabel l ; c l) ]: j
         \<lbrace>EXS s. <(pc k \<and>* q) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
  proof(rule t_hoare_label1)
    fix l assume "l = i"
    from h[OF this, unfolded tm.IHoare_def]
    show "\<lbrace>EXS s. <(pc i \<and>* p) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  l :[ c l ]: j
          \<lbrace>EXS s. <(pc k \<and>* q) s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>" 
      by (simp add:`l = i`)
  qed
qed

lemma I_hoare_label_last: 
  assumes h1: "t_last_cmd c = Some (TLabel l)"
  and h2: "l = j \<Longrightarrow> I. \<lbrace>p\<rbrace> i:[t_blast_cmd c]:j \<lbrace>q\<rbrace>"
  shows "I. \<lbrace>p\<rbrace> i:[c]:j \<lbrace>q\<rbrace>"
proof(unfold tm.IHoare_def, default)
  fix s'
  show "\<lbrace>EXS s. <p s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  i :[ c ]: j 
        \<lbrace>EXS s. <q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
  proof(rule t_hoare_label_last[OF h1])
    assume "l = j"
    from h2[OF this, unfolded tm.IHoare_def]
    show "\<lbrace>EXS s. <p s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  i :[ t_blast_cmd c ]: j
          \<lbrace>EXS s. <q s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>"
      by fast
  qed
qed

lemma I_hoare_seq2:
 assumes h: "\<And>j'. I. \<lbrace>pc i ** p\<rbrace> i:[c1]:j' \<lbrace>pc k' \<and>* r\<rbrace>"
 shows "I. \<lbrace>pc i ** p\<rbrace> i:[(c1 ; c2)]:j \<lbrace>pc k' ** r\<rbrace>"
  apply (unfold tassemble_to.simps, intro tm.I_code_exI)
  apply (unfold tm.IHoare_def, default)
  apply (rule tm.code_extension)
  by (rule h[unfolded tm.IHoare_def, rule_format])

lemma IA_pre_stren:
  assumes h1: "IA. \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
  and h2:  "\<And>s. r s \<Longrightarrow> p s"
  shows "IA. \<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"
  by (rule tm.I_pre_stren[OF assms], simp)

lemma IA_post_weaken: 
  assumes h1: "IA. \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
    and h2: "\<And> s. q s \<Longrightarrow> r s"
  shows "IA. \<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
  by (rule tm.I_post_weaken[OF assms], simp)

section {* Making triple processor for IA *}

ML {* (* Functions specific to Hoare triple: IA {P} c {Q} *)
  fun get_pre ctxt t = 
    let val pat = term_of @{cpat "IA. \<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} 
        val env = match ctxt pat t 
    in inst env (term_of @{cpat "?P::aresource set \<Rightarrow> bool"}) end

  fun can_process ctxt t = ((get_pre ctxt t; true) handle _ => false)

  fun get_post ctxt t = 
    let val pat = term_of @{cpat "IA. \<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} 
        val env = match ctxt pat t 
    in inst env (term_of @{cpat "?Q::aresource set \<Rightarrow> bool"}) end;

  fun get_mid ctxt t = 
    let val pat = term_of @{cpat "IA. \<lbrace>?P\<rbrace> ?c \<lbrace>?Q\<rbrace>"} 
        val env = match ctxt pat t 
    in inst env (term_of @{cpat "?c::tresource set \<Rightarrow> bool"}) end;

  fun is_pc_term (Const (@{const_name pc}, _) $ _) = true
    | is_pc_term _ = false

  fun mk_pc_term x =
     Const (@{const_name pc}, @{typ "nat \<Rightarrow> aresource set \<Rightarrow> bool"}) $ Free (x, @{typ "nat"})

  val sconj_term = term_of @{cterm "sep_conj::assert \<Rightarrow> assert \<Rightarrow> assert"}

  val abc_triple = {binding = @{binding "abc_triple"}, 
                   can_process = can_process,
                   get_pre = get_pre,
                   get_mid = get_mid,
                   get_post = get_post,
                   is_pc_term = is_pc_term,
                   mk_pc_term = mk_pc_term,
                   sconj_term = sconj_term,
                   sep_conj_ac_tac = sep_conj_ac_tac,
                   hoare_seq1 = @{thm I_hoare_seq1},
                   hoare_seq2 = @{thm I_hoare_seq2},
                   pre_stren = @{thm IA_pre_stren},
                   post_weaken = @{thm IA_post_weaken},
                   frame_rule = @{thm tm.I_frame_rule}
                  }:HoareTriple

  val _ = (HoareTriples_get ()) |> (fn orig => HoareTriples_store (abc_triple::orig))
*}

section {* Example proofs *}

definition "clear a = (TL start exit. TLabel start; Dec a exit; Goto start; TLabel exit)"

lemma hoare_clear[step]: 
  "IA. \<lbrace>pc i ** mm a v\<rbrace> 
         i:[clear a]:j 
       \<lbrace>pc j ** mm a 0\<rbrace>"
proof(unfold clear_def, intro I_hoare_local I_hoare_label, simp,
      rule I_hoare_label_last, simp+, prune)
  show "IA.\<lbrace>pc i \<and>* mm a v\<rbrace>  i :[ (Dec a j ; Goto i) ]: j \<lbrace>pc j \<and>* mm a 0\<rbrace>"
  proof(induct v)
    case 0
    show ?case
      by hgoto
  next
    case (Suc v)
    show ?case
      apply (rule_tac Q = "pc i \<and>* mm a v" in tm.I_sequencing)
      by hsteps
  qed
qed

definition "dup a b c = 
       (TL start exit. TLabel start; Dec a exit; Inc b; Inc c; Goto start; TLabel exit)"

lemma hoare_dup[step]: 
        "IA. \<lbrace>pc i ** mm a va ** mm b vb ** mm c vc \<rbrace> 
                  i:[dup a b c]:j 
             \<lbrace>pc j ** mm a 0 ** mm b (va + vb) ** mm c (va + vc)\<rbrace>"
proof(unfold dup_def, intro I_hoare_local I_hoare_label, clarsimp,
     rule I_hoare_label_last, simp+, prune)
  show "IA. \<lbrace>pc i \<and>* mm a va \<and>* mm b vb \<and>* mm c vc\<rbrace>  
               i :[ (Dec a j ; Inc b ; Inc c ; Goto i) ]: j
            \<lbrace>pc j \<and>* mm a 0 \<and>* mm b (va + vb) \<and>* mm c (va + vc)\<rbrace>"
  proof(induct va arbitrary: vb vc)
    case (0 vb vc)
    show ?case
      by hgoto
  next
    case (Suc va vb vc)
    show ?case
      apply (rule_tac Q = "pc i \<and>* mm a va \<and>* mm b (Suc vb) \<and>* mm c (Suc vc)" in tm.I_sequencing)
      by (hsteps Suc)
  qed
qed

definition "clear_add a b = 
               (TL start exit. TLabel start; Dec a exit; Inc b; Goto start; TLabel exit)"

lemma hoare_clear_add[step]: 
                 "IA. \<lbrace>pc i ** mm a va ** mm b vb \<rbrace> 
                          i:[clear_add a b]:j 
                      \<lbrace>pc j ** mm a 0 ** mm b (va + vb)\<rbrace>"
proof(unfold clear_add_def, intro I_hoare_local I_hoare_label, clarsimp,
      rule I_hoare_label_last, simp+, prune)
  show "IA. \<lbrace>pc i \<and>* mm a va \<and>* mm b vb\<rbrace>  
               i :[ (Dec a j ; Inc b ; Goto i) ]: j 
            \<lbrace>pc j \<and>* mm a 0 \<and>* mm b (va + vb)\<rbrace>"
  proof(induct va arbitrary: vb)
    case 0
    show ?case
      by hgoto
  next
    case (Suc va vb)
    show ?case
      apply (rule_tac Q = "pc i \<and>* mm a va \<and>* mm b (Suc vb)" in tm.I_sequencing)
      by (hsteps Suc)
  qed
qed

definition "copy_to a b c = clear b; clear c; dup a b c; clear_add c a"

lemma hoare_copy_to[step]: 
    "IA. \<lbrace>pc i ** mm a va ** mm b vb ** mm c vc \<rbrace> 
               i:[copy_to a b c]:j 
         \<lbrace>pc j ** mm a va ** mm b va ** mm c 0\<rbrace>"
  by (unfold copy_to_def, hsteps)

definition "preserve_add a b c = clear c; dup a b c; clear_add c a"

lemma hoare_preserve_add[step]: 
    "IA. \<lbrace>pc i ** mm a va ** mm b vb ** mm c vc \<rbrace> 
              i:[preserve_add a b c]:j 
         \<lbrace>pc j ** mm a va ** mm b (va + vb) ** mm c 0\<rbrace>"
  by (unfold preserve_add_def, hsteps)

definition "mult a b c t1 t2 = 
                clear c;
                copy_to a t2 t1; 
                (TL start exit. 
                    TLabel start;
                    Dec a exit;
                    preserve_add b c t1;
                    Goto start;
                    TLabel exit
                );
                clear_add t2 a"

lemma hoare_mult[step]: 
    "IA. \<lbrace>pc i ** mm a va ** mm b vb ** mm c vc ** mm t1 vt1 ** mm t2 vt2 \<rbrace> 
                         i:[mult a b c t1 t2]:j 
         \<lbrace>pc j ** mm a va ** mm b vb ** mm c (va * vb) ** mm t1 0 ** mm t2 0 \<rbrace>"
  apply (unfold mult_def, hsteps)
  apply (rule_tac q = "mm a 0 \<and>* mm b vb \<and>* mm c (va * vb) \<and>* mm t1 0 \<and>* mm t2 va" in I_hoare_seq1)
  apply (intro I_hoare_local I_hoare_label, clarify,
      rule I_hoare_label_last, simp+, clarify, prune)
  my_block
  fix i j vc
    have "IA. \<lbrace>pc i \<and>* mm a va \<and>* mm t1 0 \<and>* mm c vc \<and>* mm b vb\<rbrace> 
               i :[ (Dec a j ; preserve_add b c t1 ; Goto i) ]: j
              \<lbrace>pc j \<and>* mm a 0 \<and>* mm b vb \<and>* mm c (va * vb + vc) \<and>* mm t1 0 \<rbrace>"
    proof(induct va arbitrary:vc)
      case (0 vc)
      show ?case
        by hgoto
    next
      case (Suc va vc)
      show ?case
        apply (rule_tac Q = "pc i \<and>* mm a va \<and>* mm t1 0 \<and>* mm c (vb + vc) \<and>* mm b vb"
                in tm.I_sequencing)
        apply (hsteps Suc)
        by (sep_cancel+, simp, smt)
    qed
  my_block_end
  by (hsteps this)

end
author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Fri, 21 Mar 2014 15:10:13 +0000 (2014-03-21)
changeset 7	192672a6fff4
parent 0	1378b654acde
child 11	f8b2bf858caf
permissions	-rw-r--r--