--- a/src/HOL/TLA/Action.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Action.thy Fri Jun 26 15:55:44 2015 +0200
@@ -53,10 +53,10 @@
"_SqAct" == "CONST SqAct"
"_AnAct" == "CONST AnAct"
"_Enabled" == "CONST enabled"
- "w |= [A]_v" <= "_SqAct A v w"
- "w |= <A>_v" <= "_AnAct A v w"
- "s |= Enabled A" <= "_Enabled A s"
- "w |= unchanged f" <= "_unchanged f w"
+ "w \<Turnstile> [A]_v" <= "_SqAct A v w"
+ "w \<Turnstile> <A>_v" <= "_AnAct A v w"
+ "s \<Turnstile> Enabled A" <= "_Enabled A s"
+ "w \<Turnstile> unchanged f" <= "_unchanged f w"
axiomatization where
unl_before: "(ACT $v) (s,t) \<equiv> v s" and
@@ -161,8 +161,8 @@
done
lemma square_simulation:
- "\<And>f. \<lbrakk> \<turnstile> unchanged f & \<not>B \<longrightarrow> unchanged g;
- \<turnstile> A & \<not>unchanged g \<longrightarrow> B
+ "\<And>f. \<lbrakk> \<turnstile> unchanged f \<and> \<not>B \<longrightarrow> unchanged g;
+ \<turnstile> A \<and> \<not>unchanged g \<longrightarrow> B
\<rbrakk> \<Longrightarrow> \<turnstile> [A]_f \<longrightarrow> [B]_g"
apply clarsimp
apply (erule squareE)
@@ -210,29 +210,29 @@
apply (erule maj)
done
-lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F | G)"
+lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F \<or> G)"
by (auto elim!: enabled_mono)
-lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F | G)"
+lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F \<or> G)"
by (auto elim!: enabled_mono)
-lemma enabled_conj1: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled F"
+lemma enabled_conj1: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled F"
by (auto elim!: enabled_mono)
-lemma enabled_conj2: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled G"
+lemma enabled_conj2: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled G"
by (auto elim!: enabled_mono)
lemma enabled_conjE:
- "\<lbrakk> s \<Turnstile> Enabled (F & G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
+ "\<lbrakk> s \<Turnstile> Enabled (F \<and> G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
apply (frule enabled_conj1 [action_use])
apply (drule enabled_conj2 [action_use])
apply simp
done
-lemma enabled_disjD: "\<turnstile> Enabled (F | G) \<longrightarrow> Enabled F | Enabled G"
+lemma enabled_disjD: "\<turnstile> Enabled (F \<or> G) \<longrightarrow> Enabled F \<or> Enabled G"
by (auto simp add: enabled_def)
-lemma enabled_disj: "\<turnstile> Enabled (F | G) = (Enabled F | Enabled G)"
+lemma enabled_disj: "\<turnstile> Enabled (F \<or> G) = (Enabled F \<or> Enabled G)"
apply clarsimp
apply (rule iffI)
apply (erule enabled_disjD [action_use])
@@ -294,7 +294,7 @@
lemma
assumes "basevars (x,y,z)"
- shows "\<turnstile> x \<longrightarrow> Enabled ($x & (y$ = #False))"
+ shows "\<turnstile> x \<longrightarrow> Enabled ($x \<and> (y$ = #False))"
apply (enabled assms)
apply auto
done
--- a/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 15:55:44 2015 +0200
@@ -5,7 +5,7 @@
section {* A simple FIFO buffer (synchronous communication, interleaving) *}
theory Buffer
-imports TLA
+imports "../TLA"
begin
consts
@@ -22,16 +22,16 @@
defs
BInit_def: "BInit ic q oc == PRED q = #[]"
Enq_def: "Enq ic q oc == ACT (ic$ \<noteq> $ic)
- & (q$ = $q @ [ ic$ ])
- & (oc$ = $oc)"
+ \<and> (q$ = $q @ [ ic$ ])
+ \<and> (oc$ = $oc)"
Deq_def: "Deq ic q oc == ACT ($q \<noteq> #[])
- & (oc$ = hd< $q >)
- & (q$ = tl< $q >)
- & (ic$ = $ic)"
- Next_def: "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)"
+ \<and> (oc$ = hd< $q >)
+ \<and> (q$ = tl< $q >)
+ \<and> (ic$ = $ic)"
+ Next_def: "Next ic q oc == ACT (Enq ic q oc \<or> Deq ic q oc)"
IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc)
- & \<box>[Next ic q oc]_(ic,q,oc)
- & WF(Deq ic q oc)_(ic,q,oc)"
+ \<and> \<box>[Next ic q oc]_(ic,q,oc)
+ \<and> WF(Deq ic q oc)_(ic,q,oc)"
Buffer_def: "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
--- a/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 15:55:44 2015 +0200
@@ -29,17 +29,17 @@
(* the concatenation of the two buffers *)
qc_def: "PRED qc == PRED (q2 @ q1)" and
- DBInit_def: "DBInit == PRED (BInit inp q1 mid & BInit mid q2 out)" and
- DBEnq_def: "DBEnq == ACT Enq inp q1 mid & unchanged (q2,out)" and
- DBDeq_def: "DBDeq == ACT Deq mid q2 out & unchanged (inp,q1)" and
+ DBInit_def: "DBInit == PRED (BInit inp q1 mid \<and> BInit mid q2 out)" and
+ DBEnq_def: "DBEnq == ACT Enq inp q1 mid \<and> unchanged (q2,out)" and
+ DBDeq_def: "DBDeq == ACT Deq mid q2 out \<and> unchanged (inp,q1)" and
DBPass_def: "DBPass == ACT Deq inp q1 mid
- & (q2$ = $q2 @ [ mid$ ])
- & (out$ = $out)" and
- DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)" and
+ \<and> (q2$ = $q2 @ [ mid$ ])
+ \<and> (out$ = $out)" and
+ DBNext_def: "DBNext == ACT (DBEnq \<or> DBDeq \<or> DBPass)" and
DBuffer_def: "DBuffer == TEMP Init DBInit
- & \<box>[DBNext]_(inp,mid,out,q1,q2)
- & WF(DBDeq)_(inp,mid,out,q1,q2)
- & WF(DBPass)_(inp,mid,out,q1,q2)"
+ \<and> \<box>[DBNext]_(inp,mid,out,q1,q2)
+ \<and> WF(DBDeq)_(inp,mid,out,q1,q2)
+ \<and> WF(DBPass)_(inp,mid,out,q1,q2)"
declare qc_def [simp]
@@ -109,8 +109,8 @@
*)
(* Condition (1a) *)
-lemma DBFair_1a: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
- \<longrightarrow> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
+lemma DBFair_1a: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBPass)_(inp,mid,out,q1,q2)
+ \<longrightarrow> (qc \<noteq> #[] \<and> q2 = #[] \<leadsto> q2 \<noteq> #[])"
apply (rule WF1)
apply (force simp: db_defs)
apply (force simp: angle_def DBPass_def)
@@ -118,7 +118,7 @@
done
(* Condition (1) *)
-lemma DBFair_1: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
+lemma DBFair_1: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBPass)_(inp,mid,out,q1,q2)
\<longrightarrow> (Enabled (<Deq inp qc out>_(inp,qc,out)) \<leadsto> q2 \<noteq> #[])"
apply clarsimp
apply (rule leadsto_classical [temp_use])
@@ -130,7 +130,7 @@
done
(* Condition (2) *)
-lemma DBFair_2: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)
+lemma DBFair_2: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBDeq)_(inp,mid,out,q1,q2)
\<longrightarrow> (q2 \<noteq> #[] \<leadsto> DBDeq)"
apply (rule WF_leadsto)
apply (force simp: DBDeq_enabled [temp_use])
@@ -139,8 +139,8 @@
done
(* High-level fairness *)
-lemma DBFair: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
- & WF(DBDeq)_(inp,mid,out,q1,q2)
+lemma DBFair: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBPass)_(inp,mid,out,q1,q2)
+ \<and> WF(DBDeq)_(inp,mid,out,q1,q2)
\<longrightarrow> WF(Deq inp qc out)_(inp,qc,out)"
apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]
--- a/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 15:55:44 2015 +0200
@@ -5,7 +5,7 @@
section {* Lamport's "increment" example *}
theory Inc
-imports TLA
+imports "../TLA"
begin
(* program counter as an enumeration type *)
@@ -45,38 +45,38 @@
Inc_base: "basevars (x, y, sem, pc1, pc2)" and
(* definitions for high-level program *)
- InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0" and
- M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y" and
- M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x" and
- Phi_def: "Phi == TEMP Init InitPhi & \<box>[M1 | M2]_(x,y)
- & WF(M1)_(x,y) & WF(M2)_(x,y)" and
+ InitPhi_def: "InitPhi == PRED x = # 0 \<and> y = # 0" and
+ M1_def: "M1 == ACT x$ = Suc<$x> \<and> y$ = $y" and
+ M2_def: "M2 == ACT y$ = Suc<$y> \<and> x$ = $x" and
+ Phi_def: "Phi == TEMP Init InitPhi \<and> \<box>[M1 \<or> M2]_(x,y)
+ \<and> WF(M1)_(x,y) \<and> WF(M2)_(x,y)" and
(* definitions for low-level program *)
- InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a
- & x = # 0 & y = # 0 & sem = # 1" and
- alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
- & unchanged(x,y,pc2)" and
- alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
- & unchanged(x,y,pc1)" and
- beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
- & unchanged(y,sem,pc2)" and
- beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
- & unchanged(x,sem,pc1)" and
- gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
- & unchanged(x,y,pc2)" and
- gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
- & unchanged(x,y,pc1)" and
- N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)" and
- N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)" and
+ InitPsi_def: "InitPsi == PRED pc1 = #a \<and> pc2 = #a
+ \<and> x = # 0 \<and> y = # 0 \<and> sem = # 1" and
+ alpha1_def: "alpha1 == ACT $pc1 = #a \<and> pc1$ = #b \<and> $sem = Suc<sem$>
+ \<and> unchanged(x,y,pc2)" and
+ alpha2_def: "alpha2 == ACT $pc2 = #a \<and> pc2$ = #b \<and> $sem = Suc<sem$>
+ \<and> unchanged(x,y,pc1)" and
+ beta1_def: "beta1 == ACT $pc1 = #b \<and> pc1$ = #g \<and> x$ = Suc<$x>
+ \<and> unchanged(y,sem,pc2)" and
+ beta2_def: "beta2 == ACT $pc2 = #b \<and> pc2$ = #g \<and> y$ = Suc<$y>
+ \<and> unchanged(x,sem,pc1)" and
+ gamma1_def: "gamma1 == ACT $pc1 = #g \<and> pc1$ = #a \<and> sem$ = Suc<$sem>
+ \<and> unchanged(x,y,pc2)" and
+ gamma2_def: "gamma2 == ACT $pc2 = #g \<and> pc2$ = #a \<and> sem$ = Suc<$sem>
+ \<and> unchanged(x,y,pc1)" and
+ N1_def: "N1 == ACT (alpha1 \<or> beta1 \<or> gamma1)" and
+ N2_def: "N2 == ACT (alpha2 \<or> beta2 \<or> gamma2)" and
Psi_def: "Psi == TEMP Init InitPsi
- & \<box>[N1 | N2]_(x,y,sem,pc1,pc2)
- & SF(N1)_(x,y,sem,pc1,pc2)
- & SF(N2)_(x,y,sem,pc1,pc2)" and
+ \<and> \<box>[N1 \<or> N2]_(x,y,sem,pc1,pc2)
+ \<and> SF(N1)_(x,y,sem,pc1,pc2)
+ \<and> SF(N2)_(x,y,sem,pc1,pc2)" and
- PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
- PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
- PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
- PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
+ PsiInv1_def: "PsiInv1 == PRED sem = # 1 \<and> pc1 = #a \<and> pc2 = #a" and
+ PsiInv2_def: "PsiInv2 == PRED sem = # 0 \<and> pc1 = #a \<and> (pc2 = #b \<or> pc2 = #g)" and
+ PsiInv3_def: "PsiInv3 == PRED sem = # 0 \<and> pc2 = #a \<and> (pc1 = #b \<or> pc1 = #g)" and
+ PsiInv_def: "PsiInv == PRED (PsiInv1 \<or> PsiInv2 \<or> PsiInv3)"
lemmas PsiInv_defs = PsiInv_def PsiInv1_def PsiInv2_def PsiInv3_def
@@ -89,25 +89,25 @@
lemma PsiInv_Init: "\<turnstile> InitPsi \<longrightarrow> PsiInv"
by (auto simp: InitPsi_def PsiInv_defs)
-lemma PsiInv_alpha1: "\<turnstile> alpha1 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_alpha1: "\<turnstile> alpha1 \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: alpha1_def PsiInv_defs)
-lemma PsiInv_alpha2: "\<turnstile> alpha2 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_alpha2: "\<turnstile> alpha2 \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: alpha2_def PsiInv_defs)
-lemma PsiInv_beta1: "\<turnstile> beta1 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_beta1: "\<turnstile> beta1 \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: beta1_def PsiInv_defs)
-lemma PsiInv_beta2: "\<turnstile> beta2 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_beta2: "\<turnstile> beta2 \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: beta2_def PsiInv_defs)
-lemma PsiInv_gamma1: "\<turnstile> gamma1 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_gamma1: "\<turnstile> gamma1 \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: gamma1_def PsiInv_defs)
-lemma PsiInv_gamma2: "\<turnstile> gamma2 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_gamma2: "\<turnstile> gamma2 \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: gamma2_def PsiInv_defs)
-lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) \<and> $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: PsiInv_defs)
lemma PsiInv: "\<turnstile> Psi \<longrightarrow> \<box>PsiInv"
@@ -132,7 +132,7 @@
lemma Init_sim: "\<turnstile> Psi \<longrightarrow> Init InitPhi"
by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
-lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 | M2]_(x,y)"
+lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 \<or> M2]_(x,y)"
by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
@@ -154,7 +154,7 @@
the auxiliary lemmas are very similar.
*)
-lemma Stuck_at_b: "\<turnstile> \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) \<longrightarrow> stable(pc1 = #b)"
+lemma Stuck_at_b: "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not> beta1]_(x,y,sem,pc1,pc2) \<longrightarrow> stable(pc1 = #b)"
by (auto elim!: Stable squareE simp: Psi_defs)
lemma N1_enabled_at_g: "\<turnstile> pc1 = #g \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
@@ -166,7 +166,7 @@
done
lemma g1_leadsto_a1:
- "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True
+ "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box>#True
\<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)"
apply (rule SF1)
apply (tactic
@@ -188,7 +188,7 @@
done
lemma g2_leadsto_a2:
- "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
+ "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True
\<longrightarrow> (pc2 = #g \<leadsto> pc2 = #a)"
apply (rule SF1)
apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
@@ -207,7 +207,7 @@
done
lemma b2_leadsto_g2:
- "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
+ "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True
\<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)"
apply (rule SF1)
apply (tactic
@@ -220,8 +220,8 @@
(* Combine above lemmas: the second component will eventually reach pc2 = a *)
lemma N2_leadsto_a:
- "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
- \<longrightarrow> (pc2 = #a | pc2 = #b | pc2 = #g \<leadsto> pc2 = #a)"
+ "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True
+ \<longrightarrow> (pc2 = #a \<or> pc2 = #b \<or> pc2 = #g \<leadsto> pc2 = #a)"
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
apply (rule LatticeReflexivity [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -230,7 +230,7 @@
(* Get rid of disjunction on the left-hand side of \<leadsto> above. *)
lemma N2_live:
- "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)
+ "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2)
\<longrightarrow> \<diamond>(pc2 = #a)"
apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]])
apply (case_tac "pc2 (st1 sigma)")
@@ -240,7 +240,7 @@
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
lemma N1_enabled_at_both_a:
- "\<turnstile> pc2 = #a & (PsiInv & pc1 = #a) \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
+ "\<turnstile> pc2 = #a \<and> (PsiInv \<and> pc1 = #a) \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = alpha1 in enabled_mono)
apply (enabled Inc_base)
@@ -249,8 +249,8 @@
done
lemma a1_leadsto_b1:
- "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)
+ "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2))
+ \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)
\<longrightarrow> (pc1 = #a \<leadsto> pc1 = #b)"
apply (rule SF1)
apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
@@ -263,9 +263,9 @@
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
-lemma N1_leadsto_b: "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)
- \<longrightarrow> (pc1 = #b | pc1 = #g | pc1 = #a \<leadsto> pc1 = #b)"
+lemma N1_leadsto_b: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2))
+ \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)
+ \<longrightarrow> (pc1 = #b \<or> pc1 = #g \<or> pc1 = #a \<leadsto> pc1 = #b)"
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
apply (rule LatticeReflexivity [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -273,8 +273,8 @@
simp: split_box_conj)
done
-lemma N1_live: "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)
+lemma N1_live: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2))
+ \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)
\<longrightarrow> \<diamond>(pc1 = #b)"
apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]])
apply (case_tac "pc1 (st1 sigma)")
@@ -291,8 +291,8 @@
(* Now assemble the bits and pieces to prove that Psi is fair. *)
-lemma Fair_M1_lemma: "\<turnstile> \<box>($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & \<box>SF(N2)_(x,y,sem,pc1,pc2)
+lemma Fair_M1_lemma: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2)]_(x,y,sem,pc1,pc2))
+ \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box>SF(N2)_(x,y,sem,pc1,pc2)
\<longrightarrow> SF(M1)_(x,y)"
apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
(* action premises *)
--- a/src/HOL/TLA/Init.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Init.thy Fri Jun 26 15:55:44 2015 +0200
@@ -30,7 +30,7 @@
translations
"TEMP F" => "(F::behavior \<Rightarrow> _)"
"_Init" == "CONST Initial"
- "sigma |= Init F" <= "_Init F sigma"
+ "sigma \<Turnstile> Init F" <= "_Init F sigma"
defs
Init_def: "sigma \<Turnstile> Init F == (first_world sigma) \<Turnstile> F"
@@ -48,8 +48,8 @@
lemma Init_simps1 [int_rewrite]:
"\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)"
"\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)"
- "\<turnstile> (Init (P & Q)) = (Init P & Init Q)"
- "\<turnstile> (Init (P | Q)) = (Init P | Init Q)"
+ "\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)"
+ "\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)"
"\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))"
"\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
"\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
--- a/src/HOL/TLA/Intensional.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Jun 26 15:55:44 2015 +0200
@@ -43,8 +43,8 @@
"_constrain" :: "[lift, type] \<Rightarrow> lift" ("(_::_)" [4, 0] 3)
"" :: "lift \<Rightarrow> liftargs" ("_")
"_liftargs" :: "[lift, liftargs] \<Rightarrow> liftargs" ("_,/ _")
- "_Valid" :: "lift \<Rightarrow> bool" ("(|- _)" 5)
- "_holdsAt" :: "['a, lift] \<Rightarrow> bool" ("(_ |= _)" [100,10] 10)
+ "_Valid" :: "lift \<Rightarrow> bool" ("(\<turnstile> _)" 5)
+ "_holdsAt" :: "['a, lift] \<Rightarrow> bool" ("(_ \<Turnstile> _)" [100,10] 10)
(* Syntax for lifted expressions outside the scope of \<turnstile> or |= *)
"_LIFT" :: "lift \<Rightarrow> 'a" ("LIFT _")
@@ -57,11 +57,11 @@
(* concrete syntax for common infix functions: reuse same symbol *)
"_liftEqu" :: "[lift, lift] \<Rightarrow> lift" ("(_ =/ _)" [50,51] 50)
- "_liftNeq" :: "[lift, lift] \<Rightarrow> lift" ("(_ ~=/ _)" [50,51] 50)
- "_liftNot" :: "lift \<Rightarrow> lift" ("(~ _)" [40] 40)
- "_liftAnd" :: "[lift, lift] \<Rightarrow> lift" ("(_ &/ _)" [36,35] 35)
- "_liftOr" :: "[lift, lift] \<Rightarrow> lift" ("(_ |/ _)" [31,30] 30)
- "_liftImp" :: "[lift, lift] \<Rightarrow> lift" ("(_ -->/ _)" [26,25] 25)
+ "_liftNeq" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<noteq>/ _)" [50,51] 50)
+ "_liftNot" :: "lift \<Rightarrow> lift" ("(\<not> _)" [40] 40)
+ "_liftAnd" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<and>/ _)" [36,35] 35)
+ "_liftOr" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<or>/ _)" [31,30] 30)
+ "_liftImp" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<longrightarrow>/ _)" [26,25] 25)
"_liftIf" :: "[lift, lift, lift] \<Rightarrow> lift" ("(if (_)/ then (_)/ else (_))" 10)
"_liftPlus" :: "[lift, lift] \<Rightarrow> lift" ("(_ +/ _)" [66,65] 65)
"_liftMinus" :: "[lift, lift] \<Rightarrow> lift" ("(_ -/ _)" [66,65] 65)
@@ -69,9 +69,9 @@
"_liftDiv" :: "[lift, lift] \<Rightarrow> lift" ("(_ div _)" [71,70] 70)
"_liftMod" :: "[lift, lift] \<Rightarrow> lift" ("(_ mod _)" [71,70] 70)
"_liftLess" :: "[lift, lift] \<Rightarrow> lift" ("(_/ < _)" [50, 51] 50)
- "_liftLeq" :: "[lift, lift] \<Rightarrow> lift" ("(_/ <= _)" [50, 51] 50)
- "_liftMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ : _)" [50, 51] 50)
- "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ ~: _)" [50, 51] 50)
+ "_liftLeq" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<le> _)" [50, 51] 50)
+ "_liftMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<in> _)" [50, 51] 50)
+ "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<notin> _)" [50, 51] 50)
"_liftFinset" :: "liftargs \<Rightarrow> lift" ("{(_)}")
(** TODO: syntax for lifted collection / comprehension **)
"_liftPair" :: "[lift,liftargs] \<Rightarrow> lift" ("(1'(_,/ _'))")
@@ -81,12 +81,9 @@
"_liftList" :: "liftargs \<Rightarrow> lift" ("[(_)]")
(* Rigid quantification (syntax level) *)
- "_ARAll" :: "[idts, lift] \<Rightarrow> lift" ("(3! _./ _)" [0, 10] 10)
- "_AREx" :: "[idts, lift] \<Rightarrow> lift" ("(3? _./ _)" [0, 10] 10)
- "_AREx1" :: "[idts, lift] \<Rightarrow> lift" ("(3?! _./ _)" [0, 10] 10)
- "_RAll" :: "[idts, lift] \<Rightarrow> lift" ("(3ALL _./ _)" [0, 10] 10)
- "_REx" :: "[idts, lift] \<Rightarrow> lift" ("(3EX _./ _)" [0, 10] 10)
- "_REx1" :: "[idts, lift] \<Rightarrow> lift" ("(3EX! _./ _)" [0, 10] 10)
+ "_RAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>_./ _)" [0, 10] 10)
+ "_REx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>_./ _)" [0, 10] 10)
+ "_REx1" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>!_./ _)" [0, 10] 10)
translations
"_const" == "CONST const"
@@ -97,19 +94,16 @@
"_RAll x A" == "Rall x. A"
"_REx x A" == "Rex x. A"
"_REx1 x A" == "Rex! x. A"
- "_ARAll" => "_RAll"
- "_AREx" => "_REx"
- "_AREx1" => "_REx1"
- "w |= A" => "A w"
- "LIFT A" => "A::_=>_"
+ "w \<Turnstile> A" => "A w"
+ "LIFT A" => "A::_\<Rightarrow>_"
"_liftEqu" == "_lift2 (op =)"
"_liftNeq u v" == "_liftNot (_liftEqu u v)"
"_liftNot" == "_lift (CONST Not)"
- "_liftAnd" == "_lift2 (op &)"
- "_liftOr" == "_lift2 (op | )"
- "_liftImp" == "_lift2 (op -->)"
+ "_liftAnd" == "_lift2 (op \<and>)"
+ "_liftOr" == "_lift2 (op \<or>)"
+ "_liftImp" == "_lift2 (op \<longrightarrow>)"
"_liftIf" == "_lift3 (CONST If)"
"_liftPlus" == "_lift2 (op +)"
"_liftMinus" == "_lift2 (op -)"
@@ -117,8 +111,8 @@
"_liftDiv" == "_lift2 (op div)"
"_liftMod" == "_lift2 (op mod)"
"_liftLess" == "_lift2 (op <)"
- "_liftLeq" == "_lift2 (op <=)"
- "_liftMem" == "_lift2 (op :)"
+ "_liftLeq" == "_lift2 (op \<le>)"
+ "_liftMem" == "_lift2 (op \<in>)"
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)"
"_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)"
"_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
@@ -131,29 +125,14 @@
- "w |= ~A" <= "_liftNot A w"
- "w |= A & B" <= "_liftAnd A B w"
- "w |= A | B" <= "_liftOr A B w"
- "w |= A --> B" <= "_liftImp A B w"
- "w |= u = v" <= "_liftEqu u v w"
- "w |= ALL x. A" <= "_RAll x A w"
- "w |= EX x. A" <= "_REx x A w"
- "w |= EX! x. A" <= "_REx1 x A w"
-
-syntax (xsymbols)
- "_Valid" :: "lift \<Rightarrow> bool" ("(\<turnstile> _)" 5)
- "_holdsAt" :: "['a, lift] \<Rightarrow> bool" ("(_ \<Turnstile> _)" [100,10] 10)
- "_liftNeq" :: "[lift, lift] \<Rightarrow> lift" (infixl "\<noteq>" 50)
- "_liftNot" :: "lift \<Rightarrow> lift" ("\<not> _" [40] 40)
- "_liftAnd" :: "[lift, lift] \<Rightarrow> lift" (infixr "\<and>" 35)
- "_liftOr" :: "[lift, lift] \<Rightarrow> lift" (infixr "\<or>" 30)
- "_liftImp" :: "[lift, lift] \<Rightarrow> lift" (infixr "\<longrightarrow>" 25)
- "_RAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>_./ _)" [0, 10] 10)
- "_REx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>_./ _)" [0, 10] 10)
- "_REx1" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>!_./ _)" [0, 10] 10)
- "_liftLeq" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<le> _)" [50, 51] 50)
- "_liftMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<in> _)" [50, 51] 50)
- "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<notin> _)" [50, 51] 50)
+ "w \<Turnstile> \<not>A" <= "_liftNot A w"
+ "w \<Turnstile> A \<and> B" <= "_liftAnd A B w"
+ "w \<Turnstile> A \<or> B" <= "_liftOr A B w"
+ "w \<Turnstile> A \<longrightarrow> B" <= "_liftImp A B w"
+ "w \<Turnstile> u = v" <= "_liftEqu u v w"
+ "w \<Turnstile> \<forall>x. A" <= "_RAll x A w"
+ "w \<Turnstile> \<exists>x. A" <= "_REx x A w"
+ "w \<Turnstile> \<exists>!x. A" <= "_REx1 x A w"
defs
Valid_def: "\<turnstile> A == \<forall>w. w \<Turnstile> A"
@@ -164,7 +143,7 @@
unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
unl_Rall: "w \<Turnstile> \<forall>x. A x == \<forall>x. (w \<Turnstile> A x)"
- unl_Rex: "w \<Turnstile> \<exists>x. A x == \<exists> x. (w \<Turnstile> A x)"
+ unl_Rex: "w \<Turnstile> \<exists>x. A x == \<exists>x. (w \<Turnstile> A x)"
unl_Rex1: "w \<Turnstile> \<exists>!x. A x == \<exists>!x. (w \<Turnstile> A x)"
@@ -202,15 +181,15 @@
"\<turnstile> (#True \<longrightarrow> P) = P" "\<turnstile> (#False \<longrightarrow> P) = #True"
"\<turnstile> (P \<longrightarrow> #True) = #True" "\<turnstile> (P \<longrightarrow> P) = #True"
"\<turnstile> (P \<longrightarrow> #False) = (\<not>P)" "\<turnstile> (P \<longrightarrow> \<not>P) = (\<not>P)"
- "\<turnstile> (P & #True) = P" "\<turnstile> (#True & P) = P"
- "\<turnstile> (P & #False) = #False" "\<turnstile> (#False & P) = #False"
- "\<turnstile> (P & P) = P" "\<turnstile> (P & \<not>P) = #False" "\<turnstile> (\<not>P & P) = #False"
- "\<turnstile> (P | #True) = #True" "\<turnstile> (#True | P) = #True"
- "\<turnstile> (P | #False) = P" "\<turnstile> (#False | P) = P"
- "\<turnstile> (P | P) = P" "\<turnstile> (P | \<not>P) = #True" "\<turnstile> (\<not>P | P) = #True"
+ "\<turnstile> (P \<and> #True) = P" "\<turnstile> (#True \<and> P) = P"
+ "\<turnstile> (P \<and> #False) = #False" "\<turnstile> (#False \<and> P) = #False"
+ "\<turnstile> (P \<and> P) = P" "\<turnstile> (P \<and> \<not>P) = #False" "\<turnstile> (\<not>P \<and> P) = #False"
+ "\<turnstile> (P \<or> #True) = #True" "\<turnstile> (#True \<or> P) = #True"
+ "\<turnstile> (P \<or> #False) = P" "\<turnstile> (#False \<or> P) = P"
+ "\<turnstile> (P \<or> P) = P" "\<turnstile> (P \<or> \<not>P) = #True" "\<turnstile> (\<not>P \<or> P) = #True"
"\<turnstile> (\<forall>x. P) = P" "\<turnstile> (\<exists>x. P) = P"
"\<turnstile> (\<not>Q \<longrightarrow> \<not>P) = (P \<longrightarrow> Q)"
- "\<turnstile> (P|Q \<longrightarrow> R) = ((P\<longrightarrow>R)&(Q\<longrightarrow>R))"
+ "\<turnstile> (P\<or>Q \<longrightarrow> R) = ((P\<longrightarrow>R)\<and>(Q\<longrightarrow>R))"
apply (unfold Valid_def intensional_rews)
apply blast+
done
--- a/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 15:55:44 2015 +0200
@@ -16,50 +16,50 @@
definition
(* state predicates *)
MClkInit :: "mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> stpred"
- where "MClkInit rcv cst p = PRED (cst!p = #clkA & \<not>Calling rcv p)"
+ where "MClkInit rcv cst p = PRED (cst!p = #clkA \<and> \<not>Calling rcv p)"
definition
(* actions *)
MClkFwd :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkFwd send rcv cst p = ACT
$Calling send p
- & $(cst!p) = #clkA
- & Call rcv p MClkRelayArg<arg<send!p>>
- & (cst!p)$ = #clkB
- & unchanged (rtrner send!p)"
+ \<and> $(cst!p) = #clkA
+ \<and> Call rcv p MClkRelayArg<arg<send!p>>
+ \<and> (cst!p)$ = #clkB
+ \<and> unchanged (rtrner send!p)"
definition
MClkRetry :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkRetry send rcv cst p = ACT
$(cst!p) = #clkB
- & res<$(rcv!p)> = #RPCFailure
- & Call rcv p MClkRelayArg<arg<send!p>>
- & unchanged (cst!p, rtrner send!p)"
+ \<and> res<$(rcv!p)> = #RPCFailure
+ \<and> Call rcv p MClkRelayArg<arg<send!p>>
+ \<and> unchanged (cst!p, rtrner send!p)"
definition
MClkReply :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkReply send rcv cst p = ACT
\<not>$Calling rcv p
- & $(cst!p) = #clkB
- & Return send p MClkReplyVal<res<rcv!p>>
- & (cst!p)$ = #clkA
- & unchanged (caller rcv!p)"
+ \<and> $(cst!p) = #clkB
+ \<and> Return send p MClkReplyVal<res<rcv!p>>
+ \<and> (cst!p)$ = #clkA
+ \<and> unchanged (caller rcv!p)"
definition
MClkNext :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkNext send rcv cst p = ACT
( MClkFwd send rcv cst p
- | MClkRetry send rcv cst p
- | MClkReply send rcv cst p)"
+ \<or> MClkRetry send rcv cst p
+ \<or> MClkReply send rcv cst p)"
definition
(* temporal *)
MClkIPSpec :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> temporal"
where "MClkIPSpec send rcv cst p = TEMP
Init MClkInit rcv cst p
- & \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
- & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
- & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
+ \<and> \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
+ \<and> WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
+ \<and> SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
definition
MClkISpec :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> temporal"
@@ -73,7 +73,7 @@
(* The Clerk engages in an action for process p only if there is an outstanding,
unanswered call for that process.
*)
-lemma MClkidle: "\<turnstile> \<not>$Calling send p & $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
+lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
by (auto simp: Return_def MC_action_defs)
lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
@@ -83,7 +83,7 @@
(* Enabledness of actions *)
lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>
- \<turnstile> Calling send p & \<not>Calling rcv p & cst!p = #clkA
+ \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA
\<longrightarrow> Enabled (MClkFwd send rcv cst p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
@{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
@@ -98,7 +98,7 @@
by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use])
lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>
- \<turnstile> Calling send p & \<not>Calling rcv p & cst!p = #clkB
+ \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkB
\<longrightarrow> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
apply (tactic {* action_simp_tac @{context}
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
--- a/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 15:55:44 2015 +0200
@@ -55,79 +55,79 @@
PInit_def: "PInit rs p == PRED rs!p = #NotAResult"
RdRequest_def: "RdRequest ch p l == PRED
- Calling ch p & (arg<ch!p> = #(read l))"
+ Calling ch p \<and> (arg<ch!p> = #(read l))"
WrRequest_def: "WrRequest ch p l v == PRED
- Calling ch p & (arg<ch!p> = #(write l v))"
+ Calling ch p \<and> (arg<ch!p> = #(write l v))"
(* a read that doesn't raise BadArg *)
GoodRead_def: "GoodRead mm rs p l == ACT
- #l : #MemLoc & ((rs!p)$ = $(mm!l))"
+ #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
(* a read that raises BadArg *)
BadRead_def: "BadRead mm rs p l == ACT
- #l \<notin> #MemLoc & ((rs!p)$ = #BadArg)"
+ #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
(* the read action with l visible *)
ReadInner_def: "ReadInner ch mm rs p l == ACT
$(RdRequest ch p l)
- & (GoodRead mm rs p l | BadRead mm rs p l)
- & unchanged (rtrner ch ! p)"
+ \<and> (GoodRead mm rs p l \<or> BadRead mm rs p l)
+ \<and> unchanged (rtrner ch ! p)"
(* the read action with l quantified *)
Read_def: "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
(* similar definitions for the write action *)
GoodWrite_def: "GoodWrite mm rs p l v == ACT
- #l : #MemLoc & #v : #MemVal
- & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
+ #l \<in> #MemLoc \<and> #v \<in> #MemVal
+ \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
BadWrite_def: "BadWrite mm rs p l v == ACT
- \<not> (#l : #MemLoc & #v : #MemVal)
- & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
+ \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
+ \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
WriteInner_def: "WriteInner ch mm rs p l v == ACT
$(WrRequest ch p l v)
- & (GoodWrite mm rs p l v | BadWrite mm rs p l v)
- & unchanged (rtrner ch ! p)"
+ \<and> (GoodWrite mm rs p l v \<or> BadWrite mm rs p l v)
+ \<and> unchanged (rtrner ch ! p)"
Write_def: "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
(* the return action *)
MemReturn_def: "MemReturn ch rs p == ACT
( ($(rs!p) \<noteq> #NotAResult)
- & ((rs!p)$ = #NotAResult)
- & Return ch p (rs!p))"
+ \<and> ((rs!p)$ = #NotAResult)
+ \<and> Return ch p (rs!p))"
(* the failure action of the unreliable memory *)
MemFail_def: "MemFail ch rs p == ACT
$(Calling ch p)
- & ((rs!p)$ = #MemFailure)
- & unchanged (rtrner ch ! p)"
+ \<and> ((rs!p)$ = #MemFailure)
+ \<and> unchanged (rtrner ch ! p)"
(* next-state relations for reliable / unreliable memory *)
RNext_def: "RNext ch mm rs p == ACT
( Read ch mm rs p
- | (\<exists>l. Write ch mm rs p l)
- | MemReturn ch rs p)"
+ \<or> (\<exists>l. Write ch mm rs p l)
+ \<or> MemReturn ch rs p)"
UNext_def: "UNext ch mm rs p == ACT
- (RNext ch mm rs p | MemFail ch rs p)"
+ (RNext ch mm rs p \<or> MemFail ch rs p)"
RPSpec_def: "RPSpec ch mm rs p == TEMP
Init(PInit rs p)
- & \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
- & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
- & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+ \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+ \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+ \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
UPSpec_def: "UPSpec ch mm rs p == TEMP
Init(PInit rs p)
- & \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
- & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
- & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+ \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+ \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+ \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
MSpec_def: "MSpec ch mm rs l == TEMP
Init(MInit mm l)
- & \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
+ \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
IRSpec_def: "IRSpec ch mm rs == TEMP
(\<forall>p. RPSpec ch mm rs p)
- & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+ \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
IUSpec_def: "IUSpec ch mm rs == TEMP
(\<forall>p. UPSpec ch mm rs p)
- & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+ \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
RSpec_def: "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
USpec_def: "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
- MemInv_def: "MemInv mm l == PRED #l : #MemLoc \<longrightarrow> mm!l : #MemVal"
+ MemInv_def: "MemInv mm l == PRED #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
lemmas RM_action_defs =
MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
@@ -154,7 +154,7 @@
by (auto simp: MemInv_def intro!: necT [temp_use])
lemma MemoryInvariantAll:
- "\<turnstile> (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec ch mm rs l) \<longrightarrow> (\<forall>l. \<box>(MemInv mm l))"
+ "\<turnstile> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l) \<longrightarrow> (\<forall>l. \<box>(MemInv mm l))"
apply clarify
apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
done
@@ -173,7 +173,7 @@
by (force simp: MemReturn_def angle_def)
lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow>
- \<turnstile> Calling ch p & (rs!p \<noteq> #NotAResult)
+ \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult)
\<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
apply (tactic
{* action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
@@ -183,32 +183,32 @@
done
lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow>
- \<turnstile> Calling ch p & (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)"
+ \<turnstile> Calling ch p \<and> (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)"
apply (case_tac "l : MemLoc")
apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
intro!: exI elim!: base_enabled [temp_use])+
done
lemma WriteInner_enabled: "\<And>p. basevars (mm!l, rtrner ch ! p, rs!p) \<Longrightarrow>
- \<turnstile> Calling ch p & (arg<ch!p> = #(write l v))
+ \<turnstile> Calling ch p \<and> (arg<ch!p> = #(write l v))
\<longrightarrow> Enabled (WriteInner ch mm rs p l v)"
apply (case_tac "l:MemLoc & v:MemVal")
apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def
intro!: exI elim!: base_enabled [temp_use])+
done
-lemma ReadResult: "\<turnstile> Read ch mm rs p & (\<forall>l. $(MemInv mm l)) \<longrightarrow> (rs!p)` \<noteq> #NotAResult"
+lemma ReadResult: "\<turnstile> Read ch mm rs p \<and> (\<forall>l. $(MemInv mm l)) \<longrightarrow> (rs!p)` \<noteq> #NotAResult"
by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)
lemma WriteResult: "\<turnstile> Write ch mm rs p l \<longrightarrow> (rs!p)` \<noteq> #NotAResult"
by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)
-lemma ReturnNotReadWrite: "\<turnstile> (\<forall>l. $MemInv mm l) & MemReturn ch rs p
- \<longrightarrow> \<not> Read ch mm rs p & (\<forall>l. \<not> Write ch mm rs p l)"
+lemma ReturnNotReadWrite: "\<turnstile> (\<forall>l. $MemInv mm l) \<and> MemReturn ch rs p
+ \<longrightarrow> \<not> Read ch mm rs p \<and> (\<forall>l. \<not> Write ch mm rs p l)"
by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
-lemma RWRNext_enabled: "\<turnstile> (rs!p = #NotAResult) & (!l. MemInv mm l)
- & Enabled (Read ch mm rs p | (\<exists>l. Write ch mm rs p l))
+lemma RWRNext_enabled: "\<turnstile> (rs!p = #NotAResult) \<and> (\<forall>l. MemInv mm l)
+ \<and> Enabled (Read ch mm rs p \<or> (\<exists>l. Write ch mm rs p l))
\<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
by (force simp: RNext_def angle_def elim!: enabled_mono2
dest: ReadResult [temp_use] WriteResult [temp_use])
@@ -218,7 +218,7 @@
outstanding call for which no result has been produced.
*)
lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) \<Longrightarrow>
- \<turnstile> (rs!p = #NotAResult) & Calling ch p & (\<forall>l. MemInv mm l)
+ \<turnstile> (rs!p = #NotAResult) \<and> Calling ch p \<and> (\<forall>l. MemInv mm l)
\<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
apply (case_tac "arg (ch w p)")
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 15:55:44 2015 +0200
@@ -63,7 +63,7 @@
definition
(* the environment action *)
ENext :: "PrIds \<Rightarrow> action"
- where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
+ where "ENext p = ACT (\<exists>l. #l \<in> #MemLoc \<and> Call memCh p #(read l))"
definition
@@ -74,7 +74,7 @@
definition
HNext :: "histType \<Rightarrow> PrIds \<Rightarrow> action"
where "HNext rmhist p = ACT (rmhist!p)$ =
- (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
+ (if (MemReturn rmCh ires p \<or> RPCFail crCh rmCh rst p)
then #histB
else if (MClkReply memCh crCh cst p)
then #histA
@@ -83,7 +83,7 @@
definition
HistP :: "histType \<Rightarrow> PrIds \<Rightarrow> temporal"
where "HistP rmhist p = (TEMP Init HInit rmhist p
- & \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
+ \<and> \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
definition
Hist :: "histType \<Rightarrow> temporal"
@@ -92,40 +92,40 @@
definition
(* the implementation *)
IPImp :: "PrIds \<Rightarrow> temporal"
- where "IPImp p = (TEMP ( Init \<not>Calling memCh p & \<box>[ENext p]_(e p)
- & MClkIPSpec memCh crCh cst p
- & RPCIPSpec crCh rmCh rst p
- & RPSpec rmCh mm ires p
- & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
+ where "IPImp p = (TEMP ( Init \<not>Calling memCh p \<and> \<box>[ENext p]_(e p)
+ \<and> MClkIPSpec memCh crCh cst p
+ \<and> RPCIPSpec crCh rmCh rst p
+ \<and> RPSpec rmCh mm ires p
+ \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
definition
ImpInit :: "PrIds \<Rightarrow> stpred"
where "ImpInit p = PRED ( \<not>Calling memCh p
- & MClkInit crCh cst p
- & RPCInit rmCh rst p
- & PInit ires p)"
+ \<and> MClkInit crCh cst p
+ \<and> RPCInit rmCh rst p
+ \<and> PInit ires p)"
definition
ImpNext :: "PrIds \<Rightarrow> action"
where "ImpNext p = (ACT [ENext p]_(e p)
- & [MClkNext memCh crCh cst p]_(c p)
- & [RPCNext crCh rmCh rst p]_(r p)
- & [RNext rmCh mm ires p]_(m p))"
+ \<and> [MClkNext memCh crCh cst p]_(c p)
+ \<and> [RPCNext crCh rmCh rst p]_(r p)
+ \<and> [RNext rmCh mm ires p]_(m p))"
definition
ImpLive :: "PrIds \<Rightarrow> temporal"
where "ImpLive p = (TEMP WF(MClkFwd memCh crCh cst p)_(c p)
- & SF(MClkReply memCh crCh cst p)_(c p)
- & WF(RPCNext crCh rmCh rst p)_(r p)
- & WF(RNext rmCh mm ires p)_(m p)
- & WF(MemReturn rmCh ires p)_(m p))"
+ \<and> SF(MClkReply memCh crCh cst p)_(c p)
+ \<and> WF(RPCNext crCh rmCh rst p)_(r p)
+ \<and> WF(RNext rmCh mm ires p)_(m p)
+ \<and> WF(MemReturn rmCh ires p)_(m p))"
definition
Implementation :: "temporal"
- where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) & \<box>[ENext p]_(e p))
- & MClkISpec memCh crCh cst
- & RPCISpec crCh rmCh rst
- & IRSpec rmCh mm ires))"
+ where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) \<and> \<box>[ENext p]_(e p))
+ \<and> MClkISpec memCh crCh cst
+ \<and> RPCISpec crCh rmCh rst
+ \<and> IRSpec rmCh mm ires))"
definition
(* the predicate S describes the states of the implementation.
@@ -137,17 +137,17 @@
S :: "histType \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> mClkState \<Rightarrow> rpcState \<Rightarrow> histState \<Rightarrow> histState \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED
Calling memCh p = #ecalling
- & Calling crCh p = #ccalling
- & (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
- & (\<not> #ccalling & cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
- & Calling rmCh p = #rcalling
- & (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
- & (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult)
- & (\<not> #rcalling & rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>)
- & cst!p = #cs
- & rst!p = #rs
- & (rmhist!p = #hs1 | rmhist!p = #hs2)
- & MVNROKBA<ires!p>)"
+ \<and> Calling crCh p = #ccalling
+ \<and> (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
+ \<and> (\<not> #ccalling \<and> cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
+ \<and> Calling rmCh p = #rcalling
+ \<and> (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
+ \<and> (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult)
+ \<and> (\<not> #rcalling \<and> rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>)
+ \<and> cst!p = #cs
+ \<and> rst!p = #rs
+ \<and> (rmhist!p = #hs1 \<or> rmhist!p = #hs2)
+ \<and> MVNROKBA<ires!p>)"
definition
(* predicates S1 -- S6 define special instances of S *)
@@ -177,8 +177,8 @@
definition
(* The invariant asserts that the system is always in one of S1 - S6, for every p *)
ImpInv :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
- where "ImpInv rmhist p = (PRED (S1 rmhist p | S2 rmhist p | S3 rmhist p
- | S4 rmhist p | S5 rmhist p | S6 rmhist p))"
+ where "ImpInv rmhist p = (PRED (S1 rmhist p \<or> S2 rmhist p \<or> S3 rmhist p
+ \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p))"
definition
resbar :: "histType \<Rightarrow> resType" (* refinement mapping *)
@@ -241,9 +241,9 @@
section "History variable"
-lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
+lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) \<and> \<box>(\<forall>p. ImpNext p)
\<longrightarrow> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
- & \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
+ \<and> \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
apply clarsimp
apply (rule historyI)
apply assumption+
@@ -299,21 +299,21 @@
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
*)
-lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p & \<not>S1 rmhist p"
+lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p \<and> \<not>S1 rmhist p"
by (auto simp: S_def S1_def S2_def)
-lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
+lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def)
-lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p"
+lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p \<and> \<not>S3 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def)
-lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
- & \<not>S3 rmhist p & \<not>S4 rmhist p"
+lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p
+ \<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
-lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
- & \<not>S3 rmhist p & \<not>S4 rmhist p & \<not>S5 rmhist p"
+lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p
+ \<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p \<and> \<not>S5 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
@@ -331,24 +331,24 @@
(* ------------------------------ State S1 ---------------------------------------- *)
-lemma S1Env: "\<turnstile> ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p)
+lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
\<longrightarrow> (S2 rmhist p)$"
by (force simp: ENext_def Call_def c_def r_def m_def
caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
-lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: MClkidle [temp_use] simp: S_def S1_def)
-lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: RPCidle [temp_use] simp: S_def S1_def)
-lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: Memoryidle [temp_use] simp: S_def S1_def)
-lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
+lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S1 rmhist p)
\<longrightarrow> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
@@ -357,26 +357,26 @@
(* ------------------------------ State S2 ---------------------------------------- *)
-lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
-lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
+lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
-lemma S2Forward: "\<turnstile> $(S2 rmhist p) & MClkFwd memCh crCh cst p
- & unchanged (e p, r p, m p, rmhist!p)
+lemma S2Forward: "\<turnstile> $(S2 rmhist p) \<and> MClkFwd memCh crCh cst p
+ \<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> (S3 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
@{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
@{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
-lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
-lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
+lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S2 rmhist p)
\<longrightarrow> unchanged (rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
@@ -384,61 +384,61 @@
(* ------------------------------ State S3 ---------------------------------------- *)
-lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
-lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
lemma S3LegalRcvArg: "\<turnstile> S3 rmhist p \<longrightarrow> IsLegalRcvArg<arg<crCh!p>>"
by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
-lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S3 rmhist p)
- \<longrightarrow> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S3 rmhist p)
+ \<longrightarrow> RPCFwd crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
apply clarsimp
apply (frule S3LegalRcvArg [action_use])
apply (auto simp: RPCNext_def RPCReject_def RPCReply_def S_def S3_def)
done
-lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
- & unchanged (e p, c p, m p)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p \<and> HNext rmhist p \<and> $(S3 rmhist p)
+ \<and> unchanged (e p, c p, m p)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
@{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
@{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
@{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
- & unchanged (e p, c p, m p)
+lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S3 rmhist p) \<and> HNext rmhist p
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
@{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
@{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
@{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
-lemma S3Hist: "\<turnstile> HNext rmhist p & $(S3 rmhist p) & unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
+lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
Return_def r_def rtrner_def S_def S3_def Calling_def)
(* ------------------------------ State S4 ---------------------------------------- *)
-lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
-lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
-lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] dest!: RPCbusy [temp_use] simp: S_def S4_def)
-lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & HNext rmhist p & $(MemInv mm l)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+ \<and> HNext rmhist p \<and> $(MemInv mm l)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
@{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
@{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
@@ -446,68 +446,68 @@
@{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
-lemma S4Read: "\<turnstile> Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & HNext rmhist p & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4Read: "\<turnstile> Read rmCh mm ires p \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+ \<and> HNext rmhist p \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (auto simp: Read_def dest!: S4ReadInner [temp_use])
-lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) \<and> HNext rmhist p
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
@{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
@{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
@{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S4Write: "\<turnstile> Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & (HNext rmhist p)
- \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4Write: "\<turnstile> Write rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+ \<and> (HNext rmhist p)
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (auto simp: Write_def dest!: S4WriteInner [temp_use])
-lemma WriteS4: "\<turnstile> $ImpInv rmhist p & Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
+lemma WriteS4: "\<turnstile> $ImpInv rmhist p \<and> Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
by (auto simp: Write_def WriteInner_def ImpInv_def
WrRequest_def S_def S1_def S2_def S3_def S4_def S5_def S6_def)
-lemma S4Return: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
- & HNext rmhist p
+lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
+ \<and> HNext rmhist p
\<longrightarrow> (S5 rmhist p)$"
by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
-lemma S4Hist: "\<turnstile> HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
+lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
Return_def m_def rtrner_def S_def S4_def Calling_def)
(* ------------------------------ State S5 ---------------------------------------- *)
-lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
-lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
-lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S5 rmhist p)
- \<longrightarrow> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S5 rmhist p)
+ \<longrightarrow> RPCReply crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
-lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
+lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
@{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
+lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
@{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
-lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
+lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> $(S5 rmhist p)
\<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
@@ -515,36 +515,36 @@
(* ------------------------------ State S6 ---------------------------------------- *)
-lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
-lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S6 rmhist p)
- \<longrightarrow> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
+lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S6 rmhist p)
+ \<longrightarrow> MClkRetry memCh crCh cst p \<or> MClkReply memCh crCh cst p"
by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
-lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
- & unchanged (e p,r p,m p)
- \<longrightarrow> (S3 rmhist p)$ & unchanged (rmhist!p)"
+lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
+ \<and> unchanged (e p,r p,m p)
+ \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
@{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
- & unchanged (e p,r p,m p)
+lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
+ \<and> unchanged (e p,r p,m p)
\<longrightarrow> (S1 rmhist p)$"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
@{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
-lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p \<longrightarrow> unchanged (r p)"
+lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $S6 rmhist p \<longrightarrow> unchanged (r p)"
by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
-lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
-lemma S6Hist: "\<turnstile> HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
+lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
@@ -554,7 +554,7 @@
(* ========== Step 1.1 ================================================= *)
(* The implementation's initial condition implies the state predicate S1 *)
-lemma Step1_1: "\<turnstile> ImpInit p & HInit rmhist p \<longrightarrow> S1 rmhist p"
+lemma Step1_1: "\<turnstile> ImpInit p \<and> HInit rmhist p \<longrightarrow> S1 rmhist p"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: MVNROKBA_def
MClkInit_def RPCInit_def PInit_def HInit_def ImpInit_def S_def S1_def)
@@ -562,9 +562,9 @@
(* ========== Step 1.2 ================================================== *)
(* Figure 16 is a predicate-action diagram for the implementation. *)
-lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p
- \<longrightarrow> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
+lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S1 rmhist p
+ \<longrightarrow> (S2 rmhist p)$ \<and> ENext p \<and> unchanged (c p, r p, m p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context})
[@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
@@ -572,10 +572,10 @@
apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
done
-lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
- \<longrightarrow> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
- & unchanged (e p, r p, m p, rmhist!p)"
+lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S2 rmhist p
+ \<longrightarrow> (S3 rmhist p)$ \<and> MClkFwd memCh crCh cst p
+ \<and> unchanged (e p, r p, m p, rmhist!p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context})
[@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
@@ -583,10 +583,10 @@
apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
done
-lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
- \<longrightarrow> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
- | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
+lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S3 rmhist p
+ \<longrightarrow> ((S4 rmhist p)$ \<and> RPCFwd crCh rmCh rst p \<and> unchanged (e p, c p, m p, rmhist!p))
+ \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{context} []
@@ -595,12 +595,12 @@
apply (auto dest!: S3Hist [temp_use])
done
-lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p)
- & $S4 rmhist p & (\<forall>l. $(MemInv mm l))
- \<longrightarrow> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
- | ((S4 rmhist p)$ & (\<exists>l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
- | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
+lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p)
+ \<and> $S4 rmhist p \<and> (\<forall>l. $(MemInv mm l))
+ \<longrightarrow> ((S4 rmhist p)$ \<and> Read rmCh mm ires p \<and> unchanged (e p, c p, r p, rmhist!p))
+ \<or> ((S4 rmhist p)$ \<and> (\<exists>l. Write rmCh mm ires p l) \<and> unchanged (e p, c p, r p, rmhist!p))
+ \<or> ((S5 rmhist p)$ \<and> MemReturn rmCh ires p \<and> unchanged (e p, c p, r p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
@@ -609,10 +609,10 @@
apply (auto dest!: S4Hist [temp_use])
done
-lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
- \<longrightarrow> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
- | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
+lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S5 rmhist p
+ \<longrightarrow> ((S6 rmhist p)$ \<and> RPCReply crCh rmCh rst p \<and> unchanged (e p, c p, m p))
+ \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
@@ -620,10 +620,10 @@
apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
done
-lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
- \<longrightarrow> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
- | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
+lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+ \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S6 rmhist p
+ \<longrightarrow> ((S1 rmhist p)$ \<and> MClkReply memCh crCh cst p \<and> unchanged (e p, r p, m p))
+ \<or> ((S3 rmhist p)$ \<and> MClkRetry memCh crCh cst p \<and> unchanged (e p,r p,m p,rmhist!p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
apply (tactic {* action_simp_tac @{context} []
@@ -648,20 +648,20 @@
section "Step simulation (Step 1.4)"
-lemma Step1_4_1: "\<turnstile> ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
+lemma Step1_4_1: "\<turnstile> ENext p \<and> $S1 rmhist p \<and> (S2 rmhist p)$ \<and> unchanged (c p, r p, m p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def)
-lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
- & unchanged (e p, r p, m p, rmhist!p)
+lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p \<and> $S2 rmhist p \<and> (S3 rmhist p)$
+ \<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
by (tactic {* action_simp_tac
(@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
@{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
-lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, m p, rmhist!p)
+lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p \<and> $S3 rmhist p \<and> (S4 rmhist p)$
+ \<and> unchanged (e p, c p, m p, rmhist!p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S3_excl [temp_use] S4_excl [temp_use])+
@@ -669,8 +669,8 @@
@{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
done
-lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
- & unchanged (e p, c p, m p)
+lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S3 rmhist p \<and> (S6 rmhist p)$
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
@@ -679,8 +679,8 @@
apply (auto simp: Return_def)
done
-lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
- & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l
+lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
+ \<and> unchanged (e p, c p, r p, rmhist!p) \<and> $MemInv mm l
\<longrightarrow> ReadInner memCh mm (resbar rmhist) p l"
apply clarsimp
apply (drule S4_excl [temp_use])+
@@ -693,13 +693,13 @@
[] [@{thm impE}, @{thm MemValNotAResultE}]) *})
done
-lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, r p, rmhist!p) & (\<forall>l. $(MemInv mm l))
+lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p \<and> $S4 rmhist p \<and> (S4 rmhist p)$
+ \<and> unchanged (e p, c p, r p, rmhist!p) \<and> (\<forall>l. $(MemInv mm l))
\<longrightarrow> Read memCh mm (resbar rmhist) p"
by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
-lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
- & unchanged (e p, c p, r p, rmhist!p)
+lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> WriteInner rmCh mm ires p l v
+ \<and> unchanged (e p, c p, r p, rmhist!p)
\<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v"
apply clarsimp
apply (drule S4_excl [temp_use])+
@@ -712,13 +712,13 @@
@{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
done
-lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, r p, rmhist!p)
+lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l \<and> $S4 rmhist p \<and> (S4 rmhist p)$
+ \<and> unchanged (e p, c p, r p, rmhist!p)
\<longrightarrow> Write memCh mm (resbar rmhist) p l"
by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
-lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
- & unchanged (e p, c p, r p)
+lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> (S5 rmhist p)$
+ \<and> unchanged (e p, c p, r p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
@@ -727,8 +727,8 @@
apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
done
-lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
- & unchanged (e p, c p, m p)
+lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S5_excl [temp_use] S6_excl [temp_use])+
@@ -736,8 +736,8 @@
apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
done
-lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
- & unchanged (e p, c p, m p)
+lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
+ \<and> unchanged (e p, c p, m p)
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
@@ -745,8 +745,8 @@
apply (auto simp: S5_def S_def)
done
-lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
- & unchanged (e p, r p, m p)
+lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p \<and> $S6 rmhist p \<and> (S1 rmhist p)$
+ \<and> unchanged (e p, r p, m p)
\<longrightarrow> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
@@ -758,8 +758,8 @@
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
done
-lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
- & unchanged (e p, r p, m p, rmhist!p)
+lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p \<and> $S6 rmhist p \<and> (S3 rmhist p)$
+ \<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S3_excl [temp_use])+
@@ -825,7 +825,7 @@
(* turn into (unsafe, looping!) introduction rule *)
lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
-lemma S1safe: "\<turnstile> $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S1safe: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -833,7 +833,7 @@
apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
done
-lemma S2safe: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S2safe: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -841,7 +841,7 @@
apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
done
-lemma S3safe: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S3safe: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -849,8 +849,8 @@
apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
done
-lemma S4safe: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $(MemInv mm l))
+lemma S4safe: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $(MemInv mm l))
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -859,7 +859,7 @@
dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
done
-lemma S5safe: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S5safe: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -867,7 +867,7 @@
apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
done
-lemma S6safe: "\<turnstile> $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S6safe: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -889,8 +889,8 @@
(* ------------------------------ State S1 ------------------------------ *)
-lemma S1_successors: "\<turnstile> $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S1 rmhist p)$ | (S2 rmhist p)$"
+lemma S1_successors: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S1 rmhist p)$ \<or> (S2 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_1 [temp_use])
done
@@ -923,18 +923,18 @@
(* ------------------------------ State S2 ------------------------------ *)
-lemma S2_successors: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S2 rmhist p)$ | (S3 rmhist p)$"
+lemma S2_successors: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S2 rmhist p)$ \<or> (S3 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_2 [temp_use])
done
-lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <MClkFwd memCh crCh cst p>_(c p)
+lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <MClkFwd memCh crCh cst p>_(c p)
\<longrightarrow> (S3 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
-lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use])
apply (cut_tac MI_base)
@@ -942,26 +942,26 @@
apply (simp_all add: S_def S2_def)
done
-lemma S2_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & WF(MClkFwd memCh crCh cst p)_(c p)
+lemma S2_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> WF(MClkFwd memCh crCh cst p)_(c p)
\<longrightarrow> (S2 rmhist p \<leadsto> S3 rmhist p)"
by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
(* ------------------------------ State S3 ------------------------------ *)
-lemma S3_successors: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
+lemma S3_successors: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S3 rmhist p)$ \<or> (S4 rmhist p \<or> S6 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_3 [temp_use])
done
-lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <RPCNext crCh rmCh rst p>_(r p)
- \<longrightarrow> (S4 rmhist p | S6 rmhist p)$"
+lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <RPCNext crCh rmCh rst p>_(r p)
+ \<longrightarrow> (S4 rmhist p \<or> S6 rmhist p)$"
apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
done
-lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
apply (cut_tac MI_base)
@@ -969,39 +969,39 @@
apply (simp_all add: S_def S3_def)
done
-lemma S3_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & WF(RPCNext crCh rmCh rst p)_(r p)
- \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
+lemma S3_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> WF(RPCNext crCh rmCh rst p)_(r p)
+ \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p)"
by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
(* ------------- State S4 -------------------------------------------------- *)
-lemma S4_successors: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p)$ | (S5 rmhist p)$"
+lemma S4_successors: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p)$ \<or> (S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
-lemma S4a_successors: "\<turnstile> $(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult)$
- | ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+lemma S4a_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult)$
+ \<or> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
-lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l))
- & <RNext rmCh mm ires p>_(m p)
- \<longrightarrow> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p = #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l))
+ \<and> <RNext rmCh mm ires p>_(m p)
+ \<longrightarrow> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$"
by (auto simp: angle_def
dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
-lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
+lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)
\<longrightarrow> $Enabled (<RNext rmCh mm ires p>_(m p))"
apply (auto simp: m_def intro!: RNext_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1009,30 +1009,30 @@
apply (simp add: S_def S4_def)
done
-lemma S4a_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
- \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult
- \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)"
+lemma S4a_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)) \<and> WF(RNext rmCh mm ires p)_(m p)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)"
by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
-lemma S4b_successors: "\<turnstile> $(S4 rmhist p & ires!p \<noteq> #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
- \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (S5 rmhist p)$"
+lemma S4b_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult)$ \<or> (S5 rmhist p)$"
apply (split_idle simp: m_def)
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
done
-lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
+lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)) \<and> <MemReturn rmCh ires p>_(m p)
\<longrightarrow> (S5 rmhist p)$"
by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
-lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p & ires!p \<noteq> #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (\<forall>l. $MemInv mm l)
+lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+ \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<and> (\<forall>l. $MemInv mm l)
\<longrightarrow> $Enabled (<MemReturn rmCh ires p>_(m p))"
apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1040,25 +1040,25 @@
apply (simp add: S_def S4_def)
done
-lemma S4b_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l))
- & WF(MemReturn rmCh ires p)_(m p)
- \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
+lemma S4b_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l))
+ \<and> WF(MemReturn rmCh ires p)_(m p)
+ \<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
(* ------------------------------ State S5 ------------------------------ *)
-lemma S5_successors: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S5 rmhist p)$ | (S6 rmhist p)$"
+lemma S5_successors: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S5 rmhist p)$ \<or> (S6 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_5 [temp_use])
done
-lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <RPCNext crCh rmCh rst p>_(r p)
+lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <RPCNext crCh rmCh rst p>_(r p)
\<longrightarrow> (S6 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
-lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
\<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1066,27 +1066,27 @@
apply (simp_all add: S_def S5_def)
done
-lemma S5_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & WF(RPCNext crCh rmCh rst p)_(r p)
+lemma S5_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> WF(RPCNext crCh rmCh rst p)_(r p)
\<longrightarrow> (S5 rmhist p \<leadsto> S6 rmhist p)"
by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
(* ------------------------------ State S6 ------------------------------ *)
-lemma S6_successors: "\<turnstile> $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- \<longrightarrow> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
+lemma S6_successors: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+ \<longrightarrow> (S1 rmhist p)$ \<or> (S3 rmhist p)$ \<or> (S6 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_6 [temp_use])
done
lemma S6MClkReply_successors:
- "\<turnstile> ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
- & <MClkReply memCh crCh cst p>_(c p)
+ "\<turnstile> ($S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ \<and> <MClkReply memCh crCh cst p>_(c p)
\<longrightarrow> (S1 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
lemma MClkReplyS6:
- "\<turnstile> $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
+ "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
@{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
@{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
@@ -1099,8 +1099,8 @@
addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
done
-lemma S6_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
- & SF(MClkReply memCh crCh cst p)_(c p) & \<box>\<diamond>(S6 rmhist p)
+lemma S6_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> $(ImpInv rmhist p))
+ \<and> SF(MClkReply memCh crCh cst p)_(c p) \<and> \<box>\<diamond>(S6 rmhist p)
\<longrightarrow> \<box>\<diamond>(S1 rmhist p)"
apply clarsimp
apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
@@ -1116,25 +1116,25 @@
(* --------------- aggregate leadsto properties----------------------------- *)
lemma S5S6LeadstoS6: "sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p
- \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
+ \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p \<or> S6 rmhist p) \<leadsto> S6 rmhist p"
by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
-lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p
+ \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p
\<leadsto> S6 rmhist p"
by (auto intro!: LatticeDisjunctionIntro [temp_use]
S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
-lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
- apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p & ires!p = #NotAResult) |
- (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p")
- apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
- (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p)" in
+ \<Longrightarrow> sigma \<Turnstile> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
+ apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p \<and> ires!p = #NotAResult) \<or>
+ (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p")
+ apply (erule_tac G = "PRED ((S4 rmhist p \<and> ires!p = #NotAResult) \<or>
+ (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p)" in
LatticeTransitivity [temp_use])
apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
apply (rule LatticeDisjunctionIntro [temp_use])
@@ -1144,12 +1144,12 @@
apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
done
-lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
+ \<Longrightarrow> sigma \<Turnstile> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (erule LatticeTriangle2 [temp_use])
apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1158,12 +1158,12 @@
done
lemma S2S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
- sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+ sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
- \<Longrightarrow> sigma \<Turnstile> S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
+ \<Longrightarrow> sigma \<Turnstile> S2 rmhist p \<or> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p
\<leadsto> S6 rmhist p"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -1175,10 +1175,10 @@
lemma NotS1LeadstoS6: "\<lbrakk> sigma \<Turnstile> \<box>ImpInv rmhist p;
sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
- sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
- \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
- sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+ sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+ \<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p;
+ sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
\<Longrightarrow> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p"
apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1207,8 +1207,8 @@
lemma Step1_5_1a: "\<turnstile> IPImp p \<longrightarrow> (\<forall>l. \<box>$MemInv mm l)"
by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
-lemma Step1_5_1b: "\<turnstile> Init(ImpInit p & HInit rmhist p) & \<box>(ImpNext p)
- & \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) & \<box>(\<forall>l. $MemInv mm l)
+lemma Step1_5_1b: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<and> \<box>(ImpNext p)
+ \<and> \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> \<box>(\<forall>l. $MemInv mm l)
\<longrightarrow> \<box>ImpInv rmhist p"
apply invariant
apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
@@ -1218,26 +1218,26 @@
done
(*** Initialization ***)
-lemma Step1_5_2a: "\<turnstile> Init(ImpInit p & HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
+lemma Step1_5_2a: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3 [temp_use])
(*** step simulation ***)
-lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
- & $ImpInv rmhist p & (\<forall>l. $MemInv mm l))
+lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+ \<and> $ImpInv rmhist p \<and> (\<forall>l. $MemInv mm l))
\<longrightarrow> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
by (auto simp: ImpInv_def elim!: STL4E [temp_use]
dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
S5safe [temp_use] S6safe [temp_use])
(*** Liveness ***)
-lemma GoodImpl: "\<turnstile> IPImp p & HistP rmhist p
- \<longrightarrow> Init(ImpInit p & HInit rmhist p)
- & \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p)
- & ImpLive p"
+lemma GoodImpl: "\<turnstile> IPImp p \<and> HistP rmhist p
+ \<longrightarrow> Init(ImpInit p \<and> HInit rmhist p)
+ \<and> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p)
+ \<and> ImpLive p"
apply clarsimp
- apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p & HInit rmhist p) & \<box> (ImpNext p) &
- \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) & \<box> (\<forall>l. $MemInv mm l)")
+ apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p \<and> HInit rmhist p) \<and> \<box> (ImpNext p) \<and>
+ \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) \<and> \<box> (\<forall>l. $MemInv mm l)")
apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
dest!: Step1_5_1b [temp_use])
apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
@@ -1251,9 +1251,9 @@
done
(* The implementation is infinitely often in state S1... *)
-lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l)
- & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l)
+ \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
\<longrightarrow> \<box>\<diamond>S1 rmhist p"
apply (clarsimp simp: ImpLive_def)
apply (rule S1Infinite)
@@ -1264,18 +1264,18 @@
done
(* ... and therefore satisfies the fairness requirements of the specification *)
-lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
-lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
\<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
(* QED step of step 1 *)
-lemma Step1: "\<turnstile> IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
+lemma Step1: "\<turnstile> IPImp p \<and> HistP rmhist p \<longrightarrow> UPSpec memCh mm (resbar rmhist) p"
by (auto simp: UPSpec_def split_box_conj [temp_use]
dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use]
Step1_5_3b [temp_use] Step1_5_3c [temp_use])
@@ -1283,10 +1283,10 @@
(* ------------------------------ Step 2 ------------------------------ *)
section "Step 2"
-lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l & ImpNext p
- & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
- & $ImpInv rmhist p
- \<longrightarrow> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
+lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l \<and> ImpNext p
+ \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+ \<and> $ImpInv rmhist p
+ \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (e p, c p, r p, rmhist!p)"
apply clarsimp
apply (drule WriteS4 [action_use])
apply assumption
@@ -1297,9 +1297,9 @@
done
lemma Step2_2: "\<turnstile> (\<forall>p. ImpNext p)
- & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & (\<forall>p. $ImpInv rmhist p)
- & [\<exists>q. Write rmCh mm ires q l]_(mm!l)
+ \<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> (\<forall>p. $ImpInv rmhist p)
+ \<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l)
\<longrightarrow> [\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
apply (auto intro!: squareCI elim!: squareE)
apply (assumption | rule exI Step1_4_4b [action_use])+
@@ -1308,13 +1308,13 @@
done
lemma Step2_lemma: "\<turnstile> \<box>( (\<forall>p. ImpNext p)
- & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & (\<forall>p. $ImpInv rmhist p)
- & [\<exists>q. Write rmCh mm ires q l]_(mm!l))
+ \<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+ \<and> (\<forall>p. $ImpInv rmhist p)
+ \<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l))
\<longrightarrow> \<box>[\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
-lemma Step2: "\<turnstile> #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
+lemma Step2: "\<turnstile> #l \<in> #MemLoc \<and> (\<forall>p. IPImp p \<and> HistP rmhist p)
\<longrightarrow> MSpec memCh mm (resbar rmhist) l"
apply (auto simp: MSpec_def)
apply (force simp: IPImp_def MSpec_def)
@@ -1334,7 +1334,7 @@
(* Implementation of internal specification by combination of implementation
and history variable with explicit refinement mapping
*)
-lemma Impl_IUSpec: "\<turnstile> Implementation & Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
+lemma Impl_IUSpec: "\<turnstile> Implementation \<and> Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def
RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use])
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 15:55:44 2015 +0200
@@ -63,14 +63,14 @@
Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p
- & (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
- & (arg<ch!p>$ = $v)"
+ \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
+ \<and> (arg<ch!p>$ = $v)"
Return_def: "(ACT Return ch p v) == ACT $Calling ch p
- & (rbit<ch!p>$ = $cbit<ch!p>)
- & (res<ch!p>$ = $v)"
+ \<and> (rbit<ch!p>$ = $cbit<ch!p>)
+ \<and> (res<ch!p>$ = $v)"
PLegalCaller_def: "PLegalCaller ch p == TEMP
Init(\<not> Calling ch p)
- & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+ \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
PLegalReturner_def: "PLegalReturner ch p == TEMP
\<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
--- a/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 15:55:44 2015 +0200
@@ -28,45 +28,45 @@
RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
defs
- RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
+ RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
RPCFwd_def: "RPCFwd send rcv rst p == ACT
$(Calling send p)
- & $(rst!p) = # rpcA
- & IsLegalRcvArg<arg<$(send!p)>>
- & Call rcv p RPCRelayArg<arg<send!p>>
- & (rst!p)$ = # rpcB
- & unchanged (rtrner send!p)"
+ \<and> $(rst!p) = # rpcA
+ \<and> IsLegalRcvArg<arg<$(send!p)>>
+ \<and> Call rcv p RPCRelayArg<arg<send!p>>
+ \<and> (rst!p)$ = # rpcB
+ \<and> unchanged (rtrner send!p)"
RPCReject_def: "RPCReject send rcv rst p == ACT
$(rst!p) = # rpcA
- & \<not>IsLegalRcvArg<arg<$(send!p)>>
- & Return send p #BadCall
- & unchanged ((rst!p), (caller rcv!p))"
+ \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
+ \<and> Return send p #BadCall
+ \<and> unchanged ((rst!p), (caller rcv!p))"
RPCFail_def: "RPCFail send rcv rst p == ACT
\<not>$(Calling rcv p)
- & Return send p #RPCFailure
- & (rst!p)$ = #rpcA
- & unchanged (caller rcv!p)"
+ \<and> Return send p #RPCFailure
+ \<and> (rst!p)$ = #rpcA
+ \<and> unchanged (caller rcv!p)"
RPCReply_def: "RPCReply send rcv rst p == ACT
\<not>$(Calling rcv p)
- & $(rst!p) = #rpcB
- & Return send p res<rcv!p>
- & (rst!p)$ = #rpcA
- & unchanged (caller rcv!p)"
+ \<and> $(rst!p) = #rpcB
+ \<and> Return send p res<rcv!p>
+ \<and> (rst!p)$ = #rpcA
+ \<and> unchanged (caller rcv!p)"
RPCNext_def: "RPCNext send rcv rst p == ACT
( RPCFwd send rcv rst p
- | RPCReject send rcv rst p
- | RPCFail send rcv rst p
- | RPCReply send rcv rst p)"
+ \<or> RPCReject send rcv rst p
+ \<or> RPCFail send rcv rst p
+ \<or> RPCReply send rcv rst p)"
RPCIPSpec_def: "RPCIPSpec send rcv rst p == TEMP
Init RPCInit rcv rst p
- & \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
- & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
+ \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+ \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
RPCISpec_def: "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
@@ -84,7 +84,7 @@
lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
by (auto simp: Return_def RPC_action_defs)
-lemma RPCbusy: "\<turnstile> $(Calling rcv p) & $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
+lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
by (auto simp: RPC_action_defs)
(* RPC failure actions are visible. *)
@@ -98,13 +98,13 @@
(* Enabledness of some actions *)
lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
- \<turnstile> \<not>Calling rcv p & Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
+ \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
@{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1 *})
lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
- \<turnstile> \<not>Calling rcv p & Calling send p & rst!p = #rpcB
+ \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB
\<longrightarrow> Enabled (RPCReply send rcv rst p)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
@{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
--- a/src/HOL/TLA/TLA.thy Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/TLA.thy Fri Jun 26 15:55:44 2015 +0200
@@ -24,15 +24,15 @@
(** concrete syntax **)
syntax
- "_Box" :: "lift \<Rightarrow> lift" ("([]_)" [40] 40)
- "_Dmd" :: "lift \<Rightarrow> lift" ("(<>_)" [40] 40)
- "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ ~> _)" [23,22] 22)
+ "_Box" :: "lift \<Rightarrow> lift" ("(\<box>_)" [40] 40)
+ "_Dmd" :: "lift \<Rightarrow> lift" ("(\<diamond>_)" [40] 40)
+ "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ \<leadsto> _)" [23,22] 22)
"_stable" :: "lift \<Rightarrow> lift" ("(stable/ _)")
"_WF" :: "[lift,lift] \<Rightarrow> lift" ("(WF'(_')'_(_))" [0,60] 55)
"_SF" :: "[lift,lift] \<Rightarrow> lift" ("(SF'(_')'_(_))" [0,60] 55)
- "_EEx" :: "[idts, lift] \<Rightarrow> lift" ("(3EEX _./ _)" [0,10] 10)
- "_AAll" :: "[idts, lift] \<Rightarrow> lift" ("(3AALL _./ _)" [0,10] 10)
+ "_EEx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
+ "_AAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
translations
"_Box" == "CONST Box"
@@ -44,21 +44,14 @@
"_EEx v A" == "Eex v. A"
"_AAll v A" == "Aall v. A"
- "sigma |= []F" <= "_Box F sigma"
- "sigma |= <>F" <= "_Dmd F sigma"
- "sigma |= F ~> G" <= "_leadsto F G sigma"
- "sigma |= stable P" <= "_stable P sigma"
- "sigma |= WF(A)_v" <= "_WF A v sigma"
- "sigma |= SF(A)_v" <= "_SF A v sigma"
- "sigma |= EEX x. F" <= "_EEx x F sigma"
- "sigma |= AALL x. F" <= "_AAll x F sigma"
-
-syntax (xsymbols)
- "_Box" :: "lift \<Rightarrow> lift" ("(\<box>_)" [40] 40)
- "_Dmd" :: "lift \<Rightarrow> lift" ("(\<diamond>_)" [40] 40)
- "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ \<leadsto> _)" [23,22] 22)
- "_EEx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
- "_AAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
+ "sigma \<Turnstile> \<box>F" <= "_Box F sigma"
+ "sigma \<Turnstile> \<diamond>F" <= "_Dmd F sigma"
+ "sigma \<Turnstile> F \<leadsto> G" <= "_leadsto F G sigma"
+ "sigma \<Turnstile> stable P" <= "_stable P sigma"
+ "sigma \<Turnstile> WF(A)_v" <= "_WF A v sigma"
+ "sigma \<Turnstile> SF(A)_v" <= "_SF A v sigma"
+ "sigma \<Turnstile> \<exists>\<exists>x. F" <= "_EEx x F sigma"
+ "sigma \<Turnstile> \<forall>\<forall>x. F" <= "_AAll x F sigma"
axiomatization where
(* Definitions of derived operators *)
@@ -77,11 +70,11 @@
normalT: "\<And>F G. \<turnstile> \<box>(F \<longrightarrow> G) \<longrightarrow> (\<box>F \<longrightarrow> \<box>G)" and (* polymorphic *)
reflT: "\<And>F. \<turnstile> \<box>F \<longrightarrow> F" and (* F::temporal *)
transT: "\<And>F. \<turnstile> \<box>F \<longrightarrow> \<box>\<box>F" and (* polymorphic *)
- linT: "\<And>F G. \<turnstile> \<diamond>F & \<diamond>G \<longrightarrow> (\<diamond>(F & \<diamond>G)) | (\<diamond>(G & \<diamond>F))" and
- discT: "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F & \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and
+ linT: "\<And>F G. \<turnstile> \<diamond>F \<and> \<diamond>G \<longrightarrow> (\<diamond>(F \<and> \<diamond>G)) \<or> (\<diamond>(G \<and> \<diamond>F))" and
+ discT: "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F \<and> \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and
primeI: "\<And>P. \<turnstile> \<box>P \<longrightarrow> Init P`" and
primeE: "\<And>P F. \<turnstile> \<box>(Init P \<longrightarrow> \<box>F) \<longrightarrow> Init P` \<longrightarrow> (F \<longrightarrow> \<box>F)" and
- indT: "\<And>P F. \<turnstile> \<box>(Init P & \<not>\<box>F \<longrightarrow> Init P` & F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and
+ indT: "\<And>P F. \<turnstile> \<box>(Init P \<and> \<not>\<box>F \<longrightarrow> Init P` \<and> F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and
allT: "\<And>F. \<turnstile> (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
axiomatization where
@@ -93,7 +86,7 @@
eexE: "\<lbrakk> sigma \<Turnstile> (\<exists>\<exists>x. F x); basevars vs;
(\<And>x. \<lbrakk> basevars (x, vs); sigma \<Turnstile> F x \<rbrakk> \<Longrightarrow> (G sigma)::bool)
\<rbrakk> \<Longrightarrow> G sigma" and
- history: "\<turnstile> \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)"
+ history: "\<turnstile> \<exists>\<exists>h. Init(h = ha) \<and> \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)"
(* Specialize intensional introduction/elimination rules for temporal formulas *)
@@ -255,9 +248,9 @@
by (erule (1) DmdImpl [temp_use])
(* ------------------------ STL5 ------------------------------------------- *)
-lemma STL5: "\<turnstile> (\<box>F & \<box>G) = (\<box>(F & G))"
+lemma STL5: "\<turnstile> (\<box>F \<and> \<box>G) = (\<box>(F \<and> G))"
apply auto
- apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F & G))")
+ apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F \<and> G))")
apply (erule normalT [temp_use])
apply (fastforce elim!: STL4E [temp_use])+
done
@@ -273,7 +266,7 @@
lemma box_conjE:
assumes "sigma \<Turnstile> \<box>F"
and "sigma \<Turnstile> \<box>G"
- and "sigma \<Turnstile> \<box>(F&G) \<Longrightarrow> PROP R"
+ and "sigma \<Turnstile> \<box>(F\<and>G) \<Longrightarrow> PROP R"
shows "PROP R"
by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
@@ -317,7 +310,7 @@
*)
lemmas all_box = allT [temp_unlift, symmetric]
-lemma DmdOr: "\<turnstile> (\<diamond>(F | G)) = (\<diamond>F | \<diamond>G)"
+lemma DmdOr: "\<turnstile> (\<diamond>(F \<or> G)) = (\<diamond>F \<or> \<diamond>G)"
apply (auto simp add: dmd_def split_box_conj [try_rewrite])
apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
done
@@ -327,7 +320,7 @@
lemmas ex_dmd = exT [temp_unlift, symmetric]
-lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F & \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
+lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F \<and> \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
apply (erule dup_boxE)
apply merge_box
apply (erule STL4E)
@@ -346,7 +339,7 @@
lemma InfImpl:
assumes 1: "sigma \<Turnstile> \<box>\<diamond>F"
and 2: "sigma \<Turnstile> \<box>G"
- and 3: "\<turnstile> F & G \<longrightarrow> H"
+ and 3: "\<turnstile> F \<and> G \<longrightarrow> H"
shows "sigma \<Turnstile> \<box>\<diamond>H"
apply (insert 1 2)
apply (erule_tac F = G in dup_boxE)
@@ -356,7 +349,7 @@
(* ------------------------ STL6 ------------------------------------------- *)
(* Used in the proof of STL6, but useful in itself. *)
-lemma BoxDmd: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(\<box>F & G)"
+lemma BoxDmd: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(\<box>F \<and> G)"
apply (unfold dmd_def)
apply clarsimp
apply (erule dup_boxE)
@@ -366,14 +359,14 @@
done
(* weaker than BoxDmd, but more polymorphic (and often just right) *)
-lemma BoxDmd_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(F & G)"
+lemma BoxDmd_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(F \<and> G)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
apply (fastforce elim!: notE STL4E [temp_use])
done
-lemma BoxDmd2_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(G & F)"
+lemma BoxDmd2_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(G \<and> F)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
@@ -383,13 +376,13 @@
lemma DmdImpldup:
assumes 1: "sigma \<Turnstile> \<box>A"
and 2: "sigma \<Turnstile> \<diamond>F"
- and 3: "\<turnstile> \<box>A & F \<longrightarrow> G"
+ and 3: "\<turnstile> \<box>A \<and> F \<longrightarrow> G"
shows "sigma \<Turnstile> \<diamond>G"
apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
apply (rule 3)
done
-lemma STL6: "\<turnstile> \<diamond>\<box>F & \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F & G)"
+lemma STL6: "\<turnstile> \<diamond>\<box>F \<and> \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F \<and> G)"
apply (auto simp: STL5 [temp_rewrite, symmetric])
apply (drule linT [temp_use])
apply assumption
@@ -444,7 +437,7 @@
lemma BoxDmdBox: "\<turnstile> (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
apply (auto dest!: STL2 [temp_use])
apply (rule ccontr)
- apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
+ apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F \<and> \<diamond>\<box>\<not>\<box>F")
apply (erule thin_rl)
apply auto
apply (drule STL6 [temp_use])
@@ -463,7 +456,7 @@
(* ------------------------ Miscellaneous ----------------------------------- *)
-lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F | \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F | G)"
+lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F \<or> \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F \<or> G)"
by (fastforce elim!: STL4E [temp_use])
(* "persistently implies infinitely often" *)
@@ -476,7 +469,7 @@
apply simp
done
-lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F & \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F & G)"
+lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F \<and> \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F \<and> G)"
apply clarsimp
apply (rule ccontr)
apply (unfold more_temp_simps2)
@@ -494,11 +487,11 @@
section "priming"
(* ------------------------ TLA2 ------------------------------------------- *)
-lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P & Init P`"
+lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P \<and> Init P`"
by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
(* Auxiliary lemma allows priming of boxed actions *)
-lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P & P$)"
+lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P \<and> P$)"
apply clarsimp
apply (erule dup_boxE)
apply (unfold boxInit_act)
@@ -507,7 +500,7 @@
done
lemma TLA2:
- assumes "\<turnstile> $P & P$ \<longrightarrow> A"
+ assumes "\<turnstile> $P \<and> P$ \<longrightarrow> A"
shows "\<turnstile> \<box>P \<longrightarrow> \<box>A"
apply clarsimp
apply (drule BoxPrime [temp_use])
@@ -515,7 +508,7 @@
elim!: STL4E [temp_use])
done
-lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P & P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
+lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P \<and> P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
by (erule (1) TLA2 [temp_use])
lemma DmdPrime: "\<turnstile> (\<diamond>P`) \<longrightarrow> (\<diamond>P)"
@@ -529,7 +522,7 @@
section "stable, invariant"
lemma ind_rule:
- "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P & \<not>\<box>F \<longrightarrow> Init(P`) & F) \<rbrakk>
+ "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P \<and> \<not>\<box>F \<longrightarrow> Init(P`) \<and> F) \<rbrakk>
\<Longrightarrow> sigma \<Turnstile> \<box>F"
apply (rule indT [temp_use])
apply (erule (2) STL4E)
@@ -552,12 +545,12 @@
done
lemma StableT:
- "\<And>P. \<turnstile> $P & A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
+ "\<And>P. \<turnstile> $P \<and> A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
apply (unfold stable_def)
apply (fastforce elim!: STL4E [temp_use])
done
-lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P & A --> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
+lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P \<and> A \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
by (erule (1) StableT [temp_use])
(* Generalization of INV1 *)
@@ -568,7 +561,7 @@
apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
done
-lemma DmdStable: "\<turnstile> (stable P) & \<diamond>P \<longrightarrow> \<diamond>\<box>P"
+lemma DmdStable: "\<turnstile> (stable P) \<and> \<diamond>P \<longrightarrow> \<diamond>\<box>P"
apply clarsimp
apply (rule DmdImpl2)
prefer 2
@@ -609,7 +602,7 @@
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
*}
-lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` | Q`) \<longrightarrow> (stable P) | \<diamond>Q"
+lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) \<longrightarrow> (stable P) \<or> \<diamond>Q"
apply (unfold dmd_def)
apply (clarsimp dest!: BoxPrime [temp_use])
apply merge_box
@@ -622,13 +615,13 @@
section "recursive expansions"
(* Recursive expansions of \<box> and \<diamond> for state predicates *)
-lemma BoxRec: "\<turnstile> (\<box>P) = (Init P & \<box>P`)"
+lemma BoxRec: "\<turnstile> (\<box>P) = (Init P \<and> \<box>P`)"
apply (auto intro!: STL2_gen [temp_use])
apply (fastforce elim!: TLA2E [temp_use])
apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
done
-lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P | \<diamond>P`)"
+lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P \<or> \<diamond>P`)"
apply (unfold dmd_def BoxRec [temp_rewrite])
apply (auto simp: Init_simps)
done
@@ -643,7 +636,7 @@
apply (rule DBImplBD [temp_use])
apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>P")
apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
- apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P & \<box>\<not>P`)")
+ apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P \<and> \<box>\<not>P`)")
apply (force simp: boxInit_stp [temp_use]
elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
@@ -651,7 +644,7 @@
done
lemma InfiniteEnsures:
- "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A & N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
+ "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A \<and> N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
apply (unfold InfinitePrime [temp_rewrite])
apply (rule InfImpl)
apply assumption+
@@ -661,12 +654,12 @@
section "fairness"
(* alternative definitions of fairness *)
-lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
+lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)"
apply (unfold WF_def dmd_def)
apply fastforce
done
-lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
+lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)"
apply (unfold SF_def dmd_def)
apply fastforce
done
@@ -702,7 +695,7 @@
section "\<leadsto>"
-lemma leadsto_init: "\<turnstile> (Init F) & (F \<leadsto> G) \<longrightarrow> \<diamond>G"
+lemma leadsto_init: "\<turnstile> (Init F) \<and> (F \<leadsto> G) \<longrightarrow> \<diamond>G"
apply (unfold leadsto_def)
apply (auto dest!: STL2 [temp_use])
done
@@ -723,7 +716,7 @@
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
done
-lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F & (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G"
+lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F \<and> (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G"
apply clarsimp
apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
apply (simp add: dmdInitD)
@@ -743,7 +736,7 @@
(* introduce an invariant into the proof of a leadsto assertion.
\<box>I \<longrightarrow> ((P \<leadsto> Q) = (P /\ I \<leadsto> Q))
*)
-lemma INV_leadsto: "\<turnstile> \<box>I & (P & I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
+lemma INV_leadsto: "\<turnstile> \<box>I \<and> (P \<and> I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4Edup)
@@ -751,12 +744,12 @@
apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
done
-lemma leadsto_classical: "\<turnstile> (Init F & \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)"
+lemma leadsto_classical: "\<turnstile> (Init F \<and> \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)"
apply (unfold leadsto_def dmd_def)
apply (force simp: Init_simps elim!: STL4E [temp_use])
done
-lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>~F)"
+lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>\<not>F)"
apply (unfold leadsto_def)
apply (simp add: boxNotInitD)
done
@@ -781,7 +774,7 @@
by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
lemma EnsuresLeadsto:
- assumes "\<turnstile> A & $P \<longrightarrow> Q`"
+ assumes "\<turnstile> A \<and> $P \<longrightarrow> Q`"
shows "\<turnstile> \<box>A \<longrightarrow> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply (clarsimp elim!: INV_leadsto [temp_use])
@@ -797,15 +790,15 @@
done
lemma ensures:
- assumes 1: "\<turnstile> $P & N \<longrightarrow> P` | Q`"
- and 2: "\<turnstile> ($P & N) & A \<longrightarrow> Q`"
- shows "\<turnstile> \<box>N & \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)"
+ assumes 1: "\<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`"
+ and 2: "\<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`"
+ shows "\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4Edup)
apply assumption
apply clarsimp
- apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` | Q`) ")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) ")
apply (drule unless [temp_use])
apply (clarsimp dest!: INV1 [temp_use])
apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
@@ -815,16 +808,16 @@
done
lemma ensures_simple:
- "\<lbrakk> \<turnstile> $P & N \<longrightarrow> P` | Q`;
- \<turnstile> ($P & N) & A \<longrightarrow> Q`
- \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N & \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)"
+ "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`;
+ \<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`
+ \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N \<and> \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)"
apply clarsimp
apply (erule (2) ensures [temp_use])
apply (force elim!: STL4E [temp_use])
done
lemma EnsuresInfinite:
- "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A & $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
+ "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A \<and> $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
apply (erule leadsto_infinite [temp_use])
apply (erule EnsuresLeadsto [temp_use])
apply assumption
@@ -839,7 +832,7 @@
apply (rule necT InitDmd_gen)+
done
-lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) & (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
+lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) \<and> (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule dup_boxE) (* \<box>\<box>(Init G \<longrightarrow> H) *)
@@ -852,47 +845,47 @@
apply (simp add: dmdInitD)
done
-lemma LatticeDisjunctionElim1: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
+lemma LatticeDisjunctionElim1: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
apply (unfold leadsto_def)
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunctionElim2: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
+lemma LatticeDisjunctionElim2: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
apply (unfold leadsto_def)
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) & (G \<leadsto> H) \<longrightarrow> (F | G \<leadsto> H)"
+lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) \<and> (G \<leadsto> H) \<longrightarrow> (F \<or> G \<leadsto> H)"
apply (unfold leadsto_def)
apply clarsimp
apply merge_box
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunction: "\<turnstile> (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
+lemma LatticeDisjunction: "\<turnstile> (F \<or> G \<leadsto> H) = ((F \<leadsto> H) \<and> (G \<leadsto> H))"
by (auto intro: LatticeDisjunctionIntro [temp_use]
LatticeDisjunctionElim1 [temp_use]
LatticeDisjunctionElim2 [temp_use])
-lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
+lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B \<or> C) \<and> (B \<leadsto> D) \<and> (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma \<Turnstile> (B | C) \<leadsto> D")
- apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
+ apply (subgoal_tac "sigma \<Turnstile> (B \<or> C) \<leadsto> D")
+ apply (erule_tac G = "LIFT (B \<or> C)" in LatticeTransitivity [temp_use])
apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
done
-lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D | B) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
+lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D \<or> B) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma \<Turnstile> (D | B) \<leadsto> D")
- apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use])
+ apply (subgoal_tac "sigma \<Turnstile> (D \<or> B) \<leadsto> D")
+ apply (erule_tac G = "LIFT (D \<or> B)" in LatticeTransitivity [temp_use])
apply assumption
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
done
-lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B | D) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
+lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B \<or> D) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma \<Turnstile> B | D \<leadsto> D")
- apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use])
+ apply (subgoal_tac "sigma \<Turnstile> B \<or> D \<leadsto> D")
+ apply (erule_tac G = "LIFT (B \<or> D)" in LatticeTransitivity [temp_use])
apply assumption
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
done
@@ -901,10 +894,10 @@
section "Fairness rules"
lemma WF1:
- "\<lbrakk> \<turnstile> $P & N \<longrightarrow> P` | Q`;
- \<turnstile> ($P & N) & <A>_v \<longrightarrow> Q`;
- \<turnstile> $P & N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk>
- \<Longrightarrow> \<turnstile> \<box>N & WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
+ "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`;
+ \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`;
+ \<turnstile> $P \<and> N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk>
+ \<Longrightarrow> \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
apply (clarsimp dest!: BoxWFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule (1) STL4Edup)
@@ -917,10 +910,10 @@
(* Sometimes easier to use; designed for action B rather than state predicate Q *)
lemma WF_leadsto:
- assumes 1: "\<turnstile> N & $P \<longrightarrow> $Enabled (<A>_v)"
- and 2: "\<turnstile> N & <A>_v \<longrightarrow> B"
- and 3: "\<turnstile> \<box>(N & [~A]_v) \<longrightarrow> stable P"
- shows "\<turnstile> \<box>N & WF(A)_v \<longrightarrow> (P \<leadsto> B)"
+ assumes 1: "\<turnstile> N \<and> $P \<longrightarrow> $Enabled (<A>_v)"
+ and 2: "\<turnstile> N \<and> <A>_v \<longrightarrow> B"
+ and 3: "\<turnstile> \<box>(N \<and> [\<not>A]_v) \<longrightarrow> stable P"
+ shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> B)"
apply (unfold leadsto_def)
apply (clarsimp dest!: BoxWFI [temp_use])
apply (erule (1) STL4Edup)
@@ -939,10 +932,10 @@
done
lemma SF1:
- "\<lbrakk> \<turnstile> $P & N \<longrightarrow> P` | Q`;
- \<turnstile> ($P & N) & <A>_v \<longrightarrow> Q`;
- \<turnstile> \<box>P & \<box>N & \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk>
- \<Longrightarrow> \<turnstile> \<box>N & SF(A)_v & \<box>F \<longrightarrow> (P \<leadsto> Q)"
+ "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`;
+ \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`;
+ \<turnstile> \<box>P \<and> \<box>N \<and> \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk>
+ \<Longrightarrow> \<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)"
apply (clarsimp dest!: BoxSFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule_tac F = F in dup_boxE)
@@ -957,11 +950,11 @@
done
lemma WF2:
- assumes 1: "\<turnstile> N & <B>_f \<longrightarrow> <M>_g"
- and 2: "\<turnstile> $P & P` & <N & A>_f \<longrightarrow> B"
- and 3: "\<turnstile> P & Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
- and 4: "\<turnstile> \<box>(N & [~B]_f) & WF(A)_f & \<box>F & \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
- shows "\<turnstile> \<box>N & WF(A)_f & \<box>F \<longrightarrow> WF(M)_g"
+ assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g"
+ and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B"
+ and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
+ and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
+ shows "\<turnstile> \<box>N \<and> WF(A)_f \<and> \<box>F \<longrightarrow> WF(M)_g"
apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
simp: WF_def [where A = M])
apply (erule_tac F = F in dup_boxE)
@@ -970,7 +963,7 @@
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
apply (rule classical)
- apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <A>_f)")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)")
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
@@ -982,7 +975,7 @@
apply (erule_tac V = "sigmaa \<Turnstile> \<diamond>\<box>P" in thin_rl)
apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
apply (drule BoxWFI [temp_use])
- apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
+ apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE)
apply merge_temp_box
apply (erule DmdImpldup)
apply assumption
@@ -995,11 +988,11 @@
done
lemma SF2:
- assumes 1: "\<turnstile> N & <B>_f \<longrightarrow> <M>_g"
- and 2: "\<turnstile> $P & P` & <N & A>_f \<longrightarrow> B"
- and 3: "\<turnstile> P & Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
- and 4: "\<turnstile> \<box>(N & [~B]_f) & SF(A)_f & \<box>F & \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
- shows "\<turnstile> \<box>N & SF(A)_f & \<box>F \<longrightarrow> SF(M)_g"
+ assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g"
+ and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B"
+ and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
+ and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
+ shows "\<turnstile> \<box>N \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g"
apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
apply (erule_tac F = F in dup_boxE)
apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE)
@@ -1008,7 +1001,7 @@
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
apply (rule classical)
- apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <A>_f)")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)")
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
@@ -1018,7 +1011,7 @@
apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
apply (drule BoxSFI [temp_use])
apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE)
- apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
+ apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE)
apply merge_temp_box
apply (erule DmdImpldup)
apply assumption
@@ -1037,19 +1030,19 @@
lemma wf_leadsto:
assumes 1: "wf r"
- and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y)) "
+ and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G \<or> (\<exists>y. #((y,x)\<in>r) \<and> F y)) "
shows "sigma \<Turnstile> F x \<leadsto> G"
apply (rule 1 [THEN wf_induct])
apply (rule LatticeTriangle [temp_use])
apply (rule 2)
apply (auto simp: leadsto_exists [try_rewrite])
- apply (case_tac "(y,x) :r")
+ apply (case_tac "(y,x) \<in> r")
apply force
apply (force simp: leadsto_def Init_simps intro!: necT [temp_use])
done
(* If r is well-founded, state function v cannot decrease forever *)
-lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
+lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) \<in> #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
apply clarsimp
apply (rule ccontr)
apply (subgoal_tac "sigma \<Turnstile> (\<exists>x. v=#x) \<leadsto> #False")
@@ -1070,7 +1063,7 @@
*)
lemma wf_box_dmd_decrease:
assumes 1: "wf r"
- shows "\<turnstile> \<box>\<diamond>((v`, $v) : #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
+ shows "\<turnstile> \<box>\<diamond>((v`, $v) \<in> #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
apply clarsimp
apply (rule ccontr)
apply (simp add: not_angle [try_rewrite] more_temp_simps)
@@ -1089,7 +1082,7 @@
*)
lemma nat_box_dmd_decrease: "\<And>n::nat stfun. \<turnstile> \<box>\<diamond>(n` < $n) \<longrightarrow> \<box>\<diamond>($n < n`)"
apply clarsimp
- apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
+ apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><\<not> ((n`,$n) \<in> #less_than)>_n")
apply (erule thin_rl)
apply (erule STL4E)
apply (rule DmdImpl)
@@ -1141,9 +1134,9 @@
assumes 1: "sigma \<Turnstile> Init I"
and 2: "sigma \<Turnstile> \<box>N"
and 3: "basevars vs"
- and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I & h = ha \<longrightarrow> HI h"
+ and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I \<and> h = ha \<longrightarrow> HI h"
and 5: "\<And>h s t. \<lbrakk> basevars(h,vs); N (s,t); h t = hb (h s) (s,t) \<rbrakk> \<Longrightarrow> HN h (s,t)"
- shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) & \<box>(HN h)"
+ shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) \<and> \<box>(HN h)"
apply (rule history [temp_use, THEN eexE])
apply (rule 3)
apply (rule eexI [temp_use])
@@ -1161,7 +1154,7 @@
example of a history variable: existence of a clock
*)
-lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
+lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) \<and> \<box>(h` = (\<not>$h))"
apply (rule tempI)
apply (rule historyI)
apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+