diff -r b66578c08490 -r 8f89170bb076 Tests/abacus-2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tests/abacus-2.thy Fri Mar 29 01:36:45 2013 +0000 @@ -0,0 +1,732 @@ +header {* + {\em abacus} a kind of register machine +*} + +theory abacus +imports Main "../Separation_Algebra/Sep_Tactics" +begin + +instantiation set :: (type)sep_algebra +begin + +definition set_zero_def: "0 = {}" + +definition plus_set_def: "s1 + s2 = s1 \<union> s2" + +definition sep_disj_set_def: "sep_disj s1 s2 = (s1 \<inter> s2 = {})" + +lemmas set_ins_def = sep_disj_set_def plus_set_def set_zero_def + +instance + apply(default) + apply(simp add:set_ins_def) + apply(simp add:sep_disj_set_def plus_set_def set_zero_def) + apply (metis inf_commute) + apply(simp add:sep_disj_set_def plus_set_def set_zero_def) + apply(simp add:sep_disj_set_def plus_set_def set_zero_def) + apply (metis sup_commute) + apply(simp add:sep_disj_set_def plus_set_def set_zero_def) + apply (metis (lifting) Un_assoc) + apply(simp add:sep_disj_set_def plus_set_def set_zero_def) + apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff) + apply(simp add:sep_disj_set_def plus_set_def set_zero_def) + by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff) +end + + +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 + +datatype apg = + Instr abc_inst + | Label nat + | Seq apg apg + | Local "(nat \<Rightarrow> apg)" + +notation Local (binder "L " 10) + +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 "sg e = (\<lambda> s. s = e)" + +definition "pc l = sg (pc_set l)" + +definition "m a v =sg ({M a v})" + +declare rset_of.simps[simp del] + +type_synonym assert = "aresource set \<Rightarrow> bool" + +primrec assemble_to :: "apg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> assert" + where + "assemble_to (Instr ai) i j = (sg ({C i ai}) ** \<langle>(j = i + 1)\<rangle>)" | + "assemble_to (Seq p1 p2) i j = (EXS j'. (assemble_to p1 i j') ** (assemble_to p2 j' j))" | + "assemble_to (Local fp) i j = (EXS l. (assemble_to (fp l) i j))" | + "assemble_to (Label l) i j = \<langle>(i = j \<and> j = l)\<rangle>" + +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: "(sg x ** q) s \<Longrightarrow> q (s - x) \<and> x \<subseteq> s" + apply(erule_tac sep_conjE) + apply(unfold set_ins_def sg_def) + by (metis Diff_Int2 Diff_Int_distrib2 Diff_Un Diff_cancel + Diff_empty Diff_idemp Diff_triv Int_Diff Un_Diff + Un_Diff_cancel inf_commute inf_idem sup_bot_right sup_commute sup_ge2) + +lemma pcD: "(pc i ** r) (rset_of (prog, i', mem, fault)) + \<Longrightarrow> i' = i" +proof - + assume "(pc i ** r) (rset_of (prog, i', mem, fault))" + 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: "(pc i ** sg {C i inst} ** r) (rset_of (prog, pos, mem, fault)) + \<Longrightarrow> prog pos = Some inst" +proof - + assume "(pc i ** sg {C i inst} ** r) (rset_of (prog, pos, mem, fault))" + thus ?thesis + apply(sep_subst pcD) + apply(unfold sep_conj_def set_ins_def sg_def rset_of.simps cpn_set_def) + by auto +qed + +lemma memD: "((m a v) ** r) (rset_of (prog, pos, mem, fault)) \<Longrightarrow> mem a = Some v" +proof - + assume "((m a v) ** r) (rset_of (prog, pos, mem, fault))" + 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. (p**c**r) (rset_of s) \<longrightarrow> + (\<exists> k. ((q ** c ** r) (rset_of (run k s)))))" + +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 smem_upd: "((m a v) ** r) (rset_of (x, y, mem, f)) \<Longrightarrow> + ((m a v') ** r) (rset_of (x, y, mem(a := Some v'), f))" +proof - + have eq_s:" + (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) + assume "(m a v \<and>* r) (rset_of (x, y, mem, f))" + from this[unfolded rset_of.simps m_def] + have h: "(sg {M a v} \<and>* r) (prog_set x \<union> pc_set y \<union> mem_set mem \<union> faults_set f)" . + hence h0: "r (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)" + by(sep_drule stimes_sgD, clarify, unfold eq_s, auto) + from h M_in_simp have "{M a v} \<subseteq> mem_set mem" + by(sep_drule stimes_sgD, auto) + 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 "(m a v' ** r) (mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<union> faults_set f)" + proof(rule sep_conjI) + from h0 show "r (prog_set x \<union> pc_set y \<union> (mem_set mem - {M a v}) \<union> faults_set f)" . + next + show "m a v' ({M a v'})" by (unfold m_def sg_def, simp) + next + show "mem_set (mem(a \<mapsto> v')) \<union> prog_set x \<union> pc_set y \<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 h2(1) set_ins_def eq_s, auto) + next + from h2(2) + show " {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 set_ins_def, auto) + qed + thus ?thesis + apply (unfold rset_of.simps) + by (metis sup_commute sup_left_commute) + qed +qed + +lemma pc_dest: "(pc i') (pc_set i) \<Longrightarrow> i = i'" + sorry + +lemma spc_upd: "(pc i' ** r) (rset_of (x, i, y, z)) \<Longrightarrow> + (pc i'' ** r) (rset_of (x, i'', y, z))" +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 = (L start 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 :[ (L 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, unfold assemble_to.simps(4)) + thm 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