header {* + −
{\em abacus} a kind of register machine+ −
*}+ −
+ −
theory abacus+ −
imports Main StateMonad+ −
begin+ −
+ −
text {*+ −
{\em Abacus} instructions:+ −
*}+ −
+ −
datatype abc_inst =+ −
-- {* @{text "Inc n"} increments the memory cell (or register) + −
with address @{text "n"} by one.+ −
*}+ −
Inc nat+ −
-- {*+ −
@{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. + −
If cell @{text "n"} is already zero, no decrements happens and the executio jumps to+ −
the instruction labeled by @{text "label"}.+ −
*}+ −
| Dec nat nat+ −
-- {*+ −
@{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.+ −
*}+ −
| Goto nat+ −
+ −
+ −
fun splits :: "'a set \<Rightarrow> ('a set \<times> 'a set) \<Rightarrow> bool"+ −
where "splits s (u, v) = (u \<union> v = s \<and> u \<inter> v = {})"+ −
+ −
declare splits.simps [simp del]+ −
+ −
definition "stimes p q = {s . \<exists> u v. u \<in> p \<and> v \<in> q \<and> splits s (u, v)}"+ −
lemmas st_def = stimes_def[unfolded splits.simps]+ −
+ −
notation stimes (infixr "*" 70)+ −
+ −
lemma stimes_comm: "(p::('a set set)) * q = q * p"+ −
by (unfold st_def, auto)+ −
+ −
lemma splits_simp: "splits s (u, v) = (v = (s - u) \<and> v \<subseteq> s \<and> u \<subseteq> s)"+ −
by (unfold splits.simps, auto)+ −
+ −
lemma stimes_assoc: "p * q * r = (p * q) * (r::'a set set)"+ −
by (unfold st_def, blast)+ −
+ −
definition+ −
"emp = {{}}"+ −
+ −
lemma emp_unit_r [simp]: "p * emp = p"+ −
by (unfold st_def emp_def, auto)+ −
+ −
lemma emp_unit_l [simp]: "emp * p = p"+ −
by (metis emp_unit_r stimes_comm)+ −
+ −
lemma stimes_mono: "p \<subseteq> q \<Longrightarrow> p * r \<subseteq> q * r"+ −
by (unfold st_def, auto)+ −
+ −
lemma stimes_left_commute:+ −
"(q * (p * r)) = ((p::'a set set) * (q * r))"+ −
by (metis stimes_assoc stimes_comm)+ −
+ −
lemmas stimes_ac = stimes_comm stimes_assoc stimes_left_commute+ −
+ −
lemma "x * y * z = z * y * (x::'a set set)"+ −
by (metis stimes_ac)+ −
+ −
+ −
definition pasrt :: "bool \<Rightarrow> ('a set set)" ("<_>" [71] 71)+ −
where "pasrt b = {s . s = {} \<and> b}"+ −
+ −
datatype apg = + −
Instr abc_inst+ −
| Label nat+ −
| Seq apg apg+ −
| Local "(nat \<Rightarrow> apg)"+ −
+ −
abbreviation prog_instr :: "abc_inst \<Rightarrow> apg" ("\<guillemotright>_" [61] 61)+ −
where "\<guillemotright>i \<equiv> Instr i"+ −
+ −
abbreviation prog_seq :: "apg \<Rightarrow> apg \<Rightarrow> apg" (infixr ";" 52)+ −
where "c1 ; c2 \<equiv> Seq c1 c2"+ −
+ −
type_synonym aconf = "((nat \<rightharpoonup> abc_inst) \<times> nat \<times> (nat \<rightharpoonup> nat) \<times> nat)"+ −
+ −
fun astep :: "aconf \<Rightarrow> aconf"+ −
where "astep (prog, pc, m, faults) = + −
(case (prog pc) of+ −
Some (Inc i) \<Rightarrow> + −
case m(i) of+ −
Some n \<Rightarrow> (prog, pc + 1, m(i:= Some (n + 1)), faults)+ −
| None \<Rightarrow> (prog, pc, m, faults + 1)+ −
| Some (Dec i e) \<Rightarrow> + −
case m(i) of+ −
Some n \<Rightarrow> if (n = 0) then (prog, e, m, faults)+ −
else (prog, pc + 1, m(i:= Some (n - 1)), faults)+ −
| None \<Rightarrow> (prog, pc, m, faults + 1)+ −
| Some (Goto pc') \<Rightarrow> (prog, pc', m, faults)+ −
| None \<Rightarrow> (prog, pc, m, faults + 1))"+ −
+ −
definition "run n = astep ^^ n"+ −
+ −
datatype aresource = + −
M nat nat+ −
| C nat abc_inst+ −
| At nat+ −
| Faults nat+ −
+ −
definition "prog_set prog = {C i inst | i inst. prog i = Some inst}"+ −
definition "pc_set pc = {At pc}"+ −
definition "mem_set m = {M i n | i n. m (i) = Some n} "+ −
definition "faults_set faults = {Faults faults}"+ −
+ −
lemmas cpn_set_def = prog_set_def pc_set_def mem_set_def faults_set_def+ −
+ −
fun rset_of :: "aconf \<Rightarrow> aresource set"+ −
where "rset_of (prog, pc, m, faults) = + −
prog_set prog \<union> pc_set pc \<union> mem_set m \<union> faults_set faults"+ −
+ −
definition "pc l = {pc_set l}"+ −
+ −
+ −
definition "m a v = {{M a v}}"+ −
+ −
+ −
declare rset_of.simps[simp del]+ −
+ −
type_synonym assert = "aresource set set"+ −
+ −
primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" + −
where + −
"assemble_to (Instr ai) i j = ({{C i ai}} * <(j = i + 1)>)" |+ −
"assemble_to (Seq p1 p2) i j = (\<Union> j'. (assemble_to p1 i j') * (assemble_to p2 j' j))" |+ −
"assemble_to (Local fp) i j = (\<Union> l. (assemble_to (fp l) i j))" |+ −
"assemble_to (Label l) i j = <(i = j \<and> j = l)>"+ −
+ −
abbreviation asmb_to :: "nat \<Rightarrow> apg \<Rightarrow> nat \<Rightarrow> assert" ("_ :[ _ ]: _" [60, 60, 60] 60)+ −
where "i :[ apg ]: j \<equiv> assemble_to apg i j"+ −
+ −
lemma stimes_sgD: "s \<in> {x} * q \<Longrightarrow> (s - x) \<in> q \<and> x \<subseteq> s"+ −
apply (unfold st_def, auto)+ −
by (smt Diff_disjoint Un_Diff_cancel2 Un_Int_distrib + −
Un_commute Un_empty_right Un_left_absorb)+ −
+ −
lemma pcD: "rset_of (prog, i', mem, fault) \<in> pc i * r+ −
\<Longrightarrow> i' = i"+ −
proof -+ −
assume "rset_of (prog, i', mem, fault) \<in> pc i * r"+ −
from stimes_sgD [OF this[unfolded pc_def], unfolded rset_of.simps]+ −
have "pc_set i \<subseteq> prog_set prog \<union> pc_set i' \<union> mem_set mem \<union> faults_set fault" by auto+ −
thus ?thesis + −
by (unfold cpn_set_def, auto)+ −
qed+ −
+ −
lemma codeD: "rset_of (prog, pos, mem, fault) \<in> pc i * {{C i inst}} * r+ −
\<Longrightarrow> prog pos = Some inst"+ −
proof -+ −
assume h: "rset_of (prog, pos, mem, fault) \<in> pc i * {{C i inst}} * r" (is "?c \<in> ?X")+ −
from pcD[OF this] have "i = pos" by simp+ −
with h show ?thesis+ −
by (unfold rset_of.simps st_def pc_def prog_set_def + −
pc_set_def mem_set_def faults_set_def, auto)+ −
qed+ −
+ −
lemma memD: "rset_of (prog, pos, mem, fault) \<in> (m a v) * r \<Longrightarrow> mem a = Some v"+ −
proof -+ −
assume "rset_of (prog, pos, mem, fault) \<in> (m a v) * r"+ −
from stimes_sgD[OF this[unfolded rset_of.simps cpn_set_def m_def]]+ −
have "{M a v} \<subseteq> {C i inst |i inst. prog i = Some inst} \<union> + −
{At pos} \<union> {M i n |i n. mem i = Some n} \<union> {Faults fault}" by auto+ −
thus ?thesis by auto+ −
qed+ −
+ −
definition+ −
Hoare_abc :: "assert \<Rightarrow> assert \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)+ −
where+ −
"{p} c {q} \<equiv> (\<forall> s r. (rset_of s) \<in> (p*c*r) \<longrightarrow>+ −
(\<exists> k. ((rset_of (run k s)) \<in> (q*c*r))))" + −
+ −
definition "dec_fun v j e = (if (v = 0) then (e, v) else (j, v - 1))"+ −
+ −
lemma disj_Diff: "a \<inter> b = {} \<Longrightarrow> a \<union> b - b = a"+ −
by (metis (lifting) Diff_cancel Un_Diff Un_Diff_Int)+ −
+ −
lemma diff_pc_set: "prog_set aa \<union> pc_set i \<union> mem_set ab \<union> faults_set b - pc_set i = + −
prog_set aa \<union> mem_set ab \<union> faults_set b" (is "?L = ?R")+ −
proof -+ −
have "?L = (prog_set aa \<union> mem_set ab \<union> faults_set b \<union> pc_set i) - pc_set i"+ −
by auto+ −
also have "\<dots> = ?R"+ −
proof(rule disj_Diff)+ −
show " (prog_set aa \<union> mem_set ab \<union> faults_set b) \<inter> pc_set i = {}"+ −
by (unfold cpn_set_def, auto)+ −
qed+ −
finally show ?thesis .+ −
qed+ −
+ −
lemma M_in_simp: "({M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f) = + −
({M a v} \<subseteq> mem_set mem)"+ −
by (unfold cpn_set_def, auto)+ −
+ −
lemma mem_set_upd: + −
"{M a v} \<subseteq> mem_set mem \<Longrightarrow> mem_set (mem(a:=Some v')) = ((mem_set mem) - {M a v}) \<union> {M a v'}"+ −
by (unfold cpn_set_def, auto)+ −
+ −
lemma mem_set_disj: "{M a v} \<subseteq> mem_set mem \<Longrightarrow> {M a v'} \<inter> (mem_set mem - {M a v}) = {}"+ −
by (unfold cpn_set_def, auto)+ −
+ −
lemma stimesE:+ −
assumes h: "s \<in> x * y"+ −
obtains s1 s2 where "s = s1 \<union> s2" and "s1 \<inter> s2 = {}" and "s1 \<in> x" and "s2 \<in> y"+ −
by (insert h, auto simp:st_def)+ −
+ −
lemma stimesI: + −
"\<lbrakk>s = s1 \<union> s2; s1 \<inter> s2 = {}; s1 \<in> x; s2 \<in> y\<rbrakk> \<Longrightarrow> s \<in> x * y"+ −
by (auto simp:st_def)+ −
+ −
lemma smem_upd: "(rset_of (x, y, mem, f)) \<in> (m a v)*r \<Longrightarrow> + −
(rset_of (x, y, mem(a := Some v'), f) \<in> (m a v')*r)"+ −
proof -+ −
assume h: " rset_of (x, y, mem, f) \<in> m a v * r"+ −
from h[unfolded rset_of.simps m_def]+ −
have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f \<in> {{M a v}} * r" .+ −
from stimes_sgD [OF this]+ −
have h1: "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} \<in> r"+ −
"{M a v} \<subseteq> prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f" by auto+ −
moreover have "prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f - {M a v} = + −
prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f"+ −
by (unfold cpn_set_def, auto)+ −
ultimately have h0: "prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f \<in> r" + −
by simp+ −
from h1(2) and M_in_simp have "{M a v} \<subseteq> mem_set mem" by simp+ −
from mem_set_upd [OF this] mem_set_disj[OF this]+ −
have h2: "mem_set (mem(a \<mapsto> v')) = {M a v'} \<union> (mem_set mem - {M a v})" + −
"{M a v'} \<inter> (mem_set mem - {M a v}) = {}" by auto+ −
show ?thesis+ −
proof -+ −
have "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r"+ −
proof(rule stimesI[OF _ _ _ h0])+ −
show "{M a v'} \<in> m a v'" by (unfold m_def, auto)+ −
next+ −
show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f =+ −
{M a v'} \<union> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)"+ −
apply (unfold h2(1))+ −
by (smt Un_commute Un_insert_left Un_insert_right + −
Un_left_commute + −
`prog_set x \<union> pc_set y \<union> mem_set mem \<union> + −
faults_set f - {M a v} =prog_set x \<union> pc_set y + −
\<union> (mem_set mem - {M a v}) \<union> faults_set f`)+ −
next+ −
from h2(2)+ −
show "{M a v'} \<inter> (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f) = {}"+ −
by (unfold cpn_set_def, auto)+ −
qed+ −
thus ?thesis + −
apply (unfold rset_of.simps)+ −
by (metis `mem_set (mem(a \<mapsto> v')) + −
\<union> prog_set x \<union> pc_set y \<union> faults_set f \<in> m a v' * r` + −
stimes_comm sup_commute sup_left_commute)+ −
qed+ −
qed+ −
+ −
lemma spc_upd: "rset_of (x, i, y, z) \<in> pc i' * r \<Longrightarrow> + −
rset_of (x, i'', y, z) \<in> pc i'' * r"+ −
proof -+ −
assume h: "rset_of (x, i, y, z) \<in> pc i' * r"+ −
from stimes_sgD [OF h[unfolded rset_of.simps pc_set_def pc_def]]+ −
have h1: "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} \<in> r" + −
"{At i'} \<subseteq> prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z" by auto+ −
from h1(2) have eq_i: "i' = i" by (unfold cpn_set_def, auto)+ −
have "prog_set x \<union> {At i} \<union> mem_set y \<union> faults_set z - {At i'} =+ −
prog_set x \<union> mem_set y \<union> faults_set z "+ −
apply (unfold eq_i)+ −
by (metis (full_types) Un_insert_left Un_insert_right + −
diff_pc_set faults_set_def insert_commute insert_is_Un + −
pc_set_def sup_assoc sup_bot_left sup_commute)+ −
with h1(1) have in_r: "prog_set x \<union> mem_set y \<union> faults_set z \<in> r" by auto+ −
show ?thesis+ −
proof(unfold rset_of.simps, rule stimesI[OF _ _ _ in_r])+ −
show "{At i''} \<in> pc i''" by (unfold pc_def pc_set_def, simp)+ −
next+ −
show "prog_set x \<union> pc_set i'' \<union> mem_set y \<union> faults_set z =+ −
{At i''} \<union> (prog_set x \<union> mem_set y \<union> faults_set z)"+ −
by (unfold pc_set_def, auto)+ −
next+ −
show "{At i''} \<inter> (prog_set x \<union> mem_set y \<union> faults_set z) = {}"+ −
by (auto simp:cpn_set_def)+ −
qed+ −
qed+ −
+ −
lemma condD: "s \<in> <b>*r \<Longrightarrow> b"+ −
by (unfold st_def pasrt_def, auto)+ −
+ −
lemma condD1: "s \<in> <b>*r \<Longrightarrow> s \<in> r"+ −
by (unfold st_def pasrt_def, auto)+ −
+ −
lemma hoare_dec_suc: "{(pc i * m a v) * <(v > 0)>} + −
i:[\<guillemotright>(Dec a e) ]:j + −
{pc j * m a (v - 1)}"+ −
proof(unfold Hoare_abc_def, clarify)+ −
fix prog i' ab b r + −
assume h: "rset_of (prog, i', ab, b) \<in> ((pc i * m a v) * <(0 < v)>) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
(is "?r \<in> ?S")+ −
show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
proof -+ −
from h [unfolded assemble_to.simps]+ −
have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a v * <(0 < v)> * <(j = i + 1)> * r"+ −
"?r \<in> m a v * pc i * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r"+ −
"?r \<in> <(0 < v)> * <(j = i + 1)> * m a v * pc i * {{C i (Dec a e)}} * r"+ −
"?r \<in> <(j = i + 1)> * <(0 < v)> * m a v * pc i * {{C i (Dec a e)}} * r"+ −
by ((metis stimes_ac)+)+ −
note h2 = condD [OF h1(3)] condD[OF h1(4)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]+ −
hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> v - Suc 0), b)" (is "?x = ?y")+ −
by (unfold run_def, auto)+ −
have "rset_of ?x \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
proof -+ −
have "rset_of ?y \<in> (pc j * m a (v - 1)) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
proof -+ −
from spc_upd[OF h1(1), of "Suc i"]+ −
have "rset_of (prog, (Suc i), ab, b) \<in> + −
m a v * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" + −
by (metis stimes_ac)+ −
from smem_upd[OF this, of "v - (Suc 0)"]+ −
have "rset_of ?y \<in> + −
m a (v - Suc 0) * pc (Suc i) * {{C i (Dec a e)}} * <(0 < v)> * <(j = i + 1)> * r" .+ −
hence "rset_of ?y \<in> <(0 < v)> *+ −
(pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r"+ −
by (metis stimes_ac)+ −
from condD1[OF this] + −
have "rset_of ?y \<in> (pc (Suc i) * m a (v - Suc 0)) * ({{C i (Dec a e)}} * <(j = i + 1)>) * r" .+ −
thus ?thesis+ −
by (unfold h2(2) assemble_to.simps, simp)+ −
qed+ −
with stp show ?thesis by simp+ −
qed+ −
thus ?thesis by blast+ −
qed+ −
qed+ −
+ −
lemma hoare_dec_fail: "{pc i * m a 0} + −
i:[ \<guillemotright>(Dec a e) ]:j + −
{pc e * m a 0}"+ −
proof(unfold Hoare_abc_def, clarify)+ −
fix prog i' ab b r + −
assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
(is "?r \<in> ?S")+ −
show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
proof -+ −
from h [unfolded assemble_to.simps]+ −
have h1: "?r \<in> pc i * {{C i (Dec a e)}} * m a 0 * <(j = i + 1)> * r"+ −
"?r \<in> m a 0 * pc i * {{C i (Dec a e)}} * <(j = i + 1)> * r"+ −
"?r \<in> <(j = i + 1)> * m a 0 * pc i * {{C i (Dec a e)}} * r"+ −
by ((metis stimes_ac)+)+ −
note h2 = condD [OF h1(3)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]+ −
hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y")+ −
by (unfold run_def, auto)+ −
have "rset_of ?x \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
proof -+ −
have "rset_of ?y \<in> (pc e * m a 0) * (i :[ \<guillemotright>Dec a e ]: j) * r"+ −
proof -+ −
from spc_upd[OF h1(1), of "e"]+ −
have "rset_of ?y \<in> pc e * {{C i (Dec a e)}} * m a 0 * <(j = i + 1)> * r" .+ −
thus ?thesis+ −
by (unfold assemble_to.simps, metis stimes_ac)+ −
qed+ −
with stp show ?thesis by simp+ −
qed+ −
thus ?thesis by blast+ −
qed+ −
qed+ −
+ −
lemma pasrtD_p: "\<lbrakk>{p*<b>} c {q}\<rbrakk> \<Longrightarrow> (b \<longrightarrow> {p} c {q})"+ −
apply (unfold Hoare_abc_def pasrt_def, auto)+ −
by (fold emp_def, simp add:emp_unit_r)+ −
+ −
lemma hoare_dec: "dec_fun v j e = (pc', v') \<Longrightarrow> + −
{pc i * m a v} + −
i:[ \<guillemotright>(Dec a e) ]:j + −
{pc pc' * m a v'}"+ −
proof -+ −
assume "dec_fun v j e = (pc', v')"+ −
thus "{pc i * m a v} + −
i:[ \<guillemotright>(Dec a e) ]:j + −
{pc pc' * m a v'}"+ −
apply (auto split:if_splits simp:dec_fun_def)+ −
apply (insert hoare_dec_fail, auto)[1]+ −
apply (insert hoare_dec_suc, auto)+ −
apply (atomize)+ −
apply (erule_tac x = i in allE, erule_tac x = a in allE,+ −
erule_tac x = v in allE, erule_tac x = e in allE, erule_tac x = pc' in allE)+ −
by (drule_tac pasrtD_p, clarify)+ −
qed+ −
+ −
lemma hoare_inc: "{pc i * m a v} + −
i:[ \<guillemotright>(Inc a) ]:j + −
{pc j * m a (v + 1)}"+ −
proof(unfold Hoare_abc_def, clarify)+ −
fix prog i' ab b r + −
assume h: "rset_of (prog, i', ab, b) \<in> (pc i * m a v) * (i :[ \<guillemotright>Inc a ]: j) * r"+ −
(is "?r \<in> ?S")+ −
show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r"+ −
proof -+ −
from h [unfolded assemble_to.simps]+ −
have h1: "?r \<in> pc i * {{C i (Inc a)}} * m a v * <(j = i + 1)> * r"+ −
"?r \<in> m a v * pc i * {{C i (Inc a)}} * <(j = i + 1)> * r"+ −
"?r \<in> <(j = i + 1)> * m a v * pc i * {{C i (Inc a)}} * r"+ −
by ((metis stimes_ac)+)+ −
note h2 = condD [OF h1(3)] pcD[OF h1(1)] codeD[OF h1(1)] memD[OF h1(2)]+ −
hence stp: "run 1 (prog, i', ab, b) = (prog, Suc i, ab(a \<mapsto> Suc v), b)" (is "?x = ?y")+ −
by (unfold run_def, auto)+ −
have "rset_of ?x \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a]: j) * r"+ −
proof -+ −
have "rset_of ?y \<in> (pc j * m a (v + 1)) * (i :[ \<guillemotright>Inc a ]: j) * r"+ −
proof -+ −
from spc_upd[OF h1(1), of "Suc i"]+ −
have "rset_of (prog, (Suc i), ab, b) \<in> + −
m a v * pc (Suc i) * {{C i (Inc a)}} * <(j = i + 1)> * r" + −
by (metis stimes_ac)+ −
from smem_upd[OF this, of "Suc v"]+ −
have "rset_of ?y \<in> + −
m a (v + 1) * pc (i + 1) * {{C i (Inc a)}} * <(j = i + 1)> * r" by simp+ −
thus ?thesis+ −
by (unfold h2(1) assemble_to.simps, metis stimes_ac)+ −
qed+ −
with stp show ?thesis by simp+ −
qed+ −
thus ?thesis by blast+ −
qed+ −
qed+ −
+ −
lemma hoare_goto: "{pc i} + −
i:[ \<guillemotright>(Goto e) ]:j + −
{pc e}"+ −
proof(unfold Hoare_abc_def, clarify)+ −
fix prog i' ab b r + −
assume h: "rset_of (prog, i', ab, b) \<in> pc i * (i :[ \<guillemotright>Goto e ]: j) * r"+ −
(is "?r \<in> ?S")+ −
show "\<exists>k. rset_of (run k (prog, i', ab, b)) \<in> pc e * (i :[ \<guillemotright>Goto e ]: j) * r"+ −
proof -+ −
from h [unfolded assemble_to.simps]+ −
have h1: "?r \<in> pc i * {{C i (Goto e)}} * <(j = i + 1)> * r"+ −
by ((metis stimes_ac)+)+ −
note h2 = pcD[OF h1(1)] codeD[OF h1(1)] + −
hence stp: "run 1 (prog, i', ab, b) = (prog, e, ab, b)" (is "?x = ?y")+ −
by (unfold run_def, auto)+ −
have "rset_of ?x \<in> pc e * (i :[ \<guillemotright>Goto e]: j) * r"+ −
proof -+ −
from spc_upd[OF h1(1), of "e"] + −
show ?thesis+ −
by (unfold stp assemble_to.simps, metis stimes_ac)+ −
qed+ −
thus ?thesis by blast+ −
qed+ −
qed+ −
+ −
no_notation stimes (infixr "*" 70)+ −
+ −
interpretation foo: comm_monoid_mult + −
"stimes :: 'a set set => 'a set set => 'a set set" "emp::'a set set"+ −
apply(default)+ −
apply(simp add: stimes_assoc)+ −
apply(simp add: stimes_comm)+ −
apply(simp add: emp_def[symmetric])+ −
done+ −
+ −
+ −
notation stimes (infixr "*" 70)+ −
+ −
(*used by simplifier for numbers *)+ −
thm mult_cancel_left+ −
+ −
(*+ −
interpretation foo: comm_ring_1 "op * :: 'a set set => 'a set set => 'a set set" "{{}}::'a set set" + −
apply(default)+ −
*)+ −
+ −
lemma frame: "{p} c {q} \<Longrightarrow> \<forall> r. {p * r} c {q * r}"+ −
apply (unfold Hoare_abc_def, clarify)+ −
apply (erule_tac x = "(a, aa, ab, b)" in allE)+ −
apply (erule_tac x = "r * ra" in allE) + −
apply(metis stimes_ac)+ −
done+ −
+ −
lemma code_extension: "\<lbrakk>{p} c {q}\<rbrakk> \<Longrightarrow> (\<forall> e. {p} c * e {q})"+ −
apply (unfold Hoare_abc_def, clarify)+ −
apply (erule_tac x = "(a, aa, ab, b)" in allE)+ −
apply (erule_tac x = "e * r" in allE)+ −
apply(metis stimes_ac)+ −
done+ −
+ −
lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"+ −
apply (unfold run_def)+ −
by (metis funpow_add o_apply)+ −
+ −
lemma composition: "\<lbrakk>{p} c1 {q}; {q} c2 {r}\<rbrakk> \<Longrightarrow> {p} c1 * c2 {r}"+ −
proof -+ −
assume h: "{p} c1 {q}" "{q} c2 {r}"+ −
from code_extension [OF h(1), rule_format, of "c2"] + −
have "{p} c1 * c2 {q}" .+ −
moreover from code_extension [OF h(2), rule_format, of "c1"] and stimes_comm+ −
have "{q} c1 * c2 {r}" by metis+ −
ultimately show "{p} c1 * c2 {r}"+ −
apply (unfold Hoare_abc_def, clarify)+ −
proof -+ −
fix a aa ab b ra+ −
assume h1: "\<forall>s r. rset_of s \<in> p * (c1 * c2) * r \<longrightarrow>+ −
(\<exists>k. rset_of (run k s) \<in> q * (c1 * c2) * r)"+ −
and h2: "\<forall>s ra. rset_of s \<in> q * (c1 * c2) * ra \<longrightarrow>+ −
(\<exists>k. rset_of (run k s) \<in> r * (c1 * c2) * ra)"+ −
and h3: "rset_of (a, aa, ab, b) \<in> p * (c1 * c2) * ra"+ −
show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> r * (c1 * c2) * ra"+ −
proof -+ −
let ?s = "(a, aa, ab, b)"+ −
from h1 [rule_format, of ?s, OF h3]+ −
obtain n1 where "rset_of (run n1 ?s) \<in> q * (c1 * c2) * ra" by blast+ −
from h2 [rule_format, OF this]+ −
obtain n2 where "rset_of (run n2 (run n1 ?s)) \<in> r * (c1 * c2) * ra" by blast+ −
with run_add show ?thesis by metis+ −
qed+ −
qed+ −
qed+ −
+ −
lemma stimes_simp: "s \<in> x * y = (\<exists> s1 s2. (s = s1 \<union> s2 \<and> s1 \<inter> s2 = {} \<and> s1 \<in> x \<and> s2 \<in> y))"+ −
by (metis (lifting) stimesE stimesI)+ −
+ −
lemma hoare_seq: + −
"\<lbrakk>\<forall> i j. {pc i * p} i:[c1]:j {pc j * q}; + −
\<forall> j k. {pc j * q} j:[c2]:k {pc k * r}\<rbrakk> \<Longrightarrow> {pc i * p} i:[(c1 ; c2)]:k {pc k *r}"+ −
proof -+ −
assume h: "\<forall>i j. {pc i * p} i :[ c1 ]: j {pc j * q}" "\<forall> j k. {pc j * q} j:[c2]:k {pc k * r}"+ −
show "{pc i * p} i:[(c1 ; c2)]:k {pc k *r}"+ −
proof(subst Hoare_abc_def, clarify)+ −
fix a aa ab b ra+ −
assume "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ (c1 ; c2) ]: k) * ra"+ −
hence "rset_of (a, aa, ab, b) \<in> (i :[ (c1 ; c2) ]: k) * (pc i * p * ra)" (is "?s \<in> ?X * ?Y")+ −
by (metis stimes_ac)+ −
from stimesE[OF this] obtain s1 s2 where+ −
sp: "rset_of(a, aa, ab, b) = s1 \<union> s2" "s1 \<inter> s2 = {}" "s1 \<in> ?X" "s2 \<in> ?Y" by blast+ −
from sp (3) obtain j' where + −
"s1 \<in> (i:[c1]:j') * (j':[c2]:k)" (is "s1 \<in> ?Z")+ −
by (auto simp:assemble_to.simps)+ −
from stimesI[OF sp(1, 2) this sp(4)]+ −
have "?s \<in> (pc i * p) * (i :[ c1 ]: j') * (j' :[ c2 ]: k) * ra" by (metis stimes_ac)+ −
from h(1)[unfolded Hoare_abc_def, rule_format, OF this]+ −
obtain ka where + −
"rset_of (run ka (a, aa, ab, b)) \<in> (pc j' * q) * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" + −
sorry+ −
from h(2)[unfolded Hoare_abc_def, rule_format, OF this]+ −
obtain kb where + −
"rset_of (run kb (run ka (a, aa, ab, b)))+ −
\<in> (pc k * r) * (j' :[ c2 ]: k) * (i :[ c1 ]: j') * ra" by blast+ −
hence h3: "rset_of (run (kb + ka) (a, aa, ab, b))+ −
\<in> pc k * r * (j' :[ c2 ]: k) * ((i :[ c1 ]: j') * ra)" + −
sorry+ −
hence "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> pc k * r * (i :[ (c1 ; c2) ]: k) * ra"+ −
proof -+ −
have "rset_of (run (kb + ka) (a, aa, ab, b)) \<in> (i :[ (c1 ; c2) ]: k) * (pc k * r * ra)"+ −
proof -+ −
from h3 have "rset_of (run (kb + ka) (a, aa, ab, b))+ −
\<in> ((j' :[ c2 ]: k) * ((i :[ c1 ]: j'))) * (pc k * r * ra)"+ −
by (metis stimes_ac)+ −
then obtain + −
s1 s2 where h4: "rset_of (run (kb + ka) (a, aa, ab, b)) = s1 \<union> s2"+ −
" s1 \<inter> s2 = {}" "s1 \<in> (j' :[ c2 ]: k) * (i :[ c1 ]: j')"+ −
"s2 \<in> pc k * r * ra" by (rule stimesE, blast)+ −
from h4(3) have "s1 \<in> (i :[ (c1 ; c2) ]: k)"+ −
sorry+ −
from stimesI [OF h4(1, 2) this h4(4)]+ −
show ?thesis .+ −
qed+ −
thus ?thesis by (metis stimes_ac)+ −
qed+ −
thus "\<exists>ka. rset_of (run ka (a, aa, ab, b)) \<in> (pc k * r) * (i :[ (c1 ; c2) ]: k) * ra"+ −
by (metis stimes_ac)+ −
qed+ −
qed+ −
+ −
lemma hoare_local: + −
"\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} + −
\<Longrightarrow> {pc i * p} i:[Local c]:j {pc j * q}"+ −
proof -+ −
assume h: "\<forall> l i j. {pc i*p} i:[c(l)]:j {pc j * q} "+ −
show "{pc i * p} i:[Local c]:j {pc j * q}"+ −
proof(unfold assemble_to.simps Hoare_abc_def, clarify)+ −
fix a aa ab b r+ −
assume h1: "rset_of (a, aa, ab, b) \<in> (pc i * p) * (\<Union>l. i :[ c l ]: j) * r"+ −
hence "rset_of (a, aa, ab, b) \<in> (\<Union>l. i :[ c l ]: j) * (pc i * p * r)" + −
by (metis stimes_ac)+ −
then obtain s1 s2 l + −
where "rset_of (a, aa, ab, b) = s1 \<union> s2"+ −
"s1 \<inter> s2 = {}"+ −
"s1 \<in> (i :[ c l ]: j)"+ −
"s2 \<in> pc i * p * r"+ −
by (rule stimesE, auto)+ −
from stimesI[OF this]+ −
have "rset_of (a, aa, ab, b) \<in> (pc i * p) * (i :[ c l ]: j) * r" + −
by (metis stimes_ac)+ −
from h[unfolded Hoare_abc_def, rule_format, OF this]+ −
obtain k where "rset_of (run k (a, aa, ab, b)) \<in> (i :[ c l ]: j) * (pc j * q * r)" + −
sorry+ −
then obtain s1 s2+ −
where h3: "rset_of (run k (a, aa, ab, b)) = s1 \<union> s2"+ −
" s1 \<inter> s2 = {}" "s1 \<in> (\<Union> l. (i :[ c l ]: j))" "s2 \<in> pc j * q * r" + −
by(rule stimesE, auto)+ −
from stimesI[OF this]+ −
show "\<exists>k. rset_of (run k (a, aa, ab, b)) \<in> (pc j * q) * (\<Union>l. i :[ c l ]: j) * r"+ −
by (metis stimes_ac)+ −
qed+ −
qed+ −
+ −
lemma move_pure: "{p*<b>} c {q} = (b \<longrightarrow> {p} c {q})"+ −
proof(unfold Hoare_abc_def, default, clarify)+ −
fix prog i' mem ft r+ −
assume h: "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
"b" "rset_of (prog, i', mem, ft) \<in> p * c * r"+ −
show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r"+ −
proof(rule h(1)[rule_format])+ −
have "(p * <b>) * c * r = <b> * p * c * r" by (metis stimes_ac)+ −
moreover have "rset_of (prog, i', mem, ft) \<in> \<dots>"+ −
proof(rule stimesI[OF _ _ _ h(3)])+ −
from h(2) show "{} \<in> <b>" by (auto simp:pasrt_def)+ −
qed auto+ −
ultimately show "rset_of (prog, i', mem, ft) \<in> (p * <b>) * c * r"+ −
by (simp)+ −
qed+ −
next+ −
assume h: "b \<longrightarrow> (\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r))"+ −
show "\<forall>s r. rset_of s \<in> (p * <b>) * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
proof -+ −
{ fix s r + −
assume "rset_of s \<in> (p * <b>) * c * r"+ −
hence h1: "rset_of s \<in> <b> * p * c * r" by (metis stimes_ac)+ −
have "(\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
proof(rule h[rule_format])+ −
from condD[OF h1] show b .+ −
next+ −
from condD1[OF h1] show "rset_of s \<in> p * c * r" .+ −
qed+ −
} thus ?thesis by blast+ −
qed+ −
qed+ −
+ −
lemma precond_ex: "{\<Union> x. p x} c {q} = (\<forall> x. {p x} c {q})"+ −
proof(unfold Hoare_abc_def, default, clarify)+ −
fix x prog i' mem ft r+ −
assume h: "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
"rset_of (prog, i', mem, ft) \<in> p x * c * r"+ −
show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r"+ −
proof(rule h[rule_format])+ −
from h(2) show "rset_of (prog, i', mem, ft) \<in> UNION UNIV p * c * r" by (auto simp:stimes_def)+ −
qed+ −
next+ −
assume h: "\<forall>x s r. rset_of s \<in> p x * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
show "\<forall>s r. rset_of s \<in> UNION UNIV p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
proof -+ −
{ fix s r+ −
assume "rset_of s \<in> UNION UNIV p * c * r"+ −
then obtain x where "rset_of s \<in> p x * c * r" + −
by (unfold st_def, auto, metis)+ −
hence "(\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
by(rule h[rule_format])+ −
} thus ?thesis by blast+ −
qed+ −
qed+ −
+ −
lemma code_exI: "\<lbrakk>\<And>l. {p} c l * c' {q}\<rbrakk> \<Longrightarrow> {p} (\<Union> l. c l) * c' {q}"+ −
proof(unfold Hoare_abc_def, default, clarify)+ −
fix prog i' mem ft r+ −
assume h: "\<And>l. \<forall>s r. rset_of s \<in> p * (c l * c') * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * (c l * c') * r)"+ −
"rset_of (prog, i', mem, ft) \<in> p * (UNION UNIV c * c') * r"+ −
show " \<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * (UNION UNIV c * c') * r"+ −
proof -+ −
from h(2) obtain l where "rset_of (prog, i', mem, ft) \<in> p * (c l * c') * r"+ −
apply (unfold st_def, auto)+ −
by metis+ −
from h(1)[rule_format, OF this]+ −
obtain k where " rset_of (run k (prog, i', mem, ft)) \<in> q * (c l * c') * r" by blast+ −
thus ?thesis by (unfold st_def, auto, metis)+ −
qed+ −
qed+ −
+ −
lemma code_exIe: "\<lbrakk>\<And>l. {p} c l{q}\<rbrakk> \<Longrightarrow> {p} \<Union> l. (c l) {q}"+ −
proof -+ −
assume "\<And>l. {p} c l {q}"+ −
thus "{p} \<Union>l. c l {q}"+ −
by(rule code_exI[where c'= "emp", unfolded emp_unit_r])+ −
qed+ −
+ −
lemma pre_stren: "\<lbrakk>{p} c {q}; r \<subseteq> p\<rbrakk> \<Longrightarrow> {r} c {q}"+ −
proof(unfold Hoare_abc_def, clarify)+ −
fix prog i' mem ft r'+ −
assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
" r \<subseteq> p" " rset_of (prog, i', mem, ft) \<in> r * c * r'"+ −
show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'"+ −
proof(rule h(1)[rule_format])+ −
from stimes_mono[OF h(2), of "c * r'"] h(3)+ −
show "rset_of (prog, i', mem, ft) \<in> p * c * r'" by auto+ −
qed+ −
qed+ −
+ −
lemma post_weaken: "\<lbrakk>{p} c {q}; q \<subseteq> r\<rbrakk> \<Longrightarrow> {p} c {r}"+ −
proof(unfold Hoare_abc_def, clarify)+ −
fix prog i' mem ft r'+ −
assume h: "\<forall>s r. rset_of s \<in> p * c * r \<longrightarrow> (\<exists>k. rset_of (run k s) \<in> q * c * r)"+ −
" q \<subseteq> r" "rset_of (prog, i', mem, ft) \<in> p * c * r'"+ −
show "\<exists>k. rset_of (run k (prog, i', mem, ft)) \<in> r * c * r'"+ −
proof -+ −
from h(1)[rule_format, OF h(3)]+ −
obtain k where "rset_of (run k (prog, i', mem, ft)) \<in> q * c * r'" by auto+ −
moreover from h(2) have "\<dots> \<subseteq> r * c * r'" by (metis stimes_mono)+ −
ultimately show ?thesis by auto+ −
qed+ −
qed+ −
+ −
definition "clear a = + −
Local (\<lambda> start. (Local (\<lambda> exit. Label start; \<guillemotright>Dec a exit; \<guillemotright> Goto start; Label exit)))"+ −
+ −
lemma "{pc i * m a v} i:[clear a]:j {pc j*m a 0}"+ −
proof (unfold clear_def, rule hoare_local, default+)+ −
fix l i j+ −
show "{pc i * m a v} i :[ Local (\<lambda>exit. Label l ; \<guillemotright>Dec a exit ; \<guillemotright>Goto l ; Label exit) ]: j+ −
{pc j * m a 0}"+ −
proof(rule hoare_local, default+)+ −
fix la i j + −
show "{pc i * m a v} i :[ (Label l ; \<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j {pc j * m a 0}"+ −
proof(subst assemble_to.simps, rule code_exIe)+ −
have "\<And>j'. {pc i * m a v} (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j) * (i :[ Label l ]: j')+ −
{pc j * m a 0}" + −
proof(subst assemble_to.simps, rule code_exI)+ −
fix j' j'a+ −
show "{pc i * m a v}+ −
((j' :[ \<guillemotright>Dec a la ]: j'a) * (j'a :[ (\<guillemotright>Goto l ; Label la) ]: j)) * (i :[ Label l ]: j')+ −
{pc j * m a 0}"+ −
proof(unfold assemble_to.simps)+ −
have "{pc i * m a v}+ −
((\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * ({{C j' (Dec a la)}} * <(j'a = j' + 1)>) + −
* <(j' = j \<and> j = la)>)) *+ −
<(i = j' \<and> j' = l)>+ −
{pc j * m a 0}"+ −
proof(rule code_exI, fold assemble_to.simps)+ −
qed+ −
thus "{pc i * m a v}+ −
(({{C j' (Dec a la)}} * <(j'a = j' + 1)>) *+ −
(\<Union>j'. ({{C j'a (Goto l)}} * <(j' = j'a + 1)>) * <(j' = j \<and> j = la)>)) *+ −
<(i = j' \<and> j' = l)>+ −
{pc j * m a 0}" sorry+ −
qed+ −
qed+ −
thus "\<And>j'. {pc i * m a v} (i :[ Label l ]: j') * (j' :[ (\<guillemotright>Dec a la ; \<guillemotright>Goto l ; Label la) ]: j)+ −
{pc j * m a 0}" by (metis stimes_ac)+ −
qed+ −
qed+ −
qed+ −
+ −
end+ −