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