diff -r 000000000000 -r 1378b654acde thys/Hoare_abc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Hoare_abc.thy	Thu Mar 06 13:28:38 2014 +0000
@@ -0,0 +1,1217 @@
+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
+