--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Hoare_abc2.thy Thu Apr 03 15:28:01 2014 +0100
@@ -0,0 +1,1217 @@
+header {*
+ {\em Abacus} defined as macros of TM
+ *}
+
+theory Hoare_abc2
+imports Hoare_tm2 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 tm.pred_exI)
+ apply (rule_tac x = "?idx_f sr ks ia" in tm.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 tm.pred_exI)
+ apply (rule_tac x = "?idx_f sr ks ia" in tm.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 tm.pred_exI)
+ apply (rule_tac x = "?idx_f sr ks ia" in tm.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 tm.pred_exI)
+ apply (rule_tac x = "?idx_f sr ks ia" in tm.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
+
--- a/thys/Hoare_tm2.thy Thu Apr 03 14:02:58 2014 +0100
+++ b/thys/Hoare_tm2.thy Thu Apr 03 15:28:01 2014 +0100
@@ -2,7 +2,7 @@
Separation logic for Turing Machines
*}
-theory Hoare_tm
+theory Hoare_tm2
imports Hoare_gen
My_block
Data_slot
@@ -126,7 +126,6 @@
interpretation tm: sep_exec tstep trset_of .
-
section {* Assembly language for TMs and its program logic *}
subsection {* The assembly language *}
@@ -411,17 +410,16 @@
proof -
assume "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))"
thus ?thesis
- apply(unfold sep_conj_def set_ins_def sg_def trset_of.simps tpn_set_def)
-
+ apply(unfold sep_conj_def set_ins_def sg_def trset_of.simps tpn_set_def)
by auto
qed
-lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem)) \<Longrightarrow> mem a = Some v"
+lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem)) \<Longrightarrow> mem $ a = Some v"
proof -
assume "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))"
from stimes_sgD[OF this[unfolded trset_of.simps tpn_set_def tm_def]]
- have "{TM a v} \<subseteq> {TC i inst |i inst. prog i = Some inst} \<union> {TAt i} \<union>
- {TPos pos} \<union> {TM i n |i n. mem i = Some n} \<union> {TFaults ft}" by simp
+ have "{TM a v} \<subseteq> {TC i inst |i inst. prog $ i = Some inst} \<union> {TAt i} \<union>
+ {TPos pos} \<union> {TM i n |i n. mem $ i = Some n} \<union> {TFaults ft}" by simp
thus ?thesis by auto
qed
@@ -1214,15 +1212,20 @@
lemma tmem_set_upd:
"{TM a v} \<subseteq> tmem_set mem \<Longrightarrow>
- tmem_set (mem(a:=Some v')) = ((tmem_set mem) - {TM a v}) \<union> {TM a v'}"
- by (unfold tpn_set_def, auto)
+ tmem_set (mem(a $:=Some v')) = ((tmem_set mem) - {TM a v}) \<union> {TM a v'}"
+apply(unfold tpn_set_def)
+apply(auto)
+apply (metis finfun_upd_apply option.inject)
+apply (metis finfun_upd_apply_other)
+by (metis finfun_upd_apply_other option.inject)
+
lemma tmem_set_disj: "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow>
{TM a v'} \<inter> (tmem_set mem - {TM a v}) = {}"
by (unfold tpn_set_def, auto)
lemma smem_upd: "((tm a v) ** r) (trset_of (f, x, y, z, mem)) \<Longrightarrow>
- ((tm a v') ** r) (trset_of (f, x, y, z, mem(a := Some v')))"
+ ((tm a v') ** r) (trset_of (f, x, y, z, mem(a $:= Some v')))"
proof -
have eq_s: "(tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f - {TM a v}) =
(tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)"
@@ -1235,11 +1238,11 @@
from h TM_in_simp have "{TM a v} \<subseteq> tmem_set mem"
by(sep_drule stimes_sgD, auto)
from tmem_set_upd [OF this] tmem_set_disj[OF this]
- have h2: "tmem_set (mem(a \<mapsto> v')) = {TM a v'} \<union> (tmem_set mem - {TM a v})"
+ have h2: "tmem_set (mem(a $:= Some v')) = {TM a v'} \<union> (tmem_set mem - {TM a v})"
"{TM a v'} \<inter> (tmem_set mem - {TM a v}) = {}" by auto
show ?thesis
proof -
- have "(tm a v' ** r) (tmem_set (mem(a \<mapsto> v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f)"
+ have "(tm a v' ** r) (tmem_set (mem(a $:= Some v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f)"
proof(rule sep_conjI)
show "tm a v' ({TM a v'})" by (unfold tm_def sg_def, simp)
next
@@ -1247,13 +1250,13 @@
next
show "{TM a v'} ## tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f"
proof -
- from g have " mem a = Some v"
+ from g have " mem $ a = Some v"
by(sep_frule memD, simp)
thus "?thesis"
by(unfold tpn_set_def set_ins_def, auto)
qed
next
- show "tmem_set (mem(a \<mapsto> v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f =
+ show "tmem_set (mem(a $:= Some v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f =
{TM a v'} + (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)"
by (unfold h2(1) set_ins_def eq_s, auto)
qed
@@ -1278,11 +1281,11 @@
fix ft prog cs i' mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* sg {TC i ((W0, j), W0, j)})
(trset_of (ft, prog, cs, i', mem))"
- from h have "prog i = Some ((W0, j), W0, j)"
+ from h have "prog $ i = Some ((W0, j), W0, j)"
apply(rule_tac r = "r \<and>* ps p \<and>* tm p v" in codeD)
by(simp add: sep_conj_ac)
from h and this have stp:
- "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, j, i', mem(i'\<mapsto> Bk))" (is "?x = ?y")
+ "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, j, i', mem(i' $:= Some Bk))" (is "?x = ?y")
apply(sep_frule psD)
apply(sep_frule stD)
apply(sep_frule memD, simp)
@@ -1328,12 +1331,12 @@
fix ft prog cs i' mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* sg {TC i ((W1, ?j), W1, ?j)})
(trset_of (ft, prog, cs, i', mem))"
- from h have "prog i = Some ((W1, ?j), W1, ?j)"
+ from h have "prog $ i = Some ((W1, ?j), W1, ?j)"
apply(rule_tac r = "r \<and>* ps p \<and>* tm p v" in codeD)
by(simp add: sep_conj_ac)
from h and this have stp:
"tm.run 1 (ft, prog, cs, i', mem) =
- (ft, prog, ?j, i', mem(i'\<mapsto> Oc))" (is "?x = ?y")
+ (ft, prog, ?j, i', mem(i' $:= Some Oc))" (is "?x = ?y")
apply(sep_frule psD)
apply(sep_frule stD)
apply(sep_frule memD, simp)
@@ -1380,7 +1383,7 @@
fix ft prog cs i' mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v2 \<and>* sg {TC i ((L, ?j), L, ?j)})
(trset_of (ft, prog, cs, i', mem))"
- from h have "prog i = Some ((L, ?j), L, ?j)"
+ from h have "prog $ i = Some ((L, ?j), L, ?j)"
apply(rule_tac r = "r \<and>* ps p \<and>* tm p v2" in codeD)
by(simp add: sep_conj_ac)
from h and this have stp:
@@ -1438,7 +1441,7 @@
fix ft prog cs i' mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v1 \<and>* sg {TC i ((R, ?j), R, ?j)})
(trset_of (ft, prog, cs, i', mem))"
- from h have "prog i = Some ((R, ?j), R, ?j)"
+ from h have "prog $ i = Some ((R, ?j), R, ?j)"
apply(rule_tac r = "r \<and>* ps p \<and>* tm p v1" in codeD)
by(simp add: sep_conj_ac)
from h and this have stp:
@@ -1494,18 +1497,21 @@
fix ft prog cs pc mem r
assume h: "(r \<and>* one p \<and>* ps p \<and>* st i \<and>* sg {TC i ((W0, ?j), W1, e)})
(trset_of (ft, prog, cs, pc, mem))"
- from h have k1: "prog i = Some ((W0, ?j), W1, e)"
+ from h have k1: "prog $ i = Some ((W0, ?j), W1, e)"
apply(rule_tac r = "r \<and>* one p \<and>* ps p" in codeD)
by(simp add: sep_conj_ac)
from h have k2: "pc = p"
by(sep_drule psD, simp)
- from h and this have k3: "mem pc = Some Oc"
+ from h and this have k3: "mem $ pc = Some Oc"
apply(unfold one_def)
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
"tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, e, pc, mem)" (is "?x = ?y")
apply(sep_drule stD)
- by(unfold tm.run_def, auto)
+ apply(unfold tm.run_def)
+ apply(auto)
+ by (metis finfun_upd_triv)
+
from h k2
have "(r \<and>* one p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of ?x)"
apply(unfold stp)
@@ -1578,18 +1584,20 @@
fix ft prog cs pc mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* sg {TC i ((W0, ?j), W1, e)})
(trset_of (ft, prog, cs, pc, mem))"
- from h have k1: "prog i = Some ((W0, ?j), W1, e)"
+ from h have k1: "prog $ i = Some ((W0, ?j), W1, e)"
apply(rule_tac r = "r \<and>* zero p \<and>* ps p" in codeD)
by(simp add: sep_conj_ac)
from h have k2: "pc = p"
by(sep_drule psD, simp)
- from h and this have k3: "mem pc = Some Bk"
+ from h and this have k3: "mem $ pc = Some Bk"
apply(unfold zero_def)
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
"tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, ?j, pc, mem)" (is "?x = ?y")
apply(sep_drule stD)
- by(unfold tm.run_def, auto)
+ apply(unfold tm.run_def)
+ apply(auto)
+ by (metis finfun_upd_triv)
from h k2
have "(r \<and>* zero p \<and>* ps p \<and>* st ?j \<and>* sg {TC i ((W0, ?j), W1, e)}) (trset_of ?x)"
apply (unfold stp)
@@ -1625,18 +1633,20 @@
fix ft prog cs pc mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* sg {TC i ((W0, e), W1, ?j)})
(trset_of (ft, prog, cs, pc, mem))"
- from h have k1: "prog i = Some ((W0, e), W1, ?j)"
+ from h have k1: "prog $ i = Some ((W0, e), W1, ?j)"
apply(rule_tac r = "r \<and>* zero p \<and>* ps p" in codeD)
by(simp add: sep_conj_ac)
from h have k2: "pc = p"
by(sep_drule psD, simp)
- from h and this have k3: "mem pc = Some Bk"
+ from h and this have k3: "mem $ pc = Some Bk"
apply(unfold zero_def)
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
"tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, e, pc, mem)" (is "?x = ?y")
apply(sep_drule stD)
- by(unfold tm.run_def, auto)
+ apply(unfold tm.run_def)
+ apply(auto)
+ by (metis finfun_upd_triv)
from h k2
have "(r \<and>* zero p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of ?x)"
apply(unfold stp)
@@ -1702,17 +1712,19 @@
fix ft prog cs pc mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p Oc \<and>* sg {TC i ((W0, e), W1, ?j)})
(trset_of (ft, prog, cs, pc, mem))"
- from h have k1: "prog i = Some ((W0, e), W1, ?j)"
+ from h have k1: "prog $ i = Some ((W0, e), W1, ?j)"
apply(rule_tac r = "r \<and>* tm p Oc \<and>* ps p" in codeD)
by(simp add: sep_conj_ac)
from h have k2: "pc = p"
by(sep_drule psD, simp)
- from h and this have k3: "mem pc = Some Oc"
+ from h and this have k3: "mem $ pc = Some Oc"
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
"tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, ?j, pc, mem)" (is "?x = ?y")
apply(sep_drule stD)
- by(unfold tm.run_def, auto)
+ apply(unfold tm.run_def)
+ apply(auto)
+ by (metis finfun_upd_triv)
from h k2
have "(r \<and>* tm p Oc \<and>* ps p \<and>* st ?j \<and>* sg {TC i ((W0, e), W1, ?j)}) (trset_of ?x)"
apply(unfold stp)
@@ -1741,17 +1753,23 @@
fix ft prog cs pos mem r
assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* <(j = i + 1)> \<and>* sg {TC i ((W0, e), W1, e)})
(trset_of (ft, prog, cs, pos, mem))"
- from h have k1: "prog i = Some ((W0, e), W1, e)"
+ from h have k1: "prog $ i = Some ((W0, e), W1, e)"
apply(rule_tac r = "r \<and>* <(j = i + 1)> \<and>* tm p v \<and>* ps p" in codeD)
by(simp add: sep_conj_ac)
from h have k2: "p = pos"
by(sep_drule psD, simp)
- from h k2 have k3: "mem pos = Some v"
+ from h k2 have k3: "mem $ pos = Some v"
by(sep_drule memD, simp)
from h k1 k2 k3 have
stp: "tm.run 1 (ft, prog, cs, pos, mem) = (ft, prog, e, pos, mem)" (is "?x = ?y")
apply(sep_drule stD)
- by(unfold tm.run_def, cases "mem pos", simp, cases v, auto)
+ apply(unfold tm.run_def)
+ apply(cases "mem $ pos")
+ apply(simp)
+ apply(cases v)
+ apply(auto)
+ apply (metis finfun_upd_triv)
+ by (metis finfun_upd_triv)
from h k2
have "(r \<and>* ps p \<and>* st e \<and>* tm p v \<and>* <(j = i + 1)> \<and>*
sg {TC i ((W0, e), W1, e)}) (trset_of ?x)"
@@ -4213,7 +4231,7 @@
by (smt cond_eqI cond_true_eq sep_conj_commute sep_conj_empty)
lemma sep_conj_cond4 : "(<cond1> \<and>* <cond2> \<and>* r) = (<(cond1 \<and> cond2)> \<and>* r)"
- by (metis Hoare_gen.sep_conj_cond3 Hoare_tm.sep_conj_cond3)
+by (metis Hoare_tm2.sep_conj_cond3 sep_conj_assoc)
lemmas sep_conj_cond = sep_conj_cond3 sep_conj_cond4 sep_conj_cond