--- a/thys/Hoare_tm2.thy Fri Apr 04 13:15:07 2014 +0100
+++ b/thys/Hoare_tm2.thy Tue Apr 29 15:26:48 2014 +0100
@@ -6,7 +6,7 @@
imports Hoare_gen
My_block
Data_slot
- "~~/src/HOL/Library/FinFun_Syntax"
+ FMap
begin
@@ -64,22 +64,33 @@
- position of head (int)
- tape (int \<rightharpoonup> Block)
*)
-type_synonym tconf = "nat \<times> (nat \<Rightarrow>f tm_inst option) \<times> nat \<times> int \<times> (int \<Rightarrow>f Block option)"
+type_synonym tconf = "nat \<times> (nat f\<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int f\<rightharpoonup> Block)"
(* updates the position/tape according to an action *)
fun
- next_tape :: "taction \<Rightarrow> (int \<times> (int \<Rightarrow>f Block option)) \<Rightarrow> (int \<times> (int \<Rightarrow>f Block option))"
+ next_tape :: "taction \<Rightarrow> (int \<times> (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int f\<rightharpoonup> Block))"
where
- "next_tape W0 (pos, m) = (pos, m(pos $:= Some Bk))" |
- "next_tape W1 (pos, m) = (pos, m(pos $:= Some Oc))" |
+ "next_tape W0 (pos, m) = (pos, m(pos f\<mapsto> Bk))" |
+ "next_tape W1 (pos, m) = (pos, m(pos f\<mapsto> Oc))" |
"next_tape L (pos, m) = (pos - 1, m)" |
"next_tape R (pos, m) = (pos + 1, m)"
fun tstep :: "tconf \<Rightarrow> tconf"
where "tstep (faults, prog, pc, pos, m) =
- (case (prog $ pc) of
+ (case (prog f! pc) of
Some ((action0, pc0), (action1, pc1)) \<Rightarrow>
- case (m $ pos) of
+ case (m f! pos) of
+ Some Bk \<Rightarrow> (faults, prog, pc0, next_tape action0 (pos, m)) |
+ Some Oc \<Rightarrow> (faults, prog, pc1, next_tape action1 (pos, m)) |
+ None \<Rightarrow> (faults + 1, prog, pc, pos, m)
+ | None \<Rightarrow> (faults + 1, prog, pc, pos, m))"
+
+
+fun tstep :: "tconf \<Rightarrow> tconf"
+ where "tstep (faults, prog, pc, pos, m) =
+ (case (prog f! pc) of
+ Some ((action0, pc0), (action1, pc1)) \<Rightarrow>
+ case (m f! pos) of
Some Bk \<Rightarrow> (faults, prog, pc0, next_tape action0 (pos, m)) |
Some Oc \<Rightarrow> (faults, prog, pc1, next_tape action1 (pos, m)) |
None \<Rightarrow> (faults + 1, prog, pc, pos, m)
@@ -88,19 +99,19 @@
lemma tstep_splits:
"(P (tstep s)) = ((\<forall> faults prog pc pos m action0 pc0 action1 pc1.
s = (faults, prog, pc, pos, m) \<longrightarrow>
- prog $ pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow>
- m $ pos = Some Bk \<longrightarrow> P (faults, prog, pc0, next_tape action0 (pos, m))) \<and>
+ prog f! pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow>
+ m f! pos = Some Bk \<longrightarrow> P (faults, prog, pc0, next_tape action0 (pos, m))) \<and>
(\<forall> faults prog pc pos m action0 pc0 action1 pc1.
s = (faults, prog, pc, pos, m) \<longrightarrow>
- prog $ pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow>
- m $ pos = Some Oc \<longrightarrow> P (faults, prog, pc1, next_tape action1 (pos, m))) \<and>
+ prog f! pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow>
+ m f! pos = Some Oc \<longrightarrow> P (faults, prog, pc1, next_tape action1 (pos, m))) \<and>
(\<forall> faults prog pc pos m action0 pc0 action1 pc1.
s = (faults, prog, pc, pos, m) \<longrightarrow>
- prog $ pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow>
- m $ pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and>
+ prog f! pc = Some ((action0, pc0), (action1, pc1)) \<longrightarrow>
+ m f! pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and>
(\<forall> faults prog pc pos m .
s = (faults, prog, pc, pos, m) \<longrightarrow>
- prog $ pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m))
+ prog f! pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m))
)"
by (cases s) (auto split: option.splits Block.splits)
@@ -111,9 +122,9 @@
| TPos int (* head of TM is at position int *)
| TFaults nat (* there are nat faults *)
-definition "tprog_set prog = {TC i inst | i inst. prog $ i = Some inst}"
+definition "tprog_set prog = {TC i inst | i inst. prog f! i = Some inst}"
definition "tpc_set pc = {TAt pc}"
-definition "tmem_set m = {TM i n | i n. m $ i = Some n}"
+definition "tmem_set m = {TM i n | i n. m f! i = Some n}"
definition "tpos_set pos = {TPos pos}"
definition "tfaults_set faults = {TFaults faults}"
@@ -170,8 +181,8 @@
primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert"
where
- "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) ** <(j = i + 1)>)" |
- "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') ** (tassemble_to p2 j' j))" |
+ "tassemble_to (TInstr ai) i j = (sg ({TC i ai}) \<and>* <(j = i + 1)>)" |
+ "tassemble_to (TSeq p1 p2) i j = (EXS j'. (tassemble_to p1 i j') \<and>* (tassemble_to p2 j' j))" |
"tassemble_to (TLocal fp) i j = (EXS l. (tassemble_to (fp l) i j))" |
"tassemble_to (TLabel l) i j = <(i = j \<and> j = l)>"
@@ -405,21 +416,21 @@
by (unfold tpn_set_def, auto)
qed
-lemma codeD: "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))
- \<Longrightarrow> prog $ i = Some inst"
+lemma codeD: "(st i \<and>* sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))
+ \<Longrightarrow> prog f! i = Some inst"
proof -
- assume "(st i ** sg {TC i inst} ** r) (trset_of (ft, prog, i', pos, mem))"
+ assume "(st i \<and>* sg {TC i inst} \<and>* 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 f! 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 f! i = Some inst} \<union> {TAt i} \<union>
+ {TPos pos} \<union> {TM i n |i n. mem f! i = Some n} \<union> {TFaults ft}" by simp
thus ?thesis by auto
qed
@@ -1212,20 +1223,19 @@
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 f\<mapsto> 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)
-
+apply (metis the.simps the_lookup_fmap_upd the_lookup_fmap_upd_other)
+apply (metis the_lookup_fmap_upd_other)
+by (metis option.inject the_lookup_fmap_upd_other)
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 f\<mapsto> 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)"
@@ -1238,11 +1248,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 $:= Some v')) = {TM a v'} \<union> (tmem_set mem - {TM a v})"
+ have h2: "tmem_set (mem(a f\<mapsto> 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 $:= Some 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 f\<mapsto> 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
@@ -1250,13 +1260,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 f! 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 $:= Some v')) \<union> tprog_set x \<union> tpc_set y \<union> tpos_set z \<union> tfaults_set f =
+ show "tmem_set (mem(a f\<mapsto> 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
@@ -1281,11 +1291,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 f! 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' $:= Some Bk))" (is "?x = ?y")
+ "tm.run 1 (ft, prog, cs, i', mem) = (ft, prog, j, i', mem(i' f\<mapsto> Some Bk))" (is "?x = ?y")
apply(sep_frule psD)
apply(sep_frule stD)
apply(sep_frule memD, simp)
@@ -1331,12 +1341,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 f! 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' $:= Some Oc))" (is "?x = ?y")
+ (ft, prog, ?j, i', mem(i' f\<mapsto> Some Oc))" (is "?x = ?y")
apply(sep_frule psD)
apply(sep_frule stD)
apply(sep_frule memD, simp)
@@ -1383,7 +1393,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 f! 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:
@@ -1441,7 +1451,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 f! 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:
@@ -1497,12 +1507,12 @@
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 f! 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 f! pc = Some Oc"
apply(unfold one_def)
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
@@ -1510,6 +1520,14 @@
apply(sep_drule stD)
apply(unfold tm.run_def)
apply(auto)
+ apply(rule fmap_eqI)
+ apply(simp)
+ apply(subgoal_tac "p \<in> fdom mem")
+ apply(simp add: insert_absorb)
+ apply(simp add: fdomIff)
+ apply(rule_tac x="Some Oc" in exI)
+ apply(auto)[1]
+ apply(simp add: fun_eq_iff)
by (metis finfun_upd_triv)
from h k2
@@ -1584,12 +1602,12 @@
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 f! 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 f! pc = Some Bk"
apply(unfold zero_def)
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
@@ -1633,12 +1651,12 @@
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 f! 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 f! pc = Some Bk"
apply(unfold zero_def)
by(sep_drule memD, simp)
from h k1 k2 k3 have stp:
@@ -1712,12 +1730,12 @@
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 f! 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 f! 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")
@@ -1753,18 +1771,18 @@
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 f! 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 f! 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)
apply(unfold tm.run_def)
- apply(cases "mem $ pos")
+ apply(cases "mem f! pos")
apply(simp)
apply(cases v)
apply(auto)