tm2: comparison thys/Hoare

equal deleted inserted replaced

-:0352ad5ee9c5
+:86918b45b2e6
 header {*
 Separation logic for Turing Machines
 *}
-theory Hoare_tm
+theory Hoare_tm2
 imports Hoare_gen
 My_block
 Data_slot
 "~~/src/HOL/Library/FinFun_Syntax"
 begin
 fun trset_of :: "tconf \<Rightarrow> tresource set"
 where "trset_of (faults, prog, pc, pos, m) =
 tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults"
 interpretation tm: sep_exec tstep trset_of .
 section {* Assembly language for TMs and its program logic *}
 subsection {* The assembly language *}
 lemma codeD: "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))
 \<Longrightarrow> prog $ i = Some inst"
 proof -
 assume "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))"
 thus ?thesis
 apply(unfold sep_conj_def set_ins_def sg_def trset_of.simps tpn_set_def)
 by auto
 qed
-lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))  \<Longrightarrow> mem a = Some v"
+lemma memD: "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))  \<Longrightarrow> mem $ a = Some v"
 proof -
 assume "((tm a v) ** r) (trset_of (ft, prog, i, pos, mem))"
 from stimes_sgD[OF this[unfolded trset_of.simps tpn_set_def tm_def]]
-have "{TM a v} \<subseteq> {TC i inst |i inst. prog i = Some inst} \<union> {TAt i} \<union>
+have "{TM a v} \<subseteq> {TC i inst |i inst. prog $ i = Some inst} \<union> {TAt i} \<union>
-{TPos pos} \<union> {TM i n |i n. mem i = Some n} \<union> {TFaults ft}" by simp
+{TPos pos} \<union> {TM i n |i n. mem $ i = Some n} \<union> {TFaults ft}" by simp
 thus ?thesis by auto
 qed
 lemma t_hoare_seq:
 assumes a1: "\<And> i j. \<lbrace>st i \<and>* p\<rbrace> i:[c1]:j \<lbrace>st j \<and>* q\<rbrace>"
 ({TM a v} \<subseteq> tmem_set mem)"
 by (unfold tpn_set_def, auto)
 lemma tmem_set_upd:
 "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow>
-tmem_set (mem(a:=Some v')) = ((tmem_set mem) - {TM a v}) \<union> {TM a v'}"
+tmem_set (mem(a $:=Some v')) = ((tmem_set mem) - {TM a v}) \<union> {TM a v'}"
-by (unfold tpn_set_def, auto)
+apply(unfold tpn_set_def)
+apply(auto)
+apply (metis finfun_upd_apply option.inject)
+apply (metis finfun_upd_apply_other)
+by (metis finfun_upd_apply_other option.inject)
 lemma tmem_set_disj: "{TM a v} \<subseteq> tmem_set mem \<Longrightarrow>
 {TM a v'} \<inter>  (tmem_set mem - {TM a v}) = {}"
 by (unfold tpn_set_def, auto)
 lemma smem_upd: "((tm a v) ** r) (trset_of (f, x, y, z, mem))  \<Longrightarrow>
-((tm a v') ** r) (trset_of (f, x, y, z, mem(a := Some v')))"
+((tm a v') ** r) (trset_of (f, x, y, z, mem(a $:= Some v')))"
 proof -
 have eq_s: "(tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tmem_set mem \<union> tfaults_set f - {TM a v}) =
 (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)"
 by (unfold tpn_set_def, auto)
 assume g: "(tm a v \<and>* r) (trset_of (f, x, y, z, mem))"
 hence h0: "r (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)"
 by(sep_drule stimes_sgD, clarify, unfold eq_s, auto)
 from h TM_in_simp have "{TM a v} \<subseteq> tmem_set mem"
 by(sep_drule stimes_sgD, auto)
 from tmem_set_upd [OF this] tmem_set_disj[OF this]
-have h2: "tmem_set (mem(a \<mapsto> v')) = {TM a v'} \<union> (tmem_set mem - {TM a v})"
+have h2: "tmem_set (mem(a $:= Some v')) = {TM a v'} \<union> (tmem_set mem - {TM a v})"
 "{TM a v'} \<inter> (tmem_set mem - {TM a v}) = {}" by auto
 show ?thesis
 proof -
-have "(tm a v' ** r) (tmem_set (mem(a \<mapsto> v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f)"
+have "(tm a v' ** r) (tmem_set (mem(a $:= Some v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f)"
 proof(rule sep_conjI)
 show "tm a v' ({TM a v'})" by (unfold tm_def sg_def, simp)
 next
 from h0 show "r (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)" .
 next
 show "{TM a v'} ## tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f"
 proof -
-from g have " mem a = Some v"
+from g have " mem $ a = Some v"
 by(sep_frule memD, simp)
 thus "?thesis"
 by(unfold tpn_set_def set_ins_def, auto)
 qed
 next
-show "tmem_set (mem(a \<mapsto> v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f =
+show "tmem_set (mem(a $:= Some v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f =
 {TM a v'} + (tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> (tmem_set mem - {TM a v}) \<union> tfaults_set f)"
 by (unfold h2(1) set_ins_def eq_s, auto)
 qed
 thus ?thesis
 apply (unfold trset_of.simps)
 \<lbrace>st (Suc i) \<and>* ps p \<and>* tm p Bk\<rbrace>"
 proof(fold eq_j, unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs i' mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* sg {TC i ((W0, j), W0, j)})
 (trset_of (ft, prog, cs, i', mem))"
-from h have "prog i = Some ((W0, j), W0, j)"
+from h have "prog $ i = Some ((W0, j), W0, j)"
 apply(rule_tac r = "r \<and>* ps p \<and>* tm p v" in codeD)
 by(simp add: sep_conj_ac)
 from h and this have stp:
-"tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, j, i', mem(i'\<mapsto> Bk))" (is "?x = ?y")
+"tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, j, i', mem(i' $:= Some Bk))" (is "?x = ?y")
 apply(sep_frule psD)
 apply(sep_frule stD)
 apply(sep_frule memD, simp)
 by(cases v, unfold tm.run_def, auto)
 from h have "i' = p"
 \<lbrace>ps p \<and>* st ?j \<and>* tm p Oc\<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs i' mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* sg {TC i ((W1, ?j), W1, ?j)})
 (trset_of (ft, prog, cs, i', mem))"
-from h have "prog i = Some ((W1, ?j), W1, ?j)"
+from h have "prog $ i = Some ((W1, ?j), W1, ?j)"
 apply(rule_tac r = "r \<and>* ps p \<and>* tm p v" in codeD)
 by(simp add: sep_conj_ac)
 from h and this have stp:
 "tm.run 1 (ft, prog, cs, i', mem) =
-(ft, prog, ?j, i', mem(i'\<mapsto> Oc))" (is "?x = ?y")
+(ft, prog, ?j, i', mem(i' $:= Some Oc))" (is "?x = ?y")
 apply(sep_frule psD)
 apply(sep_frule stD)
 apply(sep_frule memD, simp)
 by(cases v, unfold tm.run_def, auto)
 from h have "i' = p"
 \<lbrace>st ?j \<and>* tm p v2 \<and>* ps (p - 1)\<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs i' mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v2 \<and>* sg {TC i ((L, ?j), L, ?j)})
 (trset_of (ft, prog, cs, i',  mem))"
-from h have "prog i = Some ((L, ?j), L, ?j)"
+from h have "prog $ i = Some ((L, ?j), L, ?j)"
 apply(rule_tac r = "r \<and>* ps p \<and>* tm p v2" in codeD)
 by(simp add: sep_conj_ac)
 from h and this have stp:
 "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, ?j, i' - 1, mem)" (is "?x = ?y")
 apply(sep_frule psD)
 \<lbrace>st ?j \<and>* tm p v1 \<and>* ps (p + 1)\<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs i' mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v1 \<and>* sg {TC i ((R, ?j), R, ?j)})
 (trset_of (ft, prog, cs, i',  mem))"
-from h have "prog i = Some ((R, ?j), R, ?j)"
+from h have "prog $ i = Some ((R, ?j), R, ?j)"
 apply(rule_tac r = "r \<and>* ps p \<and>* tm p v1" in codeD)
 by(simp add: sep_conj_ac)
 from h and this have stp:
 "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, ?j, i'+ 1, mem)" (is "?x = ?y")
 apply(sep_frule psD)
 show "\<lbrace>one p \<and>* ps p \<and>* st i\<rbrace>  sg {TC i ((W0, ?j), W1, e)} \<lbrace>one p \<and>* ps p \<and>* st e\<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs pc mem r
 assume h: "(r \<and>* one p \<and>* ps p \<and>* st i \<and>* sg {TC i ((W0, ?j), W1, e)})
 (trset_of (ft, prog, cs, pc, mem))"
-from h have k1: "prog i = Some ((W0, ?j), W1, e)"
+from h have k1: "prog $ i = Some ((W0, ?j), W1, e)"
 apply(rule_tac r = "r \<and>* one p \<and>* ps p" in codeD)
 by(simp add: sep_conj_ac)
 from h have k2: "pc = p"
 by(sep_drule psD, simp)
-from h and this have k3: "mem pc = Some Oc"
+from h and this have k3: "mem $ pc = Some Oc"
 apply(unfold one_def)
 by(sep_drule memD, simp)
 from h k1 k2 k3 have stp:
 "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, e, pc, mem)" (is "?x = ?y")
 apply(sep_drule stD)
-by(unfold tm.run_def, auto)
+apply(unfold tm.run_def)
+apply(auto)
+by (metis finfun_upd_triv)
 from h k2
 have "(r \<and>* one p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, ?j), W1, e)})  (trset_of ?x)"
 apply(unfold stp)
 by(sep_drule st_upd, simp add: sep_conj_ac)
 thus "\<exists>k.(r \<and>* one p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, ?j), W1, e)})
 show "\<lbrace>ps p \<and>* st i \<and>* zero p\<rbrace>  sg {TC i ((W0, ?j), W1, e)} \<lbrace>ps p \<and>*  zero p \<and>* st ?j \<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs pc mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* sg {TC i ((W0, ?j), W1, e)})
 (trset_of (ft, prog, cs, pc, mem))"
-from h have k1: "prog i = Some ((W0, ?j), W1, e)"
+from h have k1: "prog $ i = Some ((W0, ?j), W1, e)"
 apply(rule_tac r = "r \<and>* zero p \<and>* ps p" in codeD)
 by(simp add: sep_conj_ac)
 from h have k2: "pc = p"
 by(sep_drule psD, simp)
-from h and this have k3: "mem pc = Some Bk"
+from h and this have k3: "mem $ pc = Some Bk"
 apply(unfold zero_def)
 by(sep_drule memD, simp)
 from h k1 k2 k3 have stp:
 "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, ?j, pc, mem)" (is "?x = ?y")
 apply(sep_drule stD)
-by(unfold tm.run_def, auto)
+apply(unfold tm.run_def)
+apply(auto)
+by (metis finfun_upd_triv)
 from h k2
 have "(r \<and>* zero p \<and>* ps p \<and>* st ?j \<and>* sg {TC i ((W0, ?j), W1, e)})  (trset_of ?x)"
 apply (unfold stp)
 by (sep_drule st_upd[where i''="?j"], auto simp:sep_conj_ac)
 thus "\<exists>k. (r \<and>* ps p \<and>* zero p \<and>* st ?j \<and>*  sg {TC i ((W0, ?j), W1, e)})
 show "\<lbrace>ps p \<and>* st i \<and>* zero p\<rbrace>  sg {TC i ((W0, e), W1, ?j)} \<lbrace>ps p \<and>* st e \<and>* zero p\<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs pc mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* zero p \<and>* sg {TC i ((W0, e), W1, ?j)})
 (trset_of (ft, prog, cs, pc, mem))"
-from h have k1: "prog i = Some ((W0, e), W1, ?j)"
+from h have k1: "prog $ i = Some ((W0, e), W1, ?j)"
 apply(rule_tac r = "r \<and>* zero p \<and>* ps p" in codeD)
 by(simp add: sep_conj_ac)
 from h have k2: "pc = p"
 by(sep_drule psD, simp)
-from h and this have k3: "mem pc = Some Bk"
+from h and this have k3: "mem $ pc = Some Bk"
 apply(unfold zero_def)
 by(sep_drule memD, simp)
 from h k1 k2 k3 have stp:
 "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, e, pc, mem)" (is "?x = ?y")
 apply(sep_drule stD)
-by(unfold tm.run_def, auto)
+apply(unfold tm.run_def)
+apply(auto)
+by (metis finfun_upd_triv)
 from h k2
 have "(r \<and>* zero p \<and>* ps p \<and>* st e \<and>* sg {TC i ((W0, e), W1, ?j)})  (trset_of ?x)"
 apply(unfold stp)
 by(sep_drule st_upd, simp add: sep_conj_ac)
 thus "\<exists>k. (r \<and>* ps p \<and>* st e \<and>* zero p \<and>* sg {TC i ((W0, e), W1, ?j)})
 \<lbrace>ps p \<and>* st ?j \<and>* tm p Oc\<rbrace>"
 proof(unfold tassemble_to.simps tm.Hoare_gen_def sep_conj_ac, clarify)
 fix ft prog cs pc mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p Oc \<and>* sg {TC i ((W0, e), W1, ?j)})
 (trset_of (ft, prog, cs, pc, mem))"
-from h have k1: "prog i = Some ((W0, e), W1, ?j)"
+from h have k1: "prog $ i = Some ((W0, e), W1, ?j)"
 apply(rule_tac r = "r \<and>* tm p Oc \<and>* ps p" in codeD)
 by(simp add: sep_conj_ac)
 from h have k2: "pc = p"
 by(sep_drule psD, simp)
-from h and this have k3: "mem pc = Some Oc"
+from h and this have k3: "mem $ pc = Some Oc"
 by(sep_drule memD, simp)
 from h k1 k2 k3 have stp:
 "tm.run 1 (ft, prog, cs, pc, mem) = (ft, prog, ?j, pc, mem)" (is "?x = ?y")
 apply(sep_drule stD)
-by(unfold tm.run_def, auto)
+apply(unfold tm.run_def)
+apply(auto)
+by (metis finfun_upd_triv)
 from h k2
 have "(r \<and>* tm p Oc \<and>* ps p \<and>* st ?j \<and>* sg {TC i ((W0, e), W1, ?j)})  (trset_of ?x)"
 apply(unfold stp)
 by(sep_drule st_upd, simp add: sep_conj_ac)
 thus "\<exists>k. (r \<and>* ps p \<and>* st ?j \<and>* tm p Oc \<and>* sg {TC i ((W0, e), W1, ?j)})
 "\<lbrace>st i \<and>* ps p \<and>* tm p v\<rbrace>  i:[jmp e]:j \<lbrace>st e \<and>* ps p \<and>* tm p v\<rbrace>"
 proof(unfold jmp_def tm.Hoare_gen_def tassemble_to.simps sep_conj_ac, clarify)
 fix ft prog cs pos mem r
 assume h: "(r \<and>* ps p \<and>* st i \<and>* tm p v \<and>* <(j = i + 1)> \<and>* sg {TC i ((W0, e), W1, e)})
 (trset_of (ft, prog, cs, pos, mem))"
-from h have k1: "prog i = Some ((W0, e), W1, e)"
+from h have k1: "prog $ i = Some ((W0, e), W1, e)"
 apply(rule_tac r = "r \<and>* <(j = i + 1)> \<and>* tm p v \<and>* ps p" in codeD)
 by(simp add: sep_conj_ac)
 from h have k2: "p = pos"
 by(sep_drule psD, simp)
-from h k2 have k3: "mem pos = Some v"
+from h k2 have k3: "mem $ pos = Some v"
 by(sep_drule memD, simp)
 from h k1 k2 k3 have
 stp: "tm.run 1 (ft, prog, cs, pos, mem) = (ft, prog, e, pos, mem)" (is "?x = ?y")
 apply(sep_drule stD)
-by(unfold tm.run_def, cases "mem pos", simp, cases v, auto)
+apply(unfold tm.run_def)
+apply(cases "mem $ pos")
+apply(simp)
+apply(cases v)
+apply(auto)
+apply (metis finfun_upd_triv)
+by (metis finfun_upd_triv)
 from h k2
 have "(r \<and>* ps p \<and>* st e \<and>* tm p v \<and>* <(j = i + 1)> \<and>*
 sg {TC i ((W0, e), W1, e)}) (trset_of ?x)"
 apply(unfold stp)
 by(sep_drule st_upd, simp add: sep_conj_ac)
 lemma sep_conj_cond3 : "(<cond1> \<and>* <cond2>) = <(cond1 \<and> cond2)>"
 by (smt cond_eqI cond_true_eq sep_conj_commute sep_conj_empty)
 lemma sep_conj_cond4 : "(<cond1> \<and>* <cond2> \<and>* r) = (<(cond1 \<and> cond2)> \<and>* r)"
-by (metis Hoare_gen.sep_conj_cond3 Hoare_tm.sep_conj_cond3)
+by (metis Hoare_tm2.sep_conj_cond3 sep_conj_assoc)
 lemmas sep_conj_cond = sep_conj_cond3 sep_conj_cond4 sep_conj_cond
 lemma hoare_left_until_zero_reps:
 "\<lbrace>st i ** ps v ** zero u ** reps (u + 1) v [k]\<rbrace>

changeset 17	86918b45b2e6
parent 16	0352ad5ee9c5
child 19	087d82632852