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