--- a/src/HOL/TLA/Action.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Action.thy Fri Jun 26 14:53:15 2015 +0200
@@ -12,40 +12,40 @@
(** abstract syntax **)
-type_synonym 'a trfun = "(state * state) => 'a"
+type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
type_synonym action = "bool trfun"
instance prod :: (world, world) world ..
consts
(** abstract syntax **)
- before :: "'a stfun => 'a trfun"
- after :: "'a stfun => 'a trfun"
- unch :: "'a stfun => action"
+ before :: "'a stfun \<Rightarrow> 'a trfun"
+ after :: "'a stfun \<Rightarrow> 'a trfun"
+ unch :: "'a stfun \<Rightarrow> action"
- SqAct :: "[action, 'a stfun] => action"
- AnAct :: "[action, 'a stfun] => action"
- enabled :: "action => stpred"
+ SqAct :: "[action, 'a stfun] \<Rightarrow> action"
+ AnAct :: "[action, 'a stfun] \<Rightarrow> action"
+ enabled :: "action \<Rightarrow> stpred"
(** concrete syntax **)
syntax
(* Syntax for writing action expressions in arbitrary contexts *)
- "_ACT" :: "lift => 'a" ("(ACT _)")
+ "_ACT" :: "lift \<Rightarrow> 'a" ("(ACT _)")
- "_before" :: "lift => lift" ("($_)" [100] 99)
- "_after" :: "lift => lift" ("(_$)" [100] 99)
- "_unchanged" :: "lift => lift" ("(unchanged _)" [100] 99)
+ "_before" :: "lift \<Rightarrow> lift" ("($_)" [100] 99)
+ "_after" :: "lift \<Rightarrow> lift" ("(_$)" [100] 99)
+ "_unchanged" :: "lift \<Rightarrow> lift" ("(unchanged _)" [100] 99)
(*** Priming: same as "after" ***)
- "_prime" :: "lift => lift" ("(_`)" [100] 99)
+ "_prime" :: "lift \<Rightarrow> lift" ("(_`)" [100] 99)
- "_SqAct" :: "[lift, lift] => lift" ("([_]'_(_))" [0,1000] 99)
- "_AnAct" :: "[lift, lift] => lift" ("(<_>'_(_))" [0,1000] 99)
- "_Enabled" :: "lift => lift" ("(Enabled _)" [100] 100)
+ "_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0,1000] 99)
+ "_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0,1000] 99)
+ "_Enabled" :: "lift \<Rightarrow> lift" ("(Enabled _)" [100] 100)
translations
- "ACT A" => "(A::state*state => _)"
+ "ACT A" => "(A::state*state \<Rightarrow> _)"
"_before" == "CONST before"
"_after" == "CONST after"
"_prime" => "_after"
@@ -59,16 +59,16 @@
"w |= unchanged f" <= "_unchanged f w"
axiomatization where
- unl_before: "(ACT $v) (s,t) == v s" and
- unl_after: "(ACT v$) (s,t) == v t" and
+ unl_before: "(ACT $v) (s,t) \<equiv> v s" and
+ unl_after: "(ACT v$) (s,t) \<equiv> v t" and
- unchanged_def: "(s,t) |= unchanged v == (v t = v s)"
+ unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
defs
- square_def: "ACT [A]_v == ACT (A | unchanged v)"
- angle_def: "ACT <A>_v == ACT (A & \<not> unchanged v)"
+ square_def: "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
+ angle_def: "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
- enabled_def: "s |= Enabled A == \<exists>u. (s,u) |= A"
+ enabled_def: "s \<Turnstile> Enabled A \<equiv> \<exists>u. (s,u) \<Turnstile> A"
(* The following assertion specializes "intI" for any world type
@@ -76,22 +76,22 @@
*)
lemma actionI [intro!]:
- assumes "\<And>s t. (s,t) |= A"
- shows "|- A"
+ assumes "\<And>s t. (s,t) \<Turnstile> A"
+ shows "\<turnstile> A"
apply (rule assms intI prod.induct)+
done
-lemma actionD [dest]: "|- A ==> (s,t) |= A"
+lemma actionD [dest]: "\<turnstile> A \<Longrightarrow> (s,t) \<Turnstile> A"
apply (erule intD)
done
lemma pr_rews [int_rewrite]:
- "|- (#c)` = #c"
- "\<And>f. |- f<x>` = f<x` >"
- "\<And>f. |- f<x,y>` = f<x`,y` >"
- "\<And>f. |- f<x,y,z>` = f<x`,y`,z` >"
- "|- (\<forall>x. P x)` = (\<forall>x. (P x)`)"
- "|- (\<exists>x. P x)` = (\<exists>x. (P x)`)"
+ "\<turnstile> (#c)` = #c"
+ "\<And>f. \<turnstile> f<x>` = f<x` >"
+ "\<And>f. \<turnstile> f<x,y>` = f<x`,y` >"
+ "\<And>f. \<turnstile> f<x,y,z>` = f<x`,y`,z` >"
+ "\<turnstile> (\<forall>x. P x)` = (\<forall>x. (P x)`)"
+ "\<turnstile> (\<exists>x. P x)` = (\<exists>x. (P x)`)"
by (rule actionI, unfold unl_after intensional_rews, rule refl)+
@@ -112,7 +112,7 @@
(rewrite_rule ctxt @{thms action_rews} (th RS @{thm actionD}))
handle THM _ => int_unlift ctxt th;
-(* Turn |- A = B into meta-level rewrite rule A == B *)
+(* Turn \<turnstile> A = B into meta-level rewrite rule A == B *)
val action_rewrite = int_rewrite
fun action_use ctxt th =
@@ -132,69 +132,69 @@
(* =========================== square / angle brackets =========================== *)
-lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v"
+lemma idle_squareI: "(s,t) \<Turnstile> unchanged v \<Longrightarrow> (s,t) \<Turnstile> [A]_v"
by (simp add: square_def)
-lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"
+lemma busy_squareI: "(s,t) \<Turnstile> A \<Longrightarrow> (s,t) \<Turnstile> [A]_v"
by (simp add: square_def)
lemma squareE [elim]:
- "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
+ "\<lbrakk> (s,t) \<Turnstile> [A]_v; A (s,t) \<Longrightarrow> B (s,t); v t = v s \<Longrightarrow> B (s,t) \<rbrakk> \<Longrightarrow> B (s,t)"
apply (unfold square_def action_rews)
apply (erule disjE)
apply simp_all
done
-lemma squareCI [intro]: "[| v t \<noteq> v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
+lemma squareCI [intro]: "\<lbrakk> v t \<noteq> v s \<Longrightarrow> A (s,t) \<rbrakk> \<Longrightarrow> (s,t) \<Turnstile> [A]_v"
apply (unfold square_def action_rews)
apply (rule disjCI)
apply (erule (1) meta_mp)
done
-lemma angleI [intro]: "\<And>s t. [| A (s,t); v t \<noteq> v s |] ==> (s,t) |= <A>_v"
+lemma angleI [intro]: "\<And>s t. \<lbrakk> A (s,t); v t \<noteq> v s \<rbrakk> \<Longrightarrow> (s,t) \<Turnstile> <A>_v"
by (simp add: angle_def)
-lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t \<noteq> v s |] ==> R |] ==> R"
+lemma angleE [elim]: "\<lbrakk> (s,t) \<Turnstile> <A>_v; \<lbrakk> A (s,t); v t \<noteq> v s \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
apply (unfold angle_def action_rews)
apply (erule conjE)
apply simp
done
lemma square_simulation:
- "\<And>f. [| |- unchanged f & \<not>B --> unchanged g;
- |- A & \<not>unchanged g --> B
- |] ==> |- [A]_f --> [B]_g"
+ "\<And>f. \<lbrakk> \<turnstile> unchanged f & \<not>B \<longrightarrow> unchanged g;
+ \<turnstile> A & \<not>unchanged g \<longrightarrow> B
+ \<rbrakk> \<Longrightarrow> \<turnstile> [A]_f \<longrightarrow> [B]_g"
apply clarsimp
apply (erule squareE)
apply (auto simp add: square_def)
done
-lemma not_square: "|- (\<not> [A]_v) = <\<not>A>_v"
+lemma not_square: "\<turnstile> (\<not> [A]_v) = <\<not>A>_v"
by (auto simp: square_def angle_def)
-lemma not_angle: "|- (\<not> <A>_v) = [\<not>A]_v"
+lemma not_angle: "\<turnstile> (\<not> <A>_v) = [\<not>A]_v"
by (auto simp: square_def angle_def)
(* ============================== Facts about ENABLED ============================== *)
-lemma enabledI: "|- A --> $Enabled A"
+lemma enabledI: "\<turnstile> A \<longrightarrow> $Enabled A"
by (auto simp add: enabled_def)
-lemma enabledE: "[| s |= Enabled A; \<And>u. A (s,u) ==> Q |] ==> Q"
+lemma enabledE: "\<lbrakk> s \<Turnstile> Enabled A; \<And>u. A (s,u) \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
apply (unfold enabled_def)
apply (erule exE)
apply simp
done
-lemma notEnabledD: "|- \<not>$Enabled G --> \<not> G"
+lemma notEnabledD: "\<turnstile> \<not>$Enabled G \<longrightarrow> \<not> G"
by (auto simp add: enabled_def)
(* Monotonicity *)
lemma enabled_mono:
- assumes min: "s |= Enabled F"
- and maj: "|- F --> G"
- shows "s |= Enabled G"
+ assumes min: "s \<Turnstile> Enabled F"
+ and maj: "\<turnstile> F \<longrightarrow> G"
+ shows "s \<Turnstile> Enabled G"
apply (rule min [THEN enabledE])
apply (rule enabledI [action_use])
apply (erule maj [action_use])
@@ -202,50 +202,50 @@
(* stronger variant *)
lemma enabled_mono2:
- assumes min: "s |= Enabled F"
- and maj: "\<And>t. F (s,t) ==> G (s,t)"
- shows "s |= Enabled G"
+ assumes min: "s \<Turnstile> Enabled F"
+ and maj: "\<And>t. F (s,t) \<Longrightarrow> G (s,t)"
+ shows "s \<Turnstile> Enabled G"
apply (rule min [THEN enabledE])
apply (rule enabledI [action_use])
apply (erule maj)
done
-lemma enabled_disj1: "|- Enabled F --> Enabled (F | G)"
+lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F | G)"
by (auto elim!: enabled_mono)
-lemma enabled_disj2: "|- Enabled G --> Enabled (F | G)"
+lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F | G)"
by (auto elim!: enabled_mono)
-lemma enabled_conj1: "|- Enabled (F & G) --> Enabled F"
+lemma enabled_conj1: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled F"
by (auto elim!: enabled_mono)
-lemma enabled_conj2: "|- Enabled (F & G) --> Enabled G"
+lemma enabled_conj2: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled G"
by (auto elim!: enabled_mono)
lemma enabled_conjE:
- "[| s |= Enabled (F & G); [| s |= Enabled F; s |= Enabled G |] ==> Q |] ==> Q"
+ "\<lbrakk> s \<Turnstile> Enabled (F & 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: "|- Enabled (F | G) --> Enabled F | Enabled G"
+lemma enabled_disjD: "\<turnstile> Enabled (F | G) \<longrightarrow> Enabled F | Enabled G"
by (auto simp add: enabled_def)
-lemma enabled_disj: "|- Enabled (F | G) = (Enabled F | Enabled G)"
+lemma enabled_disj: "\<turnstile> Enabled (F | G) = (Enabled F | Enabled G)"
apply clarsimp
apply (rule iffI)
apply (erule enabled_disjD [action_use])
apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
done
-lemma enabled_ex: "|- Enabled (\<exists>x. F x) = (\<exists>x. Enabled (F x))"
+lemma enabled_ex: "\<turnstile> Enabled (\<exists>x. F x) = (\<exists>x. Enabled (F x))"
by (force simp add: enabled_def)
(* A rule that combines enabledI and baseE, but generates fewer instantiations *)
lemma base_enabled:
- "[| basevars vs; \<exists>c. \<forall>u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
+ "\<lbrakk> basevars vs; \<exists>c. \<forall>u. vs u = c \<longrightarrow> A(s,u) \<rbrakk> \<Longrightarrow> s \<Turnstile> Enabled A"
apply (erule exE)
apply (erule baseE)
apply (rule enabledI [action_use])
@@ -294,7 +294,7 @@
lemma
assumes "basevars (x,y,z)"
- shows "|- x --> Enabled ($x & (y$ = #False))"
+ shows "\<turnstile> x \<longrightarrow> Enabled ($x & (y$ = #False))"
apply (enabled assms)
apply auto
done
--- a/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 14:53:15 2015 +0200
@@ -10,14 +10,14 @@
consts
(* actions *)
- BInit :: "'a stfun => 'a list stfun => 'a stfun => stpred"
- Enq :: "'a stfun => 'a list stfun => 'a stfun => action"
- Deq :: "'a stfun => 'a list stfun => 'a stfun => action"
- Next :: "'a stfun => 'a list stfun => 'a stfun => action"
+ BInit :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> stpred"
+ Enq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+ Deq :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
+ Next :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> action"
(* temporal formulas *)
- IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal"
- Buffer :: "'a stfun => 'a stfun => temporal"
+ IBuffer :: "'a stfun \<Rightarrow> 'a list stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
+ Buffer :: "'a stfun \<Rightarrow> 'a stfun \<Rightarrow> temporal"
defs
BInit_def: "BInit ic q oc == PRED q = #[]"
@@ -38,28 +38,28 @@
(* ---------------------------- Data lemmas ---------------------------- *)
(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
-lemma tl_not_self [simp]: "xs \<noteq> [] ==> tl xs \<noteq> xs"
+lemma tl_not_self [simp]: "xs \<noteq> [] \<Longrightarrow> tl xs \<noteq> xs"
by (auto simp: neq_Nil_conv)
(* ---------------------------- Action lemmas ---------------------------- *)
(* Dequeue is visible *)
-lemma Deq_visible: "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"
+lemma Deq_visible: "\<turnstile> <Deq ic q oc>_(ic,q,oc) = Deq ic q oc"
apply (unfold angle_def Deq_def)
apply (safe, simp (asm_lr))+
done
(* Enabling condition for dequeue -- NOT NEEDED *)
lemma Deq_enabled:
- "\<And>q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])"
+ "\<And>q. basevars (ic,q,oc) \<Longrightarrow> \<turnstile> Enabled (<Deq ic q oc>_(ic,q,oc)) = (q \<noteq> #[])"
apply (unfold Deq_visible [temp_rewrite])
apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def)
done
(* For the left-to-right implication, we don't need the base variable stuff *)
lemma Deq_enabledE:
- "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (q \<noteq> #[])"
+ "\<turnstile> Enabled (<Deq ic q oc>_(ic,q,oc)) \<longrightarrow> (q \<noteq> #[])"
apply (unfold Deq_visible [temp_rewrite])
apply (auto elim!: enabledE simp add: Deq_def)
done
--- a/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 14:53:15 2015 +0200
@@ -50,12 +50,12 @@
(*** Proper initialization ***)
-lemma DBInit: "|- Init DBInit --> Init (BInit inp qc out)"
+lemma DBInit: "\<turnstile> Init DBInit \<longrightarrow> Init (BInit inp qc out)"
by (auto simp: Init_def DBInit_def BInit_def)
(*** Step simulation ***)
-lemma DB_step_simulation: "|- [DBNext]_(inp,mid,out,q1,q2) --> [Next inp qc out]_(inp,qc,out)"
+lemma DB_step_simulation: "\<turnstile> [DBNext]_(inp,mid,out,q1,q2) \<longrightarrow> [Next inp qc out]_(inp,qc,out)"
apply (rule square_simulation)
apply clarsimp
apply (tactic
@@ -66,23 +66,23 @@
(*** Simulation of fairness ***)
(* Compute enabledness predicates for DBDeq and DBPass actions *)
-lemma DBDeq_visible: "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"
+lemma DBDeq_visible: "\<turnstile> <DBDeq>_(inp,mid,out,q1,q2) = DBDeq"
apply (unfold angle_def DBDeq_def Deq_def)
apply (safe, simp (asm_lr))+
done
lemma DBDeq_enabled:
- "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 \<noteq> #[])"
+ "\<turnstile> Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 \<noteq> #[])"
apply (unfold DBDeq_visible [action_rewrite])
apply (force intro!: DB_base [THEN base_enabled, temp_use]
elim!: enabledE simp: angle_def DBDeq_def Deq_def)
done
-lemma DBPass_visible: "|- <DBPass>_(inp,mid,out,q1,q2) = DBPass"
+lemma DBPass_visible: "\<turnstile> <DBPass>_(inp,mid,out,q1,q2) = DBPass"
by (auto simp: angle_def DBPass_def Deq_def)
lemma DBPass_enabled:
- "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 \<noteq> #[])"
+ "\<turnstile> Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 \<noteq> #[])"
apply (unfold DBPass_visible [action_rewrite])
apply (force intro!: DB_base [THEN base_enabled, temp_use]
elim!: enabledE simp: angle_def DBPass_def Deq_def)
@@ -109,8 +109,8 @@
*)
(* Condition (1a) *)
-lemma DBFair_1a: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
- --> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
+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> #[])"
apply (rule WF1)
apply (force simp: db_defs)
apply (force simp: angle_def DBPass_def)
@@ -118,8 +118,8 @@
done
(* Condition (1) *)
-lemma DBFair_1: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
- --> (Enabled (<Deq inp qc out>_(inp,qc,out)) \<leadsto> q2 \<noteq> #[])"
+lemma DBFair_1: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & 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])
apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]])
@@ -130,8 +130,8 @@
done
(* Condition (2) *)
-lemma DBFair_2: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)
- --> (q2 \<noteq> #[] \<leadsto> DBDeq)"
+lemma DBFair_2: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)
+ \<longrightarrow> (q2 \<noteq> #[] \<leadsto> DBDeq)"
apply (rule WF_leadsto)
apply (force simp: DBDeq_enabled [temp_use])
apply (force simp: angle_def)
@@ -139,9 +139,9 @@
done
(* High-level fairness *)
-lemma DBFair: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
+lemma DBFair: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
& WF(DBDeq)_(inp,mid,out,q1,q2)
- --> WF(Deq inp qc out)_(inp,qc,out)"
+ \<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]]
DBFair_2 [temp_use, THEN [2] LatticeTransitivity [temp_use]])
@@ -150,7 +150,7 @@
done
(*** Main theorem ***)
-lemma DBuffer_impl_Buffer: "|- DBuffer --> Buffer inp out"
+lemma DBuffer_impl_Buffer: "\<turnstile> DBuffer \<longrightarrow> Buffer inp out"
apply (unfold DBuffer_def Buffer_def IBuffer_def)
apply (force intro!: eexI [temp_use] DBInit [temp_use]
DB_step_simulation [THEN STL4, temp_use] DBFair [temp_use])
--- a/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 14:53:15 2015 +0200
@@ -86,31 +86,31 @@
(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
-lemma PsiInv_Init: "|- InitPsi --> PsiInv"
+lemma PsiInv_Init: "\<turnstile> InitPsi \<longrightarrow> PsiInv"
by (auto simp: InitPsi_def PsiInv_defs)
-lemma PsiInv_alpha1: "|- alpha1 & $PsiInv --> PsiInv$"
+lemma PsiInv_alpha1: "\<turnstile> alpha1 & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: alpha1_def PsiInv_defs)
-lemma PsiInv_alpha2: "|- alpha2 & $PsiInv --> PsiInv$"
+lemma PsiInv_alpha2: "\<turnstile> alpha2 & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: alpha2_def PsiInv_defs)
-lemma PsiInv_beta1: "|- beta1 & $PsiInv --> PsiInv$"
+lemma PsiInv_beta1: "\<turnstile> beta1 & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: beta1_def PsiInv_defs)
-lemma PsiInv_beta2: "|- beta2 & $PsiInv --> PsiInv$"
+lemma PsiInv_beta2: "\<turnstile> beta2 & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: beta2_def PsiInv_defs)
-lemma PsiInv_gamma1: "|- gamma1 & $PsiInv --> PsiInv$"
+lemma PsiInv_gamma1: "\<turnstile> gamma1 & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: gamma1_def PsiInv_defs)
-lemma PsiInv_gamma2: "|- gamma2 & $PsiInv --> PsiInv$"
+lemma PsiInv_gamma2: "\<turnstile> gamma2 & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: gamma2_def PsiInv_defs)
-lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$"
+lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) & $PsiInv \<longrightarrow> PsiInv$"
by (auto simp: PsiInv_defs)
-lemma PsiInv: "|- Psi --> \<box>PsiInv"
+lemma PsiInv: "\<turnstile> Psi \<longrightarrow> \<box>PsiInv"
apply (invariant simp: Psi_def)
apply (force simp: PsiInv_Init [try_rewrite] Init_def)
apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
@@ -123,16 +123,16 @@
More realistic examples require user guidance anyway.
*)
-lemma "|- Psi --> \<box>PsiInv"
+lemma "\<turnstile> Psi \<longrightarrow> \<box>PsiInv"
by (auto_invariant simp: PsiInv_defs Psi_defs)
(**** Step simulation ****)
-lemma Init_sim: "|- Psi --> Init InitPhi"
+lemma Init_sim: "\<turnstile> Psi \<longrightarrow> Init InitPhi"
by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
-lemma Step_sim: "|- Psi --> \<box>[M1 | M2]_(x,y)"
+lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 | M2]_(x,y)"
by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
@@ -140,7 +140,7 @@
(*
The goal is to prove Fair_M1 far below, which asserts
- |- Psi --> WF(M1)_(x,y)
+ \<turnstile> Psi \<longrightarrow> WF(M1)_(x,y)
(the other fairness condition is symmetrical).
The strategy is to use WF2 (with beta1 as the helpful action). Proving its
@@ -154,10 +154,10 @@
the auxiliary lemmas are very similar.
*)
-lemma Stuck_at_b: "|- \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
+lemma Stuck_at_b: "\<turnstile> \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) \<longrightarrow> stable(pc1 = #b)"
by (auto elim!: Stable squareE simp: Psi_defs)
-lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
+lemma N1_enabled_at_g: "\<turnstile> pc1 = #g \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = gamma1 in enabled_mono)
apply (enabled Inc_base)
@@ -166,20 +166,20 @@
done
lemma g1_leadsto_a1:
- "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True
- --> (pc1 = #g \<leadsto> pc1 = #a)"
+ "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True
+ \<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)"
apply (rule SF1)
apply (tactic
{* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
{* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
- (* reduce |- \<box>A --> \<diamond>Enabled B to |- A --> Enabled B *)
+ (* reduce \<turnstile> \<box>A \<longrightarrow> \<diamond>Enabled B to \<turnstile> A \<longrightarrow> Enabled B *)
apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
dest!: STL2_gen [temp_use] simp: Init_def)
done
(* symmetrical for N2, and similar for beta2 *)
-lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
+lemma N2_enabled_at_g: "\<turnstile> pc2 = #g \<longrightarrow> Enabled (<N2>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = gamma2 in enabled_mono)
apply (enabled Inc_base)
@@ -188,8 +188,8 @@
done
lemma g2_leadsto_a2:
- "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
- --> (pc2 = #g \<leadsto> pc2 = #a)"
+ "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
+ \<longrightarrow> (pc2 = #g \<leadsto> pc2 = #a)"
apply (rule SF1)
apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs})
@@ -198,7 +198,7 @@
dest!: STL2_gen [temp_use] simp add: Init_def)
done
-lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
+lemma N2_enabled_at_b: "\<turnstile> pc2 = #b \<longrightarrow> Enabled (<N2>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = beta2 in enabled_mono)
apply (enabled Inc_base)
@@ -207,8 +207,8 @@
done
lemma b2_leadsto_g2:
- "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
- --> (pc2 = #b \<leadsto> pc2 = #g)"
+ "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
+ \<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)"
apply (rule SF1)
apply (tactic
{* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
@@ -220,8 +220,8 @@
(* Combine above lemmas: the second component will eventually reach pc2 = a *)
lemma N2_leadsto_a:
- "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
- --> (pc2 = #a | pc2 = #b | pc2 = #g \<leadsto> pc2 = #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)"
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
apply (rule LatticeReflexivity [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -230,8 +230,8 @@
(* Get rid of disjunction on the left-hand side of \<leadsto> above. *)
lemma N2_live:
- "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)
- --> \<diamond>(pc2 = #a)"
+ "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & 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)")
apply auto
@@ -240,7 +240,7 @@
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
lemma N1_enabled_at_both_a:
- "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
+ "\<turnstile> pc2 = #a & (PsiInv & 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,9 +249,9 @@
done
lemma a1_leadsto_b1:
- "|- \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))
+ "\<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)
- --> (pc1 = #a \<leadsto> pc1 = #b)"
+ \<longrightarrow> (pc1 = #a \<leadsto> pc1 = #b)"
apply (rule SF1)
apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
@@ -263,9 +263,9 @@
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
-lemma N1_leadsto_b: "|- \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))
+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)
- --> (pc1 = #b | pc1 = #g | pc1 = #a \<leadsto> pc1 = #b)"
+ \<longrightarrow> (pc1 = #b | pc1 = #g | pc1 = #a \<leadsto> pc1 = #b)"
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
apply (rule LatticeReflexivity [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -273,15 +273,15 @@
simp: split_box_conj)
done
-lemma N1_live: "|- \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))
+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)
- --> \<diamond>(pc1 = #b)"
+ \<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)")
apply auto
done
-lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
+lemma N1_enabled_at_b: "\<turnstile> pc1 = #b \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
apply clarsimp
apply (rule_tac F = beta1 in enabled_mono)
apply (enabled Inc_base)
@@ -291,9 +291,9 @@
(* Now assemble the bits and pieces to prove that Psi is fair. *)
-lemma Fair_M1_lemma: "|- \<box>($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))
+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)
- --> SF(M1)_(x,y)"
+ \<longrightarrow> SF(M1)_(x,y)"
apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
(* action premises *)
apply (force simp: angle_def M1_def beta1_def)
@@ -304,7 +304,7 @@
elim: STL4E [temp_use] simp: square_def)
done
-lemma Fair_M1: "|- Psi --> WF(M1)_(x,y)"
+lemma Fair_M1: "\<turnstile> Psi \<longrightarrow> WF(M1)_(x,y)"
by (auto intro!: SFImplWF [temp_use] Fair_M1_lemma [temp_use] PsiInv [temp_use]
simp: Psi_def split_box_conj [temp_use] more_temp_simps)
--- a/src/HOL/TLA/Init.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Init.thy Fri Jun 26 14:53:15 2015 +0200
@@ -18,22 +18,22 @@
consts
- Initial :: "('w::world => bool) => temporal"
- first_world :: "behavior => ('w::world)"
- st1 :: "behavior => state"
- st2 :: "behavior => state"
+ Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
+ first_world :: "behavior \<Rightarrow> ('w::world)"
+ st1 :: "behavior \<Rightarrow> state"
+ st2 :: "behavior \<Rightarrow> state"
syntax
- "_TEMP" :: "lift => 'a" ("(TEMP _)")
- "_Init" :: "lift => lift" ("(Init _)"[40] 50)
+ "_TEMP" :: "lift \<Rightarrow> 'a" ("(TEMP _)")
+ "_Init" :: "lift \<Rightarrow> lift" ("(Init _)"[40] 50)
translations
- "TEMP F" => "(F::behavior => _)"
+ "TEMP F" => "(F::behavior \<Rightarrow> _)"
"_Init" == "CONST Initial"
"sigma |= Init F" <= "_Init F sigma"
defs
- Init_def: "sigma |= Init F == (first_world sigma) |= F"
+ Init_def: "sigma \<Turnstile> Init F == (first_world sigma) \<Turnstile> F"
defs (overloaded)
fw_temp_def: "first_world == \<lambda>sigma. sigma"
@@ -41,37 +41,37 @@
fw_act_def: "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
lemma const_simps [int_rewrite, simp]:
- "|- (Init #True) = #True"
- "|- (Init #False) = #False"
+ "\<turnstile> (Init #True) = #True"
+ "\<turnstile> (Init #False) = #False"
by (auto simp: Init_def)
lemma Init_simps1 [int_rewrite]:
- "\<And>F. |- (Init \<not>F) = (\<not> Init F)"
- "|- (Init (P --> Q)) = (Init P --> Init Q)"
- "|- (Init (P & Q)) = (Init P & Init Q)"
- "|- (Init (P | Q)) = (Init P | Init Q)"
- "|- (Init (P = Q)) = ((Init P) = (Init Q))"
- "|- (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
- "|- (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
- "|- (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
+ "\<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 = 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))"
+ "\<turnstile> (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
by (auto simp: Init_def)
-lemma Init_stp_act: "|- (Init $P) = (Init P)"
+lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)"
by (auto simp add: Init_def fw_act_def fw_stp_def)
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
-lemma Init_temp: "|- (Init F) = F"
+lemma Init_temp: "\<turnstile> (Init F) = F"
by (auto simp add: Init_def fw_temp_def)
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
-lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
+lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)"
by (simp add: Init_def fw_stp_def)
-lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
+lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)"
by (simp add: Init_def fw_act_def)
lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
--- a/src/HOL/TLA/Intensional.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Jun 26 14:53:15 2015 +0200
@@ -14,79 +14,79 @@
(** abstract syntax **)
-type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *)
+type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a" (* intention: 'w::world, 'a::type *)
type_synonym 'w form = "('w, bool) expr"
consts
- Valid :: "('w::world) form => bool"
- const :: "'a => ('w::world, 'a) expr"
- lift :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr"
- lift2 :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr"
- lift3 :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr"
+ Valid :: "('w::world) form \<Rightarrow> bool"
+ const :: "'a \<Rightarrow> ('w::world, 'a) expr"
+ lift :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
+ lift2 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
+ lift3 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
(* "Rigid" quantification (logic level) *)
- RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10)
- REx :: "('a => ('w::world) form) => 'w form" (binder "Rex " 10)
- REx1 :: "('a => ('w::world) form) => 'w form" (binder "Rex! " 10)
+ RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rall " 10)
+ REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex " 10)
+ REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex! " 10)
(** concrete syntax **)
nonterminal lift and liftargs
syntax
- "" :: "id => lift" ("_")
- "" :: "longid => lift" ("_")
- "" :: "var => lift" ("_")
- "_applC" :: "[lift, cargs] => lift" ("(1_/ _)" [1000, 1000] 999)
- "" :: "lift => lift" ("'(_')")
- "_lambda" :: "[idts, 'a] => lift" ("(3\<lambda>_./ _)" [0, 3] 3)
- "_constrain" :: "[lift, type] => lift" ("(_::_)" [4, 0] 3)
- "" :: "lift => liftargs" ("_")
- "_liftargs" :: "[lift, liftargs] => liftargs" ("_,/ _")
- "_Valid" :: "lift => bool" ("(|- _)" 5)
- "_holdsAt" :: "['a, lift] => bool" ("(_ |= _)" [100,10] 10)
+ "" :: "id \<Rightarrow> lift" ("_")
+ "" :: "longid \<Rightarrow> lift" ("_")
+ "" :: "var \<Rightarrow> lift" ("_")
+ "_applC" :: "[lift, cargs] \<Rightarrow> lift" ("(1_/ _)" [1000, 1000] 999)
+ "" :: "lift \<Rightarrow> lift" ("'(_')")
+ "_lambda" :: "[idts, 'a] \<Rightarrow> lift" ("(3\<lambda>_./ _)" [0, 3] 3)
+ "_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)
- (* Syntax for lifted expressions outside the scope of |- or |= *)
- "_LIFT" :: "lift => 'a" ("LIFT _")
+ (* Syntax for lifted expressions outside the scope of \<turnstile> or |= *)
+ "_LIFT" :: "lift \<Rightarrow> 'a" ("LIFT _")
(* generic syntax for lifted constants and functions *)
- "_const" :: "'a => lift" ("(#_)" [1000] 999)
- "_lift" :: "['a, lift] => lift" ("(_<_>)" [1000] 999)
- "_lift2" :: "['a, lift, lift] => lift" ("(_<_,/ _>)" [1000] 999)
- "_lift3" :: "['a, lift, lift, lift] => lift" ("(_<_,/ _,/ _>)" [1000] 999)
+ "_const" :: "'a \<Rightarrow> lift" ("(#_)" [1000] 999)
+ "_lift" :: "['a, lift] \<Rightarrow> lift" ("(_<_>)" [1000] 999)
+ "_lift2" :: "['a, lift, lift] \<Rightarrow> lift" ("(_<_,/ _>)" [1000] 999)
+ "_lift3" :: "['a, lift, lift, lift] \<Rightarrow> lift" ("(_<_,/ _,/ _>)" [1000] 999)
(* concrete syntax for common infix functions: reuse same symbol *)
- "_liftEqu" :: "[lift, lift] => lift" ("(_ =/ _)" [50,51] 50)
- "_liftNeq" :: "[lift, lift] => lift" ("(_ ~=/ _)" [50,51] 50)
- "_liftNot" :: "lift => lift" ("(~ _)" [40] 40)
- "_liftAnd" :: "[lift, lift] => lift" ("(_ &/ _)" [36,35] 35)
- "_liftOr" :: "[lift, lift] => lift" ("(_ |/ _)" [31,30] 30)
- "_liftImp" :: "[lift, lift] => lift" ("(_ -->/ _)" [26,25] 25)
- "_liftIf" :: "[lift, lift, lift] => lift" ("(if (_)/ then (_)/ else (_))" 10)
- "_liftPlus" :: "[lift, lift] => lift" ("(_ +/ _)" [66,65] 65)
- "_liftMinus" :: "[lift, lift] => lift" ("(_ -/ _)" [66,65] 65)
- "_liftTimes" :: "[lift, lift] => lift" ("(_ */ _)" [71,70] 70)
- "_liftDiv" :: "[lift, lift] => lift" ("(_ div _)" [71,70] 70)
- "_liftMod" :: "[lift, lift] => lift" ("(_ mod _)" [71,70] 70)
- "_liftLess" :: "[lift, lift] => lift" ("(_/ < _)" [50, 51] 50)
- "_liftLeq" :: "[lift, lift] => lift" ("(_/ <= _)" [50, 51] 50)
- "_liftMem" :: "[lift, lift] => lift" ("(_/ : _)" [50, 51] 50)
- "_liftNotMem" :: "[lift, lift] => lift" ("(_/ ~: _)" [50, 51] 50)
- "_liftFinset" :: "liftargs => lift" ("{(_)}")
+ "_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)
+ "_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)
+ "_liftTimes" :: "[lift, lift] \<Rightarrow> lift" ("(_ */ _)" [71,70] 70)
+ "_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)
+ "_liftFinset" :: "liftargs \<Rightarrow> lift" ("{(_)}")
(** TODO: syntax for lifted collection / comprehension **)
- "_liftPair" :: "[lift,liftargs] => lift" ("(1'(_,/ _'))")
+ "_liftPair" :: "[lift,liftargs] \<Rightarrow> lift" ("(1'(_,/ _'))")
(* infix syntax for list operations *)
- "_liftCons" :: "[lift, lift] => lift" ("(_ #/ _)" [65,66] 65)
- "_liftApp" :: "[lift, lift] => lift" ("(_ @/ _)" [65,66] 65)
- "_liftList" :: "liftargs => lift" ("[(_)]")
+ "_liftCons" :: "[lift, lift] \<Rightarrow> lift" ("(_ #/ _)" [65,66] 65)
+ "_liftApp" :: "[lift, lift] \<Rightarrow> lift" ("(_ @/ _)" [65,66] 65)
+ "_liftList" :: "liftargs \<Rightarrow> lift" ("[(_)]")
(* Rigid quantification (syntax level) *)
- "_ARAll" :: "[idts, lift] => lift" ("(3! _./ _)" [0, 10] 10)
- "_AREx" :: "[idts, lift] => lift" ("(3? _./ _)" [0, 10] 10)
- "_AREx1" :: "[idts, lift] => lift" ("(3?! _./ _)" [0, 10] 10)
- "_RAll" :: "[idts, lift] => lift" ("(3ALL _./ _)" [0, 10] 10)
- "_REx" :: "[idts, lift] => lift" ("(3EX _./ _)" [0, 10] 10)
- "_REx1" :: "[idts, lift] => lift" ("(3EX! _./ _)" [0, 10] 10)
+ "_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)
translations
"_const" == "CONST const"
@@ -141,31 +141,31 @@
"w |= EX! x. A" <= "_REx1 x A w"
syntax (xsymbols)
- "_Valid" :: "lift => bool" ("(\<turnstile> _)" 5)
- "_holdsAt" :: "['a, lift] => bool" ("(_ \<Turnstile> _)" [100,10] 10)
- "_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50)
- "_liftNot" :: "lift => lift" ("\<not> _" [40] 40)
- "_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35)
- "_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30)
- "_liftImp" :: "[lift, lift] => lift" (infixr "\<longrightarrow>" 25)
- "_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10)
- "_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10)
- "_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10)
- "_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50)
- "_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50)
- "_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50)
+ "_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)
defs
- Valid_def: "|- A == \<forall>w. w |= A"
+ Valid_def: "\<turnstile> A == \<forall>w. w \<Turnstile> A"
unl_con: "LIFT #c w == c"
unl_lift: "lift f x w == f (x w)"
unl_lift2: "LIFT f<x, y> w == f (x w) (y w)"
unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
- unl_Rall: "w |= \<forall>x. A x == \<forall>x. (w |= A x)"
- unl_Rex: "w |= \<exists>x. A x == \<exists> x. (w |= A x)"
- unl_Rex1: "w |= \<exists>!x. A x == \<exists>!x. (w |= A x)"
+ 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_Rex1: "w \<Turnstile> \<exists>!x. A x == \<exists>!x. (w \<Turnstile> A x)"
subsection {* Lemmas and tactics for "intensional" logics. *}
@@ -173,20 +173,20 @@
lemmas intensional_rews [simp] =
unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1
-lemma inteq_reflection: "|- x=y ==> (x==y)"
+lemma inteq_reflection: "\<turnstile> x=y \<Longrightarrow> (x==y)"
apply (unfold Valid_def unl_lift2)
apply (rule eq_reflection)
apply (rule ext)
apply (erule spec)
done
-lemma intI [intro!]: "(\<And>w. w |= A) ==> |- A"
+lemma intI [intro!]: "(\<And>w. w \<Turnstile> A) \<Longrightarrow> \<turnstile> A"
apply (unfold Valid_def)
apply (rule allI)
apply (erule meta_spec)
done
-lemma intD [dest]: "|- A ==> w |= A"
+lemma intD [dest]: "\<turnstile> A \<Longrightarrow> w \<Turnstile> A"
apply (unfold Valid_def)
apply (erule spec)
done
@@ -194,30 +194,30 @@
(** Lift usual HOL simplifications to "intensional" level. **)
lemma int_simps:
- "|- (x=x) = #True"
- "|- (\<not>#True) = #False" "|- (\<not>#False) = #True" "|- (\<not>\<not> P) = P"
- "|- ((\<not>P) = P) = #False" "|- (P = (\<not>P)) = #False"
- "|- (P \<noteq> Q) = (P = (\<not>Q))"
- "|- (#True=P) = P" "|- (P=#True) = P"
- "|- (#True --> P) = P" "|- (#False --> P) = #True"
- "|- (P --> #True) = #True" "|- (P --> P) = #True"
- "|- (P --> #False) = (\<not>P)" "|- (P --> \<not>P) = (\<not>P)"
- "|- (P & #True) = P" "|- (#True & P) = P"
- "|- (P & #False) = #False" "|- (#False & P) = #False"
- "|- (P & P) = P" "|- (P & \<not>P) = #False" "|- (\<not>P & P) = #False"
- "|- (P | #True) = #True" "|- (#True | P) = #True"
- "|- (P | #False) = P" "|- (#False | P) = P"
- "|- (P | P) = P" "|- (P | \<not>P) = #True" "|- (\<not>P | P) = #True"
- "|- (\<forall>x. P) = P" "|- (\<exists>x. P) = P"
- "|- (\<not>Q --> \<not>P) = (P --> Q)"
- "|- (P|Q --> R) = ((P-->R)&(Q-->R))"
+ "\<turnstile> (x=x) = #True"
+ "\<turnstile> (\<not>#True) = #False" "\<turnstile> (\<not>#False) = #True" "\<turnstile> (\<not>\<not> P) = P"
+ "\<turnstile> ((\<not>P) = P) = #False" "\<turnstile> (P = (\<not>P)) = #False"
+ "\<turnstile> (P \<noteq> Q) = (P = (\<not>Q))"
+ "\<turnstile> (#True=P) = P" "\<turnstile> (P=#True) = P"
+ "\<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> (\<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))"
apply (unfold Valid_def intensional_rews)
apply blast+
done
declare int_simps [THEN inteq_reflection, simp]
-lemma TrueW [simp]: "|- #True"
+lemma TrueW [simp]: "\<turnstile> #True"
by (simp add: Valid_def unl_con)
@@ -226,21 +226,21 @@
ML {*
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
- |- F = G becomes F w = G w
- |- F --> G becomes F w --> G w
+ \<turnstile> F = G becomes F w = G w
+ \<turnstile> F \<longrightarrow> G becomes F w \<longrightarrow> G w
*)
fun int_unlift ctxt th =
rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
-(* Turn |- F = G into meta-level rewrite rule F == G *)
+(* Turn \<turnstile> F = G into meta-level rewrite rule F == G *)
fun int_rewrite ctxt th =
zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
-(* flattening turns "-->" into "==>" and eliminates conjunctions in the
+(* flattening turns "\<longrightarrow>" into "\<Longrightarrow>" and eliminates conjunctions in the
antecedent. For example,
- P & Q --> (R | S --> T) becomes [| P; Q; R | S |] ==> T
+ P & Q \<longrightarrow> (R | S \<longrightarrow> T) becomes \<lbrakk> P; Q; R | S \<rbrakk> \<Longrightarrow> T
Flattening can be useful with "intensional" lemmas (after unlifting).
Naive resolution with mp and conjI may run away because of higher-order
@@ -284,10 +284,10 @@
attribute_setup int_use =
{* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
-lemma Not_Rall: "|- (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
+lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
by (simp add: Valid_def)
-lemma Not_Rex: "|- (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)"
+lemma Not_Rex: "\<turnstile> (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)"
by (simp add: Valid_def)
end
--- a/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 14:53:15 2015 +0200
@@ -11,16 +11,16 @@
(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
type_synonym mClkSndChType = "memChType"
type_synonym mClkRcvChType = "rpcSndChType"
-type_synonym mClkStType = "(PrIds => mClkState) stfun"
+type_synonym mClkStType = "(PrIds \<Rightarrow> mClkState) stfun"
definition
(* state predicates *)
- MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred"
+ MClkInit :: "mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "MClkInit rcv cst p = PRED (cst!p = #clkA & \<not>Calling rcv p)"
definition
(* actions *)
- MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
+ MClkFwd :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkFwd send rcv cst p = ACT
$Calling send p
& $(cst!p) = #clkA
@@ -29,7 +29,7 @@
& unchanged (rtrner send!p)"
definition
- MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
+ MClkRetry :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkRetry send rcv cst p = ACT
$(cst!p) = #clkB
& res<$(rcv!p)> = #RPCFailure
@@ -37,7 +37,7 @@
& unchanged (cst!p, rtrner send!p)"
definition
- MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
+ MClkReply :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkReply send rcv cst p = ACT
\<not>$Calling rcv p
& $(cst!p) = #clkB
@@ -46,7 +46,7 @@
& unchanged (caller rcv!p)"
definition
- MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
+ 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
@@ -54,7 +54,7 @@
definition
(* temporal *)
- MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => 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)
@@ -62,7 +62,7 @@
& SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
definition
- MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
+ MClkISpec :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> temporal"
where "MClkISpec send rcv cst = TEMP (\<forall>p. MClkIPSpec send rcv cst p)"
lemmas MC_action_defs =
@@ -73,33 +73,33 @@
(* The Clerk engages in an action for process p only if there is an outstanding,
unanswered call for that process.
*)
-lemma MClkidle: "|- \<not>$Calling send p & $(cst!p) = #clkA --> \<not>MClkNext send rcv cst p"
+lemma MClkidle: "\<turnstile> \<not>$Calling send p & $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
by (auto simp: Return_def MC_action_defs)
-lemma MClkbusy: "|- $Calling rcv p --> \<not>MClkNext send rcv cst p"
+lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
by (auto simp: Call_def MC_action_defs)
(* Enabledness of actions *)
-lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>
- |- Calling send p & \<not>Calling rcv p & cst!p = #clkA
- --> Enabled (MClkFwd send rcv cst p)"
+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
+ \<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]
[@{thm base_enabled}, @{thm Pair_inject}] 1 *})
-lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p) -->
+lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p) \<longrightarrow>
Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
by (auto elim!: enabled_mono simp: angle_def MClkFwd_def)
-lemma MClkReply_change: "|- MClkReply send rcv cst p -->
+lemma MClkReply_change: "\<turnstile> MClkReply send rcv cst p \<longrightarrow>
<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
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) ==>
- |- Calling send p & \<not>Calling rcv p & cst!p = #clkB
- --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
+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
+ \<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 *})
apply (tactic {* action_simp_tac (@{context} addsimps
@@ -107,7 +107,7 @@
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
done
-lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> \<not>MClkRetry send rcv cst p"
+lemma MClkReplyNotRetry: "\<turnstile> MClkReply send rcv cst p \<longrightarrow> \<not>MClkRetry send rcv cst p"
by (auto simp: MClkReply_def MClkRetry_def)
end
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Fri Jun 26 14:53:15 2015 +0200
@@ -17,12 +17,12 @@
definition
(* translate a memory call to an RPC call *)
- MClkRelayArg :: "memOp => rpcOp"
+ MClkRelayArg :: "memOp \<Rightarrow> rpcOp"
where "MClkRelayArg marg = memcall marg"
definition
(* translate RPC failures to memory failures *)
- MClkReplyVal :: "Vals => Vals"
+ MClkReplyVal :: "Vals \<Rightarrow> Vals"
where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
end
--- a/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 14:53:15 2015 +0200
@@ -9,46 +9,46 @@
begin
type_synonym memChType = "(memOp, Vals) channel"
-type_synonym memType = "(Locs => Vals) stfun" (* intention: MemLocs => MemVals *)
-type_synonym resType = "(PrIds => Vals) stfun"
+type_synonym memType = "(Locs \<Rightarrow> Vals) stfun" (* intention: MemLocs \<Rightarrow> MemVals *)
+type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun"
consts
(* state predicates *)
- MInit :: "memType => Locs => stpred"
- PInit :: "resType => PrIds => stpred"
+ MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
+ PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred"
(* auxiliary predicates: is there a pending read/write request for
some process id and location/value? *)
- RdRequest :: "memChType => PrIds => Locs => stpred"
- WrRequest :: "memChType => PrIds => Locs => Vals => stpred"
+ RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred"
+ WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred"
(* actions *)
- GoodRead :: "memType => resType => PrIds => Locs => action"
- BadRead :: "memType => resType => PrIds => Locs => action"
- ReadInner :: "memChType => memType => resType => PrIds => Locs => action"
- Read :: "memChType => memType => resType => PrIds => action"
- GoodWrite :: "memType => resType => PrIds => Locs => Vals => action"
- BadWrite :: "memType => resType => PrIds => Locs => Vals => action"
- WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action"
- Write :: "memChType => memType => resType => PrIds => Locs => action"
- MemReturn :: "memChType => resType => PrIds => action"
- MemFail :: "memChType => resType => PrIds => action"
- RNext :: "memChType => memType => resType => PrIds => action"
- UNext :: "memChType => memType => resType => PrIds => action"
+ GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+ BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+ WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action"
+ Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action"
+ MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
+ UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action"
(* temporal formulas *)
- RPSpec :: "memChType => memType => resType => PrIds => temporal"
- UPSpec :: "memChType => memType => resType => PrIds => temporal"
- MSpec :: "memChType => memType => resType => Locs => temporal"
- IRSpec :: "memChType => memType => resType => temporal"
- IUSpec :: "memChType => memType => resType => temporal"
+ RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+ UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal"
+ MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal"
+ IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
+ IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal"
- RSpec :: "memChType => resType => temporal"
- USpec :: "memChType => temporal"
+ RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal"
+ USpec :: "memChType \<Rightarrow> temporal"
(* memory invariant: in the paper, the invariant is hidden in the definition of
the predicate S used in the implementation proof, but it is easier to verify
at this level. *)
- MemInv :: "memType => Locs => stpred"
+ MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred"
defs
MInit_def: "MInit mm l == PRED mm!l = #InitVal"
@@ -119,15 +119,15 @@
& \<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 --> MSpec ch mm rs l)"
+ & (\<forall>l. #l : #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 --> MSpec ch mm rs l)"
+ & (\<forall>l. #l : #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 --> mm!l : #MemVal"
+ MemInv_def: "MemInv mm l == PRED #l : #MemLoc \<longrightarrow> mm!l : #MemVal"
lemmas RM_action_defs =
MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
@@ -142,19 +142,19 @@
(* The reliable memory is an implementation of the unreliable one *)
-lemma ReliableImplementsUnReliable: "|- IRSpec ch mm rs --> IUSpec ch mm rs"
+lemma ReliableImplementsUnReliable: "\<turnstile> IRSpec ch mm rs \<longrightarrow> IUSpec ch mm rs"
by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE)
(* The memory spec implies the memory invariant *)
-lemma MemoryInvariant: "|- MSpec ch mm rs l --> \<box>(MemInv mm l)"
+lemma MemoryInvariant: "\<turnstile> MSpec ch mm rs l \<longrightarrow> \<box>(MemInv mm l)"
by (auto_invariant simp: RM_temp_defs RM_action_defs)
(* The invariant is trivial for non-locations *)
-lemma NonMemLocInvariant: "|- #l \<notin> #MemLoc --> \<box>(MemInv mm l)"
+lemma NonMemLocInvariant: "\<turnstile> #l \<notin> #MemLoc \<longrightarrow> \<box>(MemInv mm l)"
by (auto simp: MemInv_def intro!: necT [temp_use])
lemma MemoryInvariantAll:
- "|- (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l) --> (\<forall>l. \<box>(MemInv mm l))"
+ "\<turnstile> (\<forall>l. #l : #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
@@ -164,17 +164,17 @@
We need this only for the reliable memory.
*)
-lemma Memoryidle: "|- \<not>$(Calling ch p) --> \<not> RNext ch mm rs p"
+lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
by (auto simp: Return_def RM_action_defs)
(* Enabledness conditions *)
-lemma MemReturn_change: "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
+lemma MemReturn_change: "\<turnstile> MemReturn ch rs p \<longrightarrow> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
by (force simp: MemReturn_def angle_def)
-lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) ==>
- |- Calling ch p & (rs!p \<noteq> #NotAResult)
- --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
+lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow>
+ \<turnstile> Calling ch p & (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 *})
apply (tactic
@@ -182,34 +182,34 @@
@{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
done
-lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) ==>
- |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
+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)"
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) ==>
- |- Calling ch p & (arg<ch!p> = #(write l v))
- --> Enabled (WriteInner ch mm rs p l v)"
+lemma WriteInner_enabled: "\<And>p. basevars (mm!l, rtrner ch ! p, rs!p) \<Longrightarrow>
+ \<turnstile> Calling ch p & (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: "|- Read ch mm rs p & (\<forall>l. $(MemInv mm l)) --> (rs!p)` \<noteq> #NotAResult"
+lemma ReadResult: "\<turnstile> Read ch mm rs p & (\<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: "|- Write ch mm rs p l --> (rs!p)` \<noteq> #NotAResult"
+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: "|- (\<forall>l. $MemInv mm l) & MemReturn ch rs p
- --> \<not> Read ch mm rs p & (\<forall>l. \<not> Write ch mm rs p l)"
+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)"
by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
-lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l)
+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))
- --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
+ \<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])
@@ -217,9 +217,9 @@
(* Combine previous lemmas: the memory can make a visible step if there is an
outstanding call for which no result has been produced.
*)
-lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) ==>
- |- (rs!p = #NotAResult) & Calling ch p & (\<forall>l. MemInv mm l)
- --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
+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)
+ \<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)")
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Read_def},
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 14:53:15 2015 +0200
@@ -10,7 +10,7 @@
datatype histState = histA | histB
-type_synonym histType = "(PrIds => histState) stfun" (* the type of the history variable *)
+type_synonym histType = "(PrIds \<Rightarrow> histState) stfun" (* the type of the history variable *)
consts
(* the specification *)
@@ -32,15 +32,15 @@
definition
(* auxiliary predicates *)
- MVOKBARF :: "Vals => bool"
+ MVOKBARF :: "Vals \<Rightarrow> bool"
where "MVOKBARF v <-> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
definition
- MVOKBA :: "Vals => bool"
+ MVOKBA :: "Vals \<Rightarrow> bool"
where "MVOKBA v <-> (v : MemVal) | (v = OK) | (v = BadArg)"
definition
- MVNROKBA :: "Vals => bool"
+ MVNROKBA :: "Vals \<Rightarrow> bool"
where "MVNROKBA v <-> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
definition
@@ -49,30 +49,30 @@
where "e p = PRED (caller memCh!p)"
definition
- c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
+ c :: "PrIds \<Rightarrow> (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
where "c p = PRED (cst!p, rtrner memCh!p, caller crCh!p)"
definition
- r :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
+ r :: "PrIds \<Rightarrow> (rpcState * (bit * Vals) * (bit * memOp)) stfun"
where "r p = PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
definition
- m :: "PrIds => ((bit * Vals) * Vals) stfun"
+ m :: "PrIds \<Rightarrow> ((bit * Vals) * Vals) stfun"
where "m p = PRED (rtrner rmCh!p, ires!p)"
definition
(* the environment action *)
- ENext :: "PrIds => action"
+ ENext :: "PrIds \<Rightarrow> action"
where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
definition
(* specification of the history variable *)
- HInit :: "histType => PrIds => stpred"
+ HInit :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "HInit rmhist p = PRED rmhist!p = #histA"
definition
- HNext :: "histType => PrIds => action"
+ HNext :: "histType \<Rightarrow> PrIds \<Rightarrow> action"
where "HNext rmhist p = ACT (rmhist!p)$ =
(if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
then #histB
@@ -81,39 +81,39 @@
else $(rmhist!p))"
definition
- HistP :: "histType => PrIds => temporal"
+ 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))"
definition
- Hist :: "histType => temporal"
+ Hist :: "histType \<Rightarrow> temporal"
where "Hist rmhist = TEMP (\<forall>p. HistP rmhist p)"
definition
(* the implementation *)
- IPImp :: "PrIds => temporal"
+ 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 --> MSpec rmCh mm ires l)))"
+ & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
definition
- ImpInit :: "PrIds => stpred"
+ ImpInit :: "PrIds \<Rightarrow> stpred"
where "ImpInit p = PRED ( \<not>Calling memCh p
& MClkInit crCh cst p
& RPCInit rmCh rst p
& PInit ires p)"
definition
- ImpNext :: "PrIds => action"
+ 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))"
definition
- ImpLive :: "PrIds => temporal"
+ 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)
@@ -134,16 +134,16 @@
NB: The second conjunct of the definition in the paper is taken care of by
the type definitions. The last conjunct is asserted separately as the memory
invariant MemInv, proved in Memory.thy. *)
- S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
+ 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 --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
- & (\<not> #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
+ & (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
+ & (\<not> #ccalling & cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
& Calling rmCh p = #rcalling
- & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
- & (\<not> #rcalling --> ires!p = #NotAResult)
- & (\<not> #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
+ & (#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)
@@ -151,37 +151,37 @@
definition
(* predicates S1 -- S6 define special instances of S *)
- S1 :: "histType => PrIds => stpred"
+ S1 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S1 rmhist p = S rmhist False False False clkA rpcA histA histA p"
definition
- S2 :: "histType => PrIds => stpred"
+ S2 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S2 rmhist p = S rmhist True False False clkA rpcA histA histA p"
definition
- S3 :: "histType => PrIds => stpred"
+ S3 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S3 rmhist p = S rmhist True True False clkB rpcA histA histB p"
definition
- S4 :: "histType => PrIds => stpred"
+ S4 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S4 rmhist p = S rmhist True True True clkB rpcB histA histB p"
definition
- S5 :: "histType => PrIds => stpred"
+ S5 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S5 rmhist p = S rmhist True True False clkB rpcB histB histB p"
definition
- S6 :: "histType => PrIds => stpred"
+ S6 :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "S6 rmhist p = S rmhist True False False clkB rpcA histB histB p"
definition
(* The invariant asserts that the system is always in one of S1 - S6, for every p *)
- ImpInv :: "histType => PrIds => stpred"
+ 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))"
definition
- resbar :: "histType => resType" (* refinement mapping *)
+ resbar :: "histType \<Rightarrow> resType" (* refinement mapping *)
where"resbar rmhist s p =
(if (S1 rmhist p s | S2 rmhist p s)
then ires s p
@@ -241,8 +241,8 @@
section "History variable"
-lemma HistoryLemma: "|- Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
- --> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
+lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) & \<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)))"
apply clarsimp
apply (rule historyI)
@@ -255,7 +255,7 @@
apply (erule fun_cong)
done
-lemma History: "|- Implementation --> (\<exists>\<exists>rmhist. Hist rmhist)"
+lemma History: "\<turnstile> Implementation \<longrightarrow> (\<exists>\<exists>rmhist. Hist rmhist)"
apply clarsimp
apply (rule HistoryLemma [temp_use, THEN eex_mono])
prefer 3
@@ -274,14 +274,14 @@
(* RPCFailure notin MemVals U {OK,BadArg} *)
-lemma MVOKBAnotRF: "MVOKBA x ==> x \<noteq> RPCFailure"
+lemma MVOKBAnotRF: "MVOKBA x \<Longrightarrow> x \<noteq> RPCFailure"
apply (unfold MVOKBA_def)
apply auto
done
(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
-lemma MVOKBARFnotNR: "MVOKBARF x ==> x \<noteq> NotAResult"
+lemma MVOKBARFnotNR: "MVOKBARF x \<Longrightarrow> x \<noteq> NotAResult"
apply (unfold MVOKBARF_def)
apply auto
done
@@ -294,32 +294,32 @@
*)
(* --- not used ---
-lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p &
+lemma S1_excl: "\<turnstile> S1 rmhist p \<longrightarrow> S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p &
\<not>S4 rmhist p & \<not>S5 rmhist p & \<not>S6 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
*)
-lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & \<not>S1 rmhist p"
+lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p & \<not>S1 rmhist p"
by (auto simp: S_def S1_def S2_def)
-lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
+lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def)
-lemma S4_excl: "|- S4 rmhist p --> 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 & \<not>S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p"
by (auto simp: S_def S1_def S2_def S3_def S4_def)
-lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
+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"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
-lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
+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"
by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
(* ==================== Lemmas about the environment ============================== *)
-lemma Envbusy: "|- $(Calling memCh p) --> \<not>ENext p"
+lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
by (auto simp: ENext_def Call_def)
(* ==================== Lemmas about the implementation's states ==================== *)
@@ -331,25 +331,25 @@
(* ------------------------------ State S1 ---------------------------------------- *)
-lemma S1Env: "|- ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p)
- --> (S2 rmhist p)$"
+lemma S1Env: "\<turnstile> ENext p & $(S1 rmhist p) & 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: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
+lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(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: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
+lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(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: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
+lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(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: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
- --> unchanged (rmhist!p)"
+lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(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},
@{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
@@ -357,88 +357,88 @@
(* ------------------------------ State S2 ---------------------------------------- *)
-lemma S2EnvUnch: "|- [ENext p]_(e p) & $(S2 rmhist p) --> unchanged (e p)"
+lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
-lemma S2Clerk: "|- MClkNext memCh crCh cst p & $(S2 rmhist p) --> MClkFwd memCh crCh cst p"
+lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
-lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
+lemma S2Forward: "\<turnstile> $(S2 rmhist p) & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)
- --> (S3 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: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
+lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
-lemma S2MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) --> unchanged (m p)"
+lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
-lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
- --> unchanged (rmhist!p)"
+lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
+ \<longrightarrow> unchanged (rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
MClkReply_def Return_def S_def S2_def)
(* ------------------------------ State S3 ---------------------------------------- *)
-lemma S3EnvUnch: "|- [ENext p]_(e p) & $(S3 rmhist p) --> unchanged (e p)"
+lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
-lemma S3ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) --> unchanged (c p)"
+lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
-lemma S3LegalRcvArg: "|- S3 rmhist p --> IsLegalRcvArg<arg<crCh!p>>"
+lemma S3LegalRcvArg: "\<turnstile> S3 rmhist p \<longrightarrow> IsLegalRcvArg<arg<crCh!p>>"
by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
-lemma S3RPC: "|- RPCNext crCh rmCh rst p & $(S3 rmhist p)
- --> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S3 rmhist p)
+ \<longrightarrow> RPCFwd crCh rmCh rst p | 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: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
+lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
& unchanged (e p, c p, m p)
- --> (S4 rmhist p)$ & unchanged (rmhist!p)"
+ \<longrightarrow> (S4 rmhist p)$ & 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: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
+lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
& unchanged (e p, c p, m p)
- --> (S6 rmhist 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: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
+lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
-lemma S3Hist: "|- HNext rmhist p & $(S3 rmhist p) & unchanged (r p) --> unchanged (rmhist!p)"
+lemma S3Hist: "\<turnstile> HNext rmhist p & $(S3 rmhist p) & 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: "|- [ENext p]_(e p) & $(S4 rmhist p) --> unchanged (e p)"
+lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
-lemma S4ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) --> unchanged (c p)"
+lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
-lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
+lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(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: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
+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)
- --> (S4 rmhist p)$ & unchanged (rmhist!p)"
+ \<longrightarrow> (S4 rmhist p)$ & 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,105 +446,105 @@
@{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
-lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
+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)
- --> (S4 rmhist p)$ & unchanged (rmhist!p)"
+ \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
by (auto simp: Read_def dest!: S4ReadInner [temp_use])
-lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p
- --> (S4 rmhist p)$ & unchanged (rmhist!p)"
+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)"
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: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
+lemma S4Write: "\<turnstile> Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
& (HNext rmhist p)
- --> (S4 rmhist p)$ & unchanged (rmhist!p)"
+ \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
by (auto simp: Write_def dest!: S4WriteInner [temp_use])
-lemma WriteS4: "|- $ImpInv rmhist p & Write rmCh mm ires p l --> $S4 rmhist p"
+lemma WriteS4: "\<turnstile> $ImpInv rmhist p & 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: "|- MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
+lemma S4Return: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
& HNext rmhist p
- --> (S5 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: "|- HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) --> (rmhist!p)$ = $(rmhist!p)"
+lemma S4Hist: "\<turnstile> HNext rmhist p & $S4 rmhist p & (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: "|- [ENext p]_(e p) & $(S5 rmhist p) --> unchanged (e p)"
+lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
-lemma S5ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) --> unchanged (c p)"
+lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
-lemma S5RPC: "|- RPCNext crCh rmCh rst p & $(S5 rmhist p)
- --> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S5 rmhist p)
+ \<longrightarrow> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
-lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
- --> (S6 rmhist p)$"
+lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p & $(S5 rmhist p) & 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: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
- --> (S6 rmhist p)$"
+lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S5 rmhist p) & 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: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
+lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
-lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
- --> (rmhist!p)$ = $(rmhist!p)"
+lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
+ \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
MClkReply_def Return_def S_def S5_def)
(* ------------------------------ State S6 ---------------------------------------- *)
-lemma S6EnvUnch: "|- [ENext p]_(e p) & $(S6 rmhist p) --> unchanged (e p)"
+lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
-lemma S6Clerk: "|- MClkNext memCh crCh cst p & $(S6 rmhist p)
- --> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
+lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S6 rmhist p)
+ \<longrightarrow> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
-lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
+lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
- --> (S3 rmhist p)$ & unchanged (rmhist!p)"
+ \<longrightarrow> (S3 rmhist p)$ & 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: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
+lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
& unchanged (e p,r p,m p)
- --> (S1 rmhist 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: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
+lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p \<longrightarrow> unchanged (r p)"
by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
-lemma S6MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) --> unchanged (m p)"
+lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
-lemma S6Hist: "|- HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) --> (rmhist!p)$ = $(rmhist!p)"
+lemma S6Hist: "\<turnstile> HNext rmhist p & $S6 rmhist p & (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: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
+lemma Step1_1: "\<turnstile> ImpInit p & 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: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
+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
- --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
+ \<longrightarrow> (S2 rmhist p)$ & ENext p & 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,9 +572,9 @@
apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
done
-lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
+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
- --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
+ \<longrightarrow> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
& unchanged (e p, r p, m p, rmhist!p)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context})
@@ -583,9 +583,9 @@
apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
done
-lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
+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
- --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, 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))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
@@ -595,10 +595,10 @@
apply (auto dest!: S3Hist [temp_use])
done
-lemma Step1_2_4: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
+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))
- --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
+ \<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))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
@@ -609,9 +609,9 @@
apply (auto dest!: S4Hist [temp_use])
done
-lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
+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
- --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m 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))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
@@ -620,9 +620,9 @@
apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
done
-lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
+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
- --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m 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))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
@@ -637,7 +637,7 @@
section "Initialization (Step 1.3)"
-lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
+lemma Step1_3: "\<turnstile> S1 rmhist p \<longrightarrow> PInit (resbar rmhist) p"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm resbar_def},
@{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
@@ -648,30 +648,30 @@
section "Step simulation (Step 1.4)"
-lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
- --> unchanged (rtrner memCh!p, resbar rmhist!p)"
+lemma Step1_4_1: "\<turnstile> ENext p & $S1 rmhist p & (S2 rmhist p)$ & 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: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
+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)
- --> unchanged (rtrner memCh!p, resbar 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: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
+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)
- --> unchanged (rtrner memCh!p, resbar rmhist!p)"
+ \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S3_excl [temp_use] S4_excl [temp_use])+
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
@{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
done
-lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
+lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
& unchanged (e p, c p, m p)
- --> MemFail memCh (resbar rmhist) p"
+ \<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
@@ -679,9 +679,9 @@
apply (auto simp: Return_def)
done
-lemma Step1_4_4a1: "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
+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
- --> ReadInner memCh mm (resbar rmhist) p l"
+ \<longrightarrow> ReadInner memCh mm (resbar rmhist) p l"
apply clarsimp
apply (drule S4_excl [temp_use])+
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
@@ -693,14 +693,14 @@
[] [@{thm impE}, @{thm MemValNotAResultE}]) *})
done
-lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
+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))
- --> Read memCh mm (resbar rmhist) p"
+ \<longrightarrow> Read memCh mm (resbar rmhist) p"
by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
-lemma Step1_4_4b1: "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
+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)
- --> WriteInner memCh mm (resbar rmhist) p l v"
+ \<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v"
apply clarsimp
apply (drule S4_excl [temp_use])+
apply (tactic {* action_simp_tac (@{context} addsimps
@@ -712,14 +712,14 @@
@{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
done
-lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
+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)
- --> Write memCh mm (resbar rmhist) p l"
+ \<longrightarrow> Write memCh mm (resbar rmhist) p l"
by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
-lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
+lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
& unchanged (e p, c p, r p)
- --> unchanged (rtrner memCh!p, resbar rmhist!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 *})
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
@@ -727,27 +727,27 @@
apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
done
-lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
+lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
& unchanged (e p, c p, m p)
- --> unchanged (rtrner memCh!p, resbar rmhist!p)"
+ \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (drule S5_excl [temp_use] S6_excl [temp_use])+
apply (auto simp: e_def c_def m_def resbar_def)
apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
done
-lemma Step1_4_5b: "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
+lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
& unchanged (e p, c p, m p)
- --> MemFail memCh (resbar rmhist) p"
+ \<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
apply (auto simp: S5_def S_def)
done
-lemma Step1_4_6a: "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
+lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
& unchanged (e p, r p, m p)
- --> MemReturn memCh (resbar rmhist) p"
+ \<longrightarrow> MemReturn memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])+
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
@@ -758,9 +758,9 @@
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
done
-lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
+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)
- --> MemFail memCh (resbar rmhist) p"
+ \<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S3_excl [temp_use])+
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def},
@@ -768,12 +768,12 @@
apply (auto simp: S6_def S_def)
done
-lemma S_lemma: "|- unchanged (e p, c p, r p, m p, rmhist!p)
- --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
+lemma S_lemma: "\<turnstile> unchanged (e p, c p, r p, m p, rmhist!p)
+ \<longrightarrow> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"
by (auto simp: e_def c_def r_def m_def caller_def rtrner_def S_def Calling_def)
-lemma Step1_4_7H: "|- unchanged (e p, c p, r p, m p, rmhist!p)
- --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p,
+lemma Step1_4_7H: "\<turnstile> unchanged (e p, c p, r p, m p, rmhist!p)
+ \<longrightarrow> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p,
S4 rmhist p, S5 rmhist p, S6 rmhist p)"
apply clarsimp
apply (rule conjI)
@@ -781,8 +781,8 @@
apply (force simp: S1_def S2_def S3_def S4_def S5_def S6_def intro!: S_lemma [temp_use])
done
-lemma Step1_4_7: "|- unchanged (e p, c p, r p, m p, rmhist!p)
- --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p,
+lemma Step1_4_7: "\<turnstile> unchanged (e p, c p, r p, m p, rmhist!p)
+ \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p,
S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)"
apply (rule actionI)
apply (unfold action_rews)
@@ -798,7 +798,7 @@
fun split_idle_tac ctxt =
SELECT_GOAL
(TRY (rtac @{thm actionI} 1) THEN
- Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
+ Induct_Tacs.case_tac ctxt "(s,t) \<Turnstile> unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
rewrite_goals_tac ctxt @{thms action_rews} THEN
forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
asm_full_simp_tac ctxt 1);
@@ -816,42 +816,42 @@
(* Steps that leave all variables unchanged are safe, so I may assume
that some variable changes in the proof that a step is safe. *)
-lemma unchanged_safe: "|- (\<not>unchanged (e p, c p, r p, m p, rmhist!p)
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma unchanged_safe: "\<turnstile> (\<not>unchanged (e p, c p, r p, m p, rmhist!p)
+ \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
+ \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply (split_idle simp: square_def)
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
-lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma S1safe: "\<turnstile> $S1 rmhist p & ImpNext p & [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)
apply (rule idle_squareI)
apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
done
-lemma S2safe: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma S2safe: "\<turnstile> $S2 rmhist p & ImpNext p & [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)
apply (rule idle_squareI)
apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
done
-lemma S3safe: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma S3safe: "\<turnstile> $S3 rmhist p & ImpNext p & [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)
apply (auto dest!: Step1_2_3 [temp_use])
apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
done
-lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S4safe: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
& (\<forall>l. $(MemInv mm l))
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+ \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
apply (auto dest!: Step1_2_4 [temp_use])
@@ -859,16 +859,16 @@
dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
done
-lemma S5safe: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma S5safe: "\<turnstile> $S5 rmhist p & ImpNext p & [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)
apply (auto dest!: Step1_2_5 [temp_use])
apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
done
-lemma S6safe: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma S6safe: "\<turnstile> $S6 rmhist p & ImpNext p & [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)
apply (auto dest!: Step1_2_6 [temp_use])
@@ -889,8 +889,8 @@
(* ------------------------------ State S1 ------------------------------ *)
-lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> (S1 rmhist p)$ | (S2 rmhist p)$"
+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)$"
apply split_idle
apply (auto dest!: Step1_2_1 [temp_use])
done
@@ -899,199 +899,199 @@
by entering the state S1 infinitely often.
*)
-lemma S1_RNextdisabled: "|- S1 rmhist p -->
+lemma S1_RNextdisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
\<not>Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
@{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
apply force
done
-lemma S1_Returndisabled: "|- S1 rmhist p -->
+lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
\<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
@{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
-lemma RNext_fair: "|- \<box>\<diamond>S1 rmhist p
- --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
+lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
+ \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
elim!: STL4E [temp_use] DmdImplE [temp_use])
-lemma Return_fair: "|- \<box>\<diamond>S1 rmhist p
- --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
+lemma Return_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
+ \<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
by (auto simp: WF_alt [try_rewrite]
intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
(* ------------------------------ State S2 ------------------------------ *)
-lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> (S2 rmhist p)$ | (S3 rmhist p)$"
+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)$"
apply split_idle
apply (auto dest!: Step1_2_2 [temp_use])
done
-lemma S2MClkFwd_successors: "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+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)
- --> (S3 rmhist p)$"
+ \<longrightarrow> (S3 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
-lemma S2MClkFwd_enabled: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
+lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p & ImpNext p & [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)
apply (blast dest: base_pair)
apply (simp_all add: S_def S2_def)
done
-lemma S2_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+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)
- --> (S2 rmhist p \<leadsto> S3 rmhist p)"
+ \<longrightarrow> (S2 rmhist p \<leadsto> S3 rmhist p)"
by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
(* ------------------------------ State S3 ------------------------------ *)
-lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
+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)$"
apply split_idle
apply (auto dest!: Step1_2_3 [temp_use])
done
-lemma S3RPC_successors: "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+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)
- --> (S4 rmhist p | S6 rmhist p)$"
+ \<longrightarrow> (S4 rmhist p | S6 rmhist p)$"
apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
done
-lemma S3RPC_enabled: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
+lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p & ImpNext p & [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)
apply (blast dest: base_pair)
apply (simp_all add: S_def S3_def)
done
-lemma S3_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+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)
- --> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
+ \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
(* ------------- State S4 -------------------------------------------------- *)
-lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+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)
- --> (S4 rmhist p)$ | (S5 rmhist p)$"
+ \<longrightarrow> (S4 rmhist p)$ | (S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
-lemma S4a_successors: "|- $(S4 rmhist p & 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)
- --> (S4 rmhist p & ires!p = #NotAResult)$
+ \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult)$
| ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
done
-lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult)
+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)
- --> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+ \<longrightarrow> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
by (auto simp: angle_def
dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
-lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult)
+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)
- --> $Enabled (<RNext rmCh mm ires p>_(m p))"
+ \<longrightarrow> $Enabled (<RNext rmCh mm ires p>_(m p))"
apply (auto simp: m_def intro!: RNext_enabled [temp_use])
apply (cut_tac MI_base)
apply (blast dest: base_pair)
apply (simp add: S_def S4_def)
done
-lemma S4a_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+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)
- --> (S4 rmhist p & ires!p = #NotAResult
+ \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult
\<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)"
by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
-lemma S4b_successors: "|- $(S4 rmhist p & ires!p \<noteq> #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)
- --> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (S5 rmhist p)$"
+ \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (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: "|- ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
+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)
- --> (S5 rmhist p)$"
+ \<longrightarrow> (S5 rmhist p)$"
by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
-lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p \<noteq> #NotAResult)
+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)
- --> $Enabled (<MemReturn rmCh ires p>_(m p))"
+ \<longrightarrow> $Enabled (<MemReturn rmCh ires p>_(m p))"
apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
apply (cut_tac MI_base)
apply (blast dest: base_pair)
apply (simp add: S_def S4_def)
done
-lemma S4b_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l))
+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)
- --> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
+ \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
(* ------------------------------ State S5 ------------------------------ *)
-lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> (S5 rmhist p)$ | (S6 rmhist p)$"
+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)$"
apply split_idle
apply (auto dest!: Step1_2_5 [temp_use])
done
-lemma S5RPC_successors: "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+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)
- --> (S6 rmhist p)$"
+ \<longrightarrow> (S6 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
-lemma S5RPC_enabled: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
+lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p & ImpNext p & [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)
apply (blast dest: base_pair)
apply (simp_all add: S_def S5_def)
done
-lemma S5_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+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)
- --> (S5 rmhist p \<leadsto> S6 rmhist p)"
+ \<longrightarrow> (S5 rmhist p \<leadsto> S6 rmhist p)"
by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
(* ------------------------------ State S6 ------------------------------ *)
-lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
+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)$"
apply split_idle
apply (auto dest!: Step1_2_6 [temp_use])
done
lemma S6MClkReply_successors:
- "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+ "\<turnstile> ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
& <MClkReply memCh crCh cst p>_(c p)
- --> (S1 rmhist p)$"
+ \<longrightarrow> (S1 rmhist p)$"
by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
lemma MClkReplyS6:
- "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
+ "\<turnstile> $ImpInv rmhist p & <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 *})
-lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
+lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
apply (cut_tac MI_base)
apply (blast dest: base_pair)
@@ -1099,11 +1099,11 @@
addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
done
-lemma S6_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
+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)
- --> \<box>\<diamond>(S1 rmhist p)"
+ \<longrightarrow> \<box>\<diamond>(S1 rmhist p)"
apply clarsimp
- apply (subgoal_tac "sigma |= \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
+ apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
apply (erule InfiniteEnsures)
apply assumption
apply (tactic {* action_simp_tac @{context} []
@@ -1115,23 +1115,23 @@
(* --------------- aggregate leadsto properties----------------------------- *)
-lemma S5S6LeadstoS6: "sigma |= S5 rmhist p \<leadsto> S6 rmhist p
- ==> sigma |= (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
+lemma S5S6LeadstoS6: "sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p
+ \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
-lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
- sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
- ==> sigma |= (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p
+lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & 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
\<leadsto> S6 rmhist p"
by (auto intro!: LatticeDisjunctionIntro [temp_use]
S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
-lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult
+lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
\<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
- sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
- sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
- ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
- apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) |
+ sigma \<Turnstile> S4 rmhist p & 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
@@ -1144,12 +1144,12 @@
apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
done
-lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma |= S4 rmhist p & ires!p = #NotAResult
+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 |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
- sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
- ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
+ sigma \<Turnstile> S4 rmhist p & 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"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (erule LatticeTriangle2 [temp_use])
apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1157,13 +1157,13 @@
intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
done
-lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p \<leadsto> S3 rmhist p;
- sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma |= S4 rmhist p & ires!p = #NotAResult
+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 |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
- sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
- ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
+ sigma \<Turnstile> S4 rmhist p & 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
\<leadsto> S6 rmhist p"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -1173,14 +1173,14 @@
intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
done
-lemma NotS1LeadstoS6: "[| sigma |= \<box>ImpInv rmhist p;
- sigma |= S2 rmhist p \<leadsto> S3 rmhist p;
- sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
- sigma |= S4 rmhist p & ires!p = #NotAResult
+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 |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
- sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
- ==> sigma |= \<not>S1 rmhist p \<leadsto> S6 rmhist p"
+ sigma \<Turnstile> S4 rmhist p & 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]])
apply assumption+
apply (erule INV_leadsto [temp_use])
@@ -1189,9 +1189,9 @@
apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use])
done
-lemma S1Infinite: "[| sigma |= \<not>S1 rmhist p \<leadsto> S6 rmhist p;
- sigma |= \<box>\<diamond>S6 rmhist p --> \<box>\<diamond>S1 rmhist p |]
- ==> sigma |= \<box>\<diamond>S1 rmhist p"
+lemma S1Infinite: "\<lbrakk> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p;
+ sigma \<Turnstile> \<box>\<diamond>S6 rmhist p \<longrightarrow> \<box>\<diamond>S1 rmhist p \<rbrakk>
+ \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>S1 rmhist p"
apply (rule classical)
apply (tactic {* asm_lr_simp_tac (@{context} addsimps
[temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
@@ -1204,12 +1204,12 @@
a. memory invariant
b. "implementation invariant": always in states S1,...,S6
*)
-lemma Step1_5_1a: "|- IPImp p --> (\<forall>l. \<box>$MemInv mm l)"
+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: "|- Init(ImpInit p & HInit rmhist p) & \<box>(ImpNext p)
+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)
- --> \<box>ImpInv rmhist p"
+ \<longrightarrow> \<box>ImpInv rmhist p"
apply invariant
apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
@@ -1218,25 +1218,25 @@
done
(*** Initialization ***)
-lemma Step1_5_2a: "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"
+lemma Step1_5_2a: "\<turnstile> Init(ImpInit p & 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: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+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))
- --> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+ \<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: "|- IPImp p & HistP rmhist p
- --> Init(ImpInit p & HInit rmhist p)
+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"
apply clarsimp
- apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & \<box> (ImpNext p) &
+ 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 (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
dest!: Step1_5_1b [temp_use])
@@ -1251,10 +1251,10 @@
done
(* The implementation is infinitely often in state S1... *)
-lemma Step1_5_3a: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+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
- --> \<box>\<diamond>S1 rmhist p"
+ \<longrightarrow> \<box>\<diamond>S1 rmhist p"
apply (clarsimp simp: ImpLive_def)
apply (rule S1Infinite)
apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
@@ -1264,18 +1264,18 @@
done
(* ... and therefore satisfies the fairness requirements of the specification *)
-lemma Step1_5_3b: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+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
- --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!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: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+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
- --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!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: "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
+lemma Step1: "\<turnstile> IPImp p & HistP rmhist p --> 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: "|- Write rmCh mm ires p l & ImpNext p
+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
- --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
+ \<longrightarrow> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
apply clarsimp
apply (drule WriteS4 [action_use])
apply assumption
@@ -1296,26 +1296,26 @@
apply (auto simp: square_def dest: S4Write [temp_use])
done
-lemma Step2_2: "|- (\<forall>p. ImpNext p)
+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)
- --> [\<exists>q. Write memCh mm (resbar rmhist) 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])+
apply (force intro!: WriteS4 [temp_use])
apply (auto dest!: Step2_2a [temp_use])
done
-lemma Step2_lemma: "|- \<box>( (\<forall>p. ImpNext p)
+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))
- --> \<box>[\<exists>q. Write memCh mm (resbar rmhist) 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: "|- #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
- --> MSpec memCh mm (resbar rmhist) l"
+lemma Step2: "\<turnstile> #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
+ \<longrightarrow> MSpec memCh mm (resbar rmhist) l"
apply (auto simp: MSpec_def)
apply (force simp: IPImp_def MSpec_def)
apply (auto intro!: Step2_lemma [temp_use] simp: split_box_conj [temp_use] all_box [temp_use])
@@ -1334,12 +1334,12 @@
(* Implementation of internal specification by combination of implementation
and history variable with explicit refinement mapping
*)
-lemma Impl_IUSpec: "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"
+lemma Impl_IUSpec: "\<turnstile> Implementation & 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])
(* The main theorem: introduce hiding and eliminate history variable. *)
-lemma Implementation: "|- Implementation --> USpec memCh"
+lemma Implementation: "\<turnstile> Implementation \<longrightarrow> USpec memCh"
apply clarsimp
apply (frule History [temp_use])
apply (auto simp: USpec_def intro: eexI [temp_use] Impl_IUSpec [temp_use]
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jun 26 14:53:15 2015 +0200
@@ -40,7 +40,7 @@
NotAResultNotOK NotAResultNotBA NotAResultNotMF
NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
-lemma MemValNotAResultE: "[| x : MemVal; (x \<noteq> NotAResult ==> P) |] ==> P"
+lemma MemValNotAResultE: "\<lbrakk> x \<in> MemVal; (x \<noteq> NotAResult \<Longrightarrow> P) \<rbrakk> \<Longrightarrow> P"
using NotAResultNotVal by blast
end
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 14:53:15 2015 +0200
@@ -14,40 +14,40 @@
rather than a single array-valued variable because the
notation gets a little simpler.
*)
-type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
+type_synonym ('a,'r) channel =" (PrIds \<Rightarrow> ('a,'r) chan) stfun"
consts
(* data-level functions *)
- cbit :: "('a,'r) chan => bit"
- rbit :: "('a,'r) chan => bit"
- arg :: "('a,'r) chan => 'a"
- res :: "('a,'r) chan => 'r"
+ cbit :: "('a,'r) chan \<Rightarrow> bit"
+ rbit :: "('a,'r) chan \<Rightarrow> bit"
+ arg :: "('a,'r) chan \<Rightarrow> 'a"
+ res :: "('a,'r) chan \<Rightarrow> 'r"
(* state functions *)
- caller :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
- rtrner :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
+ caller :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'a)) stfun"
+ rtrner :: "('a,'r) channel \<Rightarrow> (PrIds \<Rightarrow> (bit * 'r)) stfun"
(* state predicates *)
- Calling :: "('a,'r) channel => PrIds => stpred"
+ Calling :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> stpred"
(* actions *)
- ACall :: "('a,'r) channel => PrIds => 'a stfun => action"
- AReturn :: "('a,'r) channel => PrIds => 'r stfun => action"
+ ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+ AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
(* temporal formulas *)
- PLegalCaller :: "('a,'r) channel => PrIds => temporal"
- LegalCaller :: "('a,'r) channel => temporal"
- PLegalReturner :: "('a,'r) channel => PrIds => temporal"
- LegalReturner :: "('a,'r) channel => temporal"
+ PLegalCaller :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+ LegalCaller :: "('a,'r) channel \<Rightarrow> temporal"
+ PLegalReturner :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> temporal"
+ LegalReturner :: "('a,'r) channel \<Rightarrow> temporal"
(* slice through array-valued state function *)
- slice :: "('a => 'b) stfun => 'a => 'b stfun"
+ slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
syntax
- "_slice" :: "[lift, 'a] => lift" ("(_!_)" [70,70] 70)
+ "_slice" :: "[lift, 'a] \<Rightarrow> lift" ("(_!_)" [70,70] 70)
- "_Call" :: "['a, 'b, lift] => lift" ("(Call _ _ _)" [90,90,90] 90)
- "_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90)
+ "_Call" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Call _ _ _)" [90,90,90] 90)
+ "_Return" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Return _ _ _)" [90,90,90] 90)
translations
"_slice" == "CONST slice"
@@ -82,10 +82,10 @@
PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
(* Calls and returns change their subchannel *)
-lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"
+lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
by (auto simp: angle_def Call_def caller_def Calling_def)
-lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"
+lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
by (auto simp: angle_def Return_def rtrner_def Calling_def)
end
--- a/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 14:53:15 2015 +0200
@@ -10,22 +10,22 @@
type_synonym rpcSndChType = "(rpcOp,Vals) channel"
type_synonym rpcRcvChType = "memChType"
-type_synonym rpcStType = "(PrIds => rpcState) stfun"
+type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
consts
(* state predicates *)
- RPCInit :: "rpcRcvChType => rpcStType => PrIds => stpred"
+ RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
(* actions *)
- RPCFwd :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
- RPCReject :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
- RPCFail :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
- RPCReply :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
- RPCNext :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
+ RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+ RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
(* temporal *)
- RPCIPSpec :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
- RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
+ RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
+ RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
defs
RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
@@ -81,31 +81,31 @@
unanswered call for that process.
*)
-lemma RPCidle: "|- \<not>$(Calling send p) --> \<not>RPCNext send rcv rst p"
+lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
by (auto simp: Return_def RPC_action_defs)
-lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> \<not>RPCNext send rcv rst p"
+lemma RPCbusy: "\<turnstile> $(Calling rcv p) & $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
by (auto simp: RPC_action_defs)
(* RPC failure actions are visible. *)
-lemma RPCFail_vis: "|- RPCFail send rcv rst p -->
+lemma RPCFail_vis: "\<turnstile> RPCFail send rcv rst p \<longrightarrow>
<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)
-lemma RPCFail_Next_enabled: "|- Enabled (RPCFail send rcv rst p) -->
+lemma RPCFail_Next_enabled: "\<turnstile> Enabled (RPCFail send rcv rst p) \<longrightarrow>
Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
(* Enabledness of some actions *)
-lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
- |- \<not>Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
+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)"
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) ==>
- |- \<not>Calling rcv p & Calling send p & rst!p = #rpcB
- --> Enabled (RPCReply send rcv rst p)"
+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
+ \<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]
[@{thm base_enabled}, @{thm Pair_inject}] 1 *})
--- a/src/HOL/TLA/Memory/RPCParameters.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Fri Jun 26 14:53:15 2015 +0200
@@ -25,8 +25,8 @@
is legal for the receiver (i.e., the memory). This can now be a little
simpler than for the generic RPC component. RelayArg returns an arbitrary
memory call for illegal arguments. *)
- IsLegalRcvArg :: "rpcOp => bool"
- RPCRelayArg :: "rpcOp => memOp"
+ IsLegalRcvArg :: "rpcOp \<Rightarrow> bool"
+ RPCRelayArg :: "rpcOp \<Rightarrow> memOp"
axiomatization where
(* RPCFailure is different from MemVals and exceptions *)
@@ -37,11 +37,11 @@
defs
IsLegalRcvArg_def: "IsLegalRcvArg ra ==
- case ra of (memcall m) => True
- | (othercall v) => False"
+ case ra of (memcall m) \<Rightarrow> True
+ | (othercall v) \<Rightarrow> False"
RPCRelayArg_def: "RPCRelayArg ra ==
- case ra of (memcall m) => m
- | (othercall v) => undefined"
+ case ra of (memcall m) \<Rightarrow> m
+ | (othercall v) \<Rightarrow> undefined"
lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
--- a/src/HOL/TLA/Stfun.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Stfun.thy Fri Jun 26 14:53:15 2015 +0200
@@ -12,7 +12,7 @@
typedecl state
instance state :: world ..
-type_synonym 'a stfun = "state => 'a"
+type_synonym 'a stfun = "state \<Rightarrow> 'a"
type_synonym stpred = "bool stfun"
@@ -30,14 +30,14 @@
identifies (tuples of) "base" state variables in a specification via the
"meta predicate" basevars, which is defined here.
*)
- stvars :: "'a stfun => bool"
+ stvars :: "'a stfun \<Rightarrow> bool"
syntax
- "_PRED" :: "lift => 'a" ("PRED _")
- "_stvars" :: "lift => bool" ("basevars _")
+ "_PRED" :: "lift \<Rightarrow> 'a" ("PRED _")
+ "_stvars" :: "lift \<Rightarrow> bool" ("basevars _")
translations
- "PRED P" => "(P::state => _)"
+ "PRED P" => "(P::state \<Rightarrow> _)"
"_stvars" == "CONST stvars"
defs
@@ -50,13 +50,13 @@
basevars_def: "stvars vs == range vs = UNIV"
-lemma basevars: "\<And>vs. basevars vs ==> \<exists>u. vs u = c"
+lemma basevars: "\<And>vs. basevars vs \<Longrightarrow> \<exists>u. vs u = c"
apply (unfold basevars_def)
apply (rule_tac b = c and f = vs in rangeE)
apply auto
done
-lemma base_pair1: "\<And>x y. basevars (x,y) ==> basevars x"
+lemma base_pair1: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x"
apply (simp (no_asm) add: basevars_def)
apply (rule equalityI)
apply (rule subset_UNIV)
@@ -65,7 +65,7 @@
apply auto
done
-lemma base_pair2: "\<And>x y. basevars (x,y) ==> basevars y"
+lemma base_pair2: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars y"
apply (simp (no_asm) add: basevars_def)
apply (rule equalityI)
apply (rule subset_UNIV)
@@ -74,7 +74,7 @@
apply auto
done
-lemma base_pair: "\<And>x y. basevars (x,y) ==> basevars x & basevars y"
+lemma base_pair: "\<And>x y. basevars (x,y) \<Longrightarrow> basevars x & basevars y"
apply (rule conjI)
apply (erule base_pair1)
apply (erule base_pair2)
@@ -89,7 +89,7 @@
apply auto
done
-lemma baseE: "[| basevars v; \<And>x. v x = c ==> Q |] ==> Q"
+lemma baseE: "\<lbrakk> basevars v; \<And>x. v x = c \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
apply (erule basevars [THEN exE])
apply blast
done
@@ -99,7 +99,7 @@
The following shows that there should not be duplicates in a "stvars" tuple:
*)
-lemma "\<And>v. basevars (v::bool stfun, v) ==> False"
+lemma "\<And>v. basevars (v::bool stfun, v) \<Longrightarrow> False"
apply (erule baseE)
apply (subgoal_tac "(LIFT (v,v)) x = (True, False)")
prefer 2
--- a/src/HOL/TLA/TLA.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/TLA.thy Fri Jun 26 14:53:15 2015 +0200
@@ -11,28 +11,28 @@
consts
(** abstract syntax **)
- Box :: "('w::world) form => temporal"
- Dmd :: "('w::world) form => temporal"
- leadsto :: "['w::world form, 'v::world form] => temporal"
- Stable :: "stpred => temporal"
- WF :: "[action, 'a stfun] => temporal"
- SF :: "[action, 'a stfun] => temporal"
+ Box :: "('w::world) form \<Rightarrow> temporal"
+ Dmd :: "('w::world) form \<Rightarrow> temporal"
+ leadsto :: "['w::world form, 'v::world form] \<Rightarrow> temporal"
+ Stable :: "stpred \<Rightarrow> temporal"
+ WF :: "[action, 'a stfun] \<Rightarrow> temporal"
+ SF :: "[action, 'a stfun] \<Rightarrow> temporal"
(* Quantification over (flexible) state variables *)
- EEx :: "('a stfun => temporal) => temporal" (binder "Eex " 10)
- AAll :: "('a stfun => temporal) => temporal" (binder "Aall " 10)
+ EEx :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal" (binder "Eex " 10)
+ AAll :: "('a stfun \<Rightarrow> temporal) \<Rightarrow> temporal" (binder "Aall " 10)
(** concrete syntax **)
syntax
- "_Box" :: "lift => lift" ("([]_)" [40] 40)
- "_Dmd" :: "lift => lift" ("(<>_)" [40] 40)
- "_leadsto" :: "[lift,lift] => lift" ("(_ ~> _)" [23,22] 22)
- "_stable" :: "lift => lift" ("(stable/ _)")
- "_WF" :: "[lift,lift] => lift" ("(WF'(_')'_(_))" [0,60] 55)
- "_SF" :: "[lift,lift] => lift" ("(SF'(_')'_(_))" [0,60] 55)
+ "_Box" :: "lift \<Rightarrow> lift" ("([]_)" [40] 40)
+ "_Dmd" :: "lift \<Rightarrow> lift" ("(<>_)" [40] 40)
+ "_leadsto" :: "[lift,lift] \<Rightarrow> lift" ("(_ ~> _)" [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] => lift" ("(3EEX _./ _)" [0,10] 10)
- "_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10)
+ "_EEx" :: "[idts, lift] \<Rightarrow> lift" ("(3EEX _./ _)" [0,10] 10)
+ "_AAll" :: "[idts, lift] \<Rightarrow> lift" ("(3AALL _./ _)" [0,10] 10)
translations
"_Box" == "CONST Box"
@@ -54,11 +54,11 @@
"sigma |= AALL x. F" <= "_AAll x F sigma"
syntax (xsymbols)
- "_Box" :: "lift => lift" ("(\<box>_)" [40] 40)
- "_Dmd" :: "lift => lift" ("(\<diamond>_)" [40] 40)
- "_leadsto" :: "[lift,lift] => lift" ("(_ \<leadsto> _)" [23,22] 22)
- "_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
- "_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
+ "_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)
axiomatization where
(* Definitions of derived operators *)
@@ -66,44 +66,44 @@
axiomatization where
boxInit: "\<And>F. TEMP \<box>F == TEMP \<box>Init F" and
- leadsto_def: "\<And>F G. TEMP F \<leadsto> G == TEMP \<box>(Init F --> \<diamond>G)" and
- stable_def: "\<And>P. TEMP stable P == TEMP \<box>($P --> P$)" and
- WF_def: "TEMP WF(A)_v == TEMP \<diamond>\<box> Enabled(<A>_v) --> \<box>\<diamond><A>_v" and
- SF_def: "TEMP SF(A)_v == TEMP \<box>\<diamond> Enabled(<A>_v) --> \<box>\<diamond><A>_v" and
+ leadsto_def: "\<And>F G. TEMP F \<leadsto> G == TEMP \<box>(Init F \<longrightarrow> \<diamond>G)" and
+ stable_def: "\<And>P. TEMP stable P == TEMP \<box>($P \<longrightarrow> P$)" and
+ WF_def: "TEMP WF(A)_v == TEMP \<diamond>\<box> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and
+ SF_def: "TEMP SF(A)_v == TEMP \<box>\<diamond> Enabled(<A>_v) \<longrightarrow> \<box>\<diamond><A>_v" and
aall_def: "TEMP (\<forall>\<forall>x. F x) == TEMP \<not> (\<exists>\<exists>x. \<not> F x)"
axiomatization where
(* Base axioms for raw TLA. *)
- normalT: "\<And>F G. |- \<box>(F --> G) --> (\<box>F --> \<box>G)" and (* polymorphic *)
- reflT: "\<And>F. |- \<box>F --> F" and (* F::temporal *)
- transT: "\<And>F. |- \<box>F --> \<box>\<box>F" and (* polymorphic *)
- linT: "\<And>F G. |- \<diamond>F & \<diamond>G --> (\<diamond>(F & \<diamond>G)) | (\<diamond>(G & \<diamond>F))" and
- discT: "\<And>F. |- \<box>(F --> \<diamond>(\<not>F & \<diamond>F)) --> (F --> \<box>\<diamond>F)" and
- primeI: "\<And>P. |- \<box>P --> Init P`" and
- primeE: "\<And>P F. |- \<box>(Init P --> \<box>F) --> Init P` --> (F --> \<box>F)" and
- indT: "\<And>P F. |- \<box>(Init P & \<not>\<box>F --> Init P` & F) --> Init P --> \<box>F" and
- allT: "\<And>F. |- (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
+ 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
+ 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
+ allT: "\<And>F. \<turnstile> (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
axiomatization where
- necT: "\<And>F. |- F ==> |- \<box>F" (* polymorphic *)
+ necT: "\<And>F. \<turnstile> F \<Longrightarrow> \<turnstile> \<box>F" (* polymorphic *)
axiomatization where
(* Flexible quantification: refinement mappings, history variables *)
- eexI: "|- F x --> (\<exists>\<exists>x. F x)" and
- eexE: "[| sigma |= (\<exists>\<exists>x. F x); basevars vs;
- (\<And>x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
- |] ==> G sigma" and
- history: "|- \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x --> h` = hb x)"
+ eexI: "\<turnstile> F x \<longrightarrow> (\<exists>\<exists>x. F x)" and
+ 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)"
(* Specialize intensional introduction/elimination rules for temporal formulas *)
-lemma tempI [intro!]: "(\<And>sigma. sigma |= (F::temporal)) ==> |- F"
+lemma tempI [intro!]: "(\<And>sigma. sigma \<Turnstile> (F::temporal)) \<Longrightarrow> \<turnstile> F"
apply (rule intI)
apply (erule meta_spec)
done
-lemma tempD [dest]: "|- (F::temporal) ==> sigma |= F"
+lemma tempD [dest]: "\<turnstile> (F::temporal) \<Longrightarrow> sigma \<Turnstile> F"
by (erule intD)
@@ -118,7 +118,7 @@
(rewrite_rule ctxt @{thms action_rews} (th RS @{thm tempD}))
handle THM _ => action_unlift ctxt th;
-(* Turn |- F = G into meta-level rewrite rule F == G *)
+(* Turn \<turnstile> F = G into meta-level rewrite rule F == G *)
val temp_rewrite = int_rewrite
fun temp_use ctxt th =
@@ -176,21 +176,21 @@
lemmas STL2 = reflT
(* The "polymorphic" (generic) variant *)
-lemma STL2_gen: "|- \<box>F --> Init F"
+lemma STL2_gen: "\<turnstile> \<box>F \<longrightarrow> Init F"
apply (unfold boxInit [of F])
apply (rule STL2)
done
-(* see also STL2_pr below: "|- \<box>P --> Init P & Init (P`)" *)
+(* see also STL2_pr below: "\<turnstile> \<box>P \<longrightarrow> Init P & Init (P`)" *)
(* Dual versions for \<diamond> *)
-lemma InitDmd: "|- F --> \<diamond> F"
+lemma InitDmd: "\<turnstile> F \<longrightarrow> \<diamond> F"
apply (unfold dmd_def)
apply (auto dest!: STL2 [temp_use])
done
-lemma InitDmd_gen: "|- Init F --> \<diamond>F"
+lemma InitDmd_gen: "\<turnstile> Init F \<longrightarrow> \<diamond>F"
apply clarsimp
apply (drule InitDmd [temp_use])
apply (simp add: dmdInitD)
@@ -198,17 +198,17 @@
(* ------------------------ STL3 ------------------------------------------- *)
-lemma STL3: "|- (\<box>\<box>F) = (\<box>F)"
+lemma STL3: "\<turnstile> (\<box>\<box>F) = (\<box>F)"
by (auto elim: transT [temp_use] STL2 [temp_use])
(* corresponding elimination rule introduces double boxes:
- [| (sigma |= \<box>F); (sigma |= \<box>\<box>F) ==> PROP W |] ==> PROP W
+ \<lbrakk> (sigma \<Turnstile> \<box>F); (sigma \<Turnstile> \<box>\<box>F) \<Longrightarrow> PROP W \<rbrakk> \<Longrightarrow> PROP W
*)
lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
(* dual versions for \<diamond> *)
-lemma DmdDmd: "|- (\<diamond>\<diamond>F) = (\<diamond>F)"
+lemma DmdDmd: "\<turnstile> (\<diamond>\<diamond>F) = (\<diamond>F)"
by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
@@ -217,8 +217,8 @@
(* ------------------------ STL4 ------------------------------------------- *)
lemma STL4:
- assumes "|- F --> G"
- shows "|- \<box>F --> \<box>G"
+ assumes "\<turnstile> F \<longrightarrow> G"
+ shows "\<turnstile> \<box>F \<longrightarrow> \<box>G"
apply clarsimp
apply (rule normalT [temp_use])
apply (rule assms [THEN necT, temp_use])
@@ -226,15 +226,15 @@
done
(* Unlifted version as an elimination rule *)
-lemma STL4E: "[| sigma |= \<box>F; |- F --> G |] ==> sigma |= \<box>G"
+lemma STL4E: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
by (erule (1) STL4 [temp_use])
-lemma STL4_gen: "|- Init F --> Init G ==> |- \<box>F --> \<box>G"
+lemma STL4_gen: "\<turnstile> Init F \<longrightarrow> Init G \<Longrightarrow> \<turnstile> \<box>F \<longrightarrow> \<box>G"
apply (drule STL4)
apply (simp add: boxInitD)
done
-lemma STL4E_gen: "[| sigma |= \<box>F; |- Init F --> Init G |] ==> sigma |= \<box>G"
+lemma STL4E_gen: "\<lbrakk> sigma \<Turnstile> \<box>F; \<turnstile> Init F \<longrightarrow> Init G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
by (erule (1) STL4_gen [temp_use])
(* see also STL4Edup below, which allows an auxiliary boxed formula:
@@ -245,19 +245,19 @@
(* The dual versions for \<diamond> *)
lemma DmdImpl:
- assumes prem: "|- F --> G"
- shows "|- \<diamond>F --> \<diamond>G"
+ assumes prem: "\<turnstile> F \<longrightarrow> G"
+ shows "\<turnstile> \<diamond>F \<longrightarrow> \<diamond>G"
apply (unfold dmd_def)
apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
done
-lemma DmdImplE: "[| sigma |= \<diamond>F; |- F --> G |] ==> sigma |= \<diamond>G"
+lemma DmdImplE: "\<lbrakk> sigma \<Turnstile> \<diamond>F; \<turnstile> F \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G"
by (erule (1) DmdImpl [temp_use])
(* ------------------------ STL5 ------------------------------------------- *)
-lemma STL5: "|- (\<box>F & \<box>G) = (\<box>(F & G))"
+lemma STL5: "\<turnstile> (\<box>F & \<box>G) = (\<box>(F & G))"
apply auto
- apply (subgoal_tac "sigma |= \<box> (G --> (F & G))")
+ apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F & G))")
apply (erule normalT [temp_use])
apply (fastforce elim!: STL4E [temp_use])+
done
@@ -271,9 +271,9 @@
Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
*)
lemma box_conjE:
- assumes "sigma |= \<box>F"
- and "sigma |= \<box>G"
- and "sigma |= \<box>(F&G) ==> PROP R"
+ assumes "sigma \<Turnstile> \<box>F"
+ and "sigma \<Turnstile> \<box>G"
+ and "sigma \<Turnstile> \<box>(F&G) \<Longrightarrow> PROP R"
shows "PROP R"
by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
@@ -288,7 +288,7 @@
a bit kludgy in order to simulate "double elim-resolution".
*)
-lemma box_thin: "[| sigma |= \<box>F; PROP W |] ==> PROP W" .
+lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
ML {*
fun merge_box_tac i =
@@ -313,21 +313,21 @@
method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
(* rewrite rule to push universal quantification through box:
- (sigma |= \<box>(\<forall>x. F x)) = (\<forall>x. (sigma |= \<box>F x))
+ (sigma \<Turnstile> \<box>(\<forall>x. F x)) = (\<forall>x. (sigma \<Turnstile> \<box>F x))
*)
lemmas all_box = allT [temp_unlift, symmetric]
-lemma DmdOr: "|- (\<diamond>(F | G)) = (\<diamond>F | \<diamond>G)"
+lemma DmdOr: "\<turnstile> (\<diamond>(F | G)) = (\<diamond>F | \<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
-lemma exT: "|- (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))"
+lemma exT: "\<turnstile> (\<exists>x. \<diamond>(F x)) = (\<diamond>(\<exists>x. F x))"
by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
lemmas ex_dmd = exT [temp_unlift, symmetric]
-lemma STL4Edup: "\<And>sigma. [| sigma |= \<box>A; sigma |= \<box>F; |- F & \<box>A --> G |] ==> sigma |= \<box>G"
+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"
apply (erule dup_boxE)
apply merge_box
apply (erule STL4E)
@@ -335,7 +335,7 @@
done
lemma DmdImpl2:
- "\<And>sigma. [| sigma |= \<diamond>F; sigma |= \<box>(F --> G) |] ==> sigma |= \<diamond>G"
+ "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>F; sigma \<Turnstile> \<box>(F \<longrightarrow> G) \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<diamond>G"
apply (unfold dmd_def)
apply auto
apply (erule notE)
@@ -344,10 +344,10 @@
done
lemma InfImpl:
- assumes 1: "sigma |= \<box>\<diamond>F"
- and 2: "sigma |= \<box>G"
- and 3: "|- F & G --> H"
- shows "sigma |= \<box>\<diamond>H"
+ assumes 1: "sigma \<Turnstile> \<box>\<diamond>F"
+ and 2: "sigma \<Turnstile> \<box>G"
+ and 3: "\<turnstile> F & G \<longrightarrow> H"
+ shows "sigma \<Turnstile> \<box>\<diamond>H"
apply (insert 1 2)
apply (erule_tac F = G in dup_boxE)
apply merge_box
@@ -356,7 +356,7 @@
(* ------------------------ STL6 ------------------------------------------- *)
(* Used in the proof of STL6, but useful in itself. *)
-lemma BoxDmd: "|- \<box>F & \<diamond>G --> \<diamond>(\<box>F & G)"
+lemma BoxDmd: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(\<box>F & G)"
apply (unfold dmd_def)
apply clarsimp
apply (erule dup_boxE)
@@ -366,14 +366,14 @@
done
(* weaker than BoxDmd, but more polymorphic (and often just right) *)
-lemma BoxDmd_simple: "|- \<box>F & \<diamond>G --> \<diamond>(F & G)"
+lemma BoxDmd_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(F & G)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
apply (fastforce elim!: notE STL4E [temp_use])
done
-lemma BoxDmd2_simple: "|- \<box>F & \<diamond>G --> \<diamond>(G & F)"
+lemma BoxDmd2_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(G & F)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
@@ -381,15 +381,15 @@
done
lemma DmdImpldup:
- assumes 1: "sigma |= \<box>A"
- and 2: "sigma |= \<diamond>F"
- and 3: "|- \<box>A & F --> G"
- shows "sigma |= \<diamond>G"
+ assumes 1: "sigma \<Turnstile> \<box>A"
+ and 2: "sigma \<Turnstile> \<diamond>F"
+ and 3: "\<turnstile> \<box>A & 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: "|- \<diamond>\<box>F & \<diamond>\<box>G --> \<diamond>\<box>(F & G)"
+lemma STL6: "\<turnstile> \<diamond>\<box>F & \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F & G)"
apply (auto simp: STL5 [temp_rewrite, symmetric])
apply (drule linT [temp_use])
apply assumption
@@ -410,13 +410,13 @@
(* ------------------------ True / False ----------------------------------------- *)
section "Simplification of constants"
-lemma BoxConst: "|- (\<box>#P) = #P"
+lemma BoxConst: "\<turnstile> (\<box>#P) = #P"
apply (rule tempI)
apply (cases P)
apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps)
done
-lemma DmdConst: "|- (\<diamond>#P) = #P"
+lemma DmdConst: "\<turnstile> (\<diamond>#P) = #P"
apply (unfold dmd_def)
apply (cases P)
apply (simp_all add: BoxConst [try_rewrite])
@@ -428,10 +428,10 @@
(* ------------------------ Further rewrites ----------------------------------------- *)
section "Further rewrites"
-lemma NotBox: "|- (\<not>\<box>F) = (\<diamond>\<not>F)"
+lemma NotBox: "\<turnstile> (\<not>\<box>F) = (\<diamond>\<not>F)"
by (simp add: dmd_def)
-lemma NotDmd: "|- (\<not>\<diamond>F) = (\<box>\<not>F)"
+lemma NotDmd: "\<turnstile> (\<not>\<diamond>F) = (\<box>\<not>F)"
by (simp add: dmd_def)
(* These are not declared by default, because they could be harmful,
@@ -441,10 +441,10 @@
NotBox [temp_unlift, THEN eq_reflection]
NotDmd [temp_unlift, THEN eq_reflection]
-lemma BoxDmdBox: "|- (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
+lemma BoxDmdBox: "\<turnstile> (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
apply (auto dest!: STL2 [temp_use])
apply (rule ccontr)
- apply (subgoal_tac "sigma |= \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
+ apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
apply (erule thin_rl)
apply auto
apply (drule STL6 [temp_use])
@@ -453,7 +453,7 @@
apply (simp_all add: more_temp_simps1)
done
-lemma DmdBoxDmd: "|- (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
+lemma DmdBoxDmd: "\<turnstile> (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
apply (unfold dmd_def)
apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
done
@@ -463,11 +463,11 @@
(* ------------------------ Miscellaneous ----------------------------------- *)
-lemma BoxOr: "\<And>sigma. [| sigma |= \<box>F | \<box>G |] ==> sigma |= \<box>(F | G)"
+lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F | \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F | G)"
by (fastforce elim!: STL4E [temp_use])
(* "persistently implies infinitely often" *)
-lemma DBImplBD: "|- \<diamond>\<box>F --> \<box>\<diamond>F"
+lemma DBImplBD: "\<turnstile> \<diamond>\<box>F \<longrightarrow> \<box>\<diamond>F"
apply clarsimp
apply (rule ccontr)
apply (simp add: more_temp_simps2)
@@ -476,13 +476,13 @@
apply simp
done
-lemma BoxDmdDmdBox: "|- \<box>\<diamond>F & \<diamond>\<box>G --> \<box>\<diamond>(F & G)"
+lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F & \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F & G)"
apply clarsimp
apply (rule ccontr)
apply (unfold more_temp_simps2)
apply (drule STL6 [temp_use])
apply assumption
- apply (subgoal_tac "sigma |= \<diamond>\<box>\<not>F")
+ apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<not>F")
apply (force simp: dmd_def)
apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
done
@@ -494,11 +494,11 @@
section "priming"
(* ------------------------ TLA2 ------------------------------------------- *)
-lemma STL2_pr: "|- \<box>P --> Init P & Init P`"
+lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P & Init P`"
by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
(* Auxiliary lemma allows priming of boxed actions *)
-lemma BoxPrime: "|- \<box>P --> \<box>($P & P$)"
+lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P & P$)"
apply clarsimp
apply (erule dup_boxE)
apply (unfold boxInit_act)
@@ -507,18 +507,18 @@
done
lemma TLA2:
- assumes "|- $P & P$ --> A"
- shows "|- \<box>P --> \<box>A"
+ assumes "\<turnstile> $P & P$ \<longrightarrow> A"
+ shows "\<turnstile> \<box>P \<longrightarrow> \<box>A"
apply clarsimp
apply (drule BoxPrime [temp_use])
apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use]
elim!: STL4E [temp_use])
done
-lemma TLA2E: "[| sigma |= \<box>P; |- $P & P$ --> A |] ==> sigma |= \<box>A"
+lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P & P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
by (erule (1) TLA2 [temp_use])
-lemma DmdPrime: "|- (\<diamond>P`) --> (\<diamond>P)"
+lemma DmdPrime: "\<turnstile> (\<diamond>P`) \<longrightarrow> (\<diamond>P)"
apply (unfold dmd_def)
apply (fastforce elim!: TLA2E [temp_use])
done
@@ -529,13 +529,13 @@
section "stable, invariant"
lemma ind_rule:
- "[| sigma |= \<box>H; sigma |= Init P; |- H --> (Init P & \<not>\<box>F --> Init(P`) & F) |]
- ==> sigma |= \<box>F"
+ "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P & \<not>\<box>F \<longrightarrow> Init(P`) & F) \<rbrakk>
+ \<Longrightarrow> sigma \<Turnstile> \<box>F"
apply (rule indT [temp_use])
apply (erule (2) STL4E)
done
-lemma box_stp_act: "|- (\<box>$P) = (\<box>P)"
+lemma box_stp_act: "\<turnstile> (\<box>$P) = (\<box>P)"
by (simp add: boxInit_act Init_simps)
lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
@@ -544,7 +544,7 @@
lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
lemma INV1:
- "|- (Init P) --> (stable P) --> \<box>P"
+ "\<turnstile> (Init P) \<longrightarrow> (stable P) \<longrightarrow> \<box>P"
apply (unfold stable_def boxInit_stp boxInit_act)
apply clarsimp
apply (erule ind_rule)
@@ -552,23 +552,23 @@
done
lemma StableT:
- "\<And>P. |- $P & A --> P` ==> |- \<box>A --> stable P"
+ "\<And>P. \<turnstile> $P & A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
apply (unfold stable_def)
apply (fastforce elim!: STL4E [temp_use])
done
-lemma Stable: "[| sigma |= \<box>A; |- $P & A --> P` |] ==> sigma |= stable P"
+lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P & A --> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
by (erule (1) StableT [temp_use])
(* Generalization of INV1 *)
-lemma StableBox: "|- (stable P) --> \<box>(Init P --> \<box>P)"
+lemma StableBox: "\<turnstile> (stable P) \<longrightarrow> \<box>(Init P \<longrightarrow> \<box>P)"
apply (unfold stable_def)
apply clarsimp
apply (erule dup_boxE)
apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
done
-lemma DmdStable: "|- (stable P) & \<diamond>P --> \<diamond>\<box>P"
+lemma DmdStable: "\<turnstile> (stable P) & \<diamond>P \<longrightarrow> \<diamond>\<box>P"
apply clarsimp
apply (rule DmdImpl2)
prefer 2
@@ -579,7 +579,7 @@
(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
ML {*
-(* inv_tac reduces goals of the form ... ==> sigma |= \<box>P *)
+(* inv_tac reduces goals of the form ... \<Longrightarrow> sigma \<Turnstile> \<box>P *)
fun inv_tac ctxt =
SELECT_GOAL
(EVERY
@@ -589,7 +589,7 @@
TRYALL (etac @{thm Stable})]);
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
- in simple cases it may be able to handle goals like |- MyProg --> \<box>Inv.
+ in simple cases it may be able to handle goals like \<turnstile> MyProg \<longrightarrow> \<box>Inv.
In these simple cases the simplifier seems to be more useful than the
auto-tactic, which applies too much propositional logic and simplifies
too late.
@@ -609,7 +609,7 @@
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
*}
-lemma unless: "|- \<box>($P --> P` | Q`) --> (stable P) | \<diamond>Q"
+lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` | Q`) \<longrightarrow> (stable P) | \<diamond>Q"
apply (unfold dmd_def)
apply (clarsimp dest!: BoxPrime [temp_use])
apply merge_box
@@ -622,28 +622,28 @@
section "recursive expansions"
(* Recursive expansions of \<box> and \<diamond> for state predicates *)
-lemma BoxRec: "|- (\<box>P) = (Init P & \<box>P`)"
+lemma BoxRec: "\<turnstile> (\<box>P) = (Init P & \<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: "|- (\<diamond>P) = (Init P | \<diamond>P`)"
+lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P | \<diamond>P`)"
apply (unfold dmd_def BoxRec [temp_rewrite])
apply (auto simp: Init_simps)
done
-lemma DmdRec2: "\<And>sigma. [| sigma |= \<diamond>P; sigma |= \<box>\<not>P` |] ==> sigma |= Init P"
+lemma DmdRec2: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<diamond>P; sigma \<Turnstile> \<box>\<not>P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> Init P"
apply (force simp: DmdRec [temp_rewrite] dmd_def)
done
-lemma InfinitePrime: "|- (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
+lemma InfinitePrime: "\<turnstile> (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
apply auto
apply (rule classical)
apply (rule DBImplBD [temp_use])
- apply (subgoal_tac "sigma |= \<diamond>\<box>P")
+ apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>P")
apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
- apply (subgoal_tac "sigma |= \<diamond>\<box> (\<diamond>P & \<box>\<not>P`)")
+ apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P & \<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 +651,7 @@
done
lemma InfiniteEnsures:
- "[| sigma |= \<box>N; sigma |= \<box>\<diamond>A; |- A & N --> P` |] ==> sigma |= \<box>\<diamond>P"
+ "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A & N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
apply (unfold InfinitePrime [temp_rewrite])
apply (rule InfImpl)
apply assumption+
@@ -661,32 +661,32 @@
section "fairness"
(* alternative definitions of fairness *)
-lemma WF_alt: "|- 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) | \<box>\<diamond><A>_v)"
apply (unfold WF_def dmd_def)
apply fastforce
done
-lemma SF_alt: "|- 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) | \<box>\<diamond><A>_v)"
apply (unfold SF_def dmd_def)
apply fastforce
done
(* theorems to "box" fairness conditions *)
-lemma BoxWFI: "|- WF(A)_v --> \<box>WF(A)_v"
+lemma BoxWFI: "\<turnstile> WF(A)_v \<longrightarrow> \<box>WF(A)_v"
by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
-lemma WF_Box: "|- (\<box>WF(A)_v) = WF(A)_v"
+lemma WF_Box: "\<turnstile> (\<box>WF(A)_v) = WF(A)_v"
by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
-lemma BoxSFI: "|- SF(A)_v --> \<box>SF(A)_v"
+lemma BoxSFI: "\<turnstile> SF(A)_v \<longrightarrow> \<box>SF(A)_v"
by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
-lemma SF_Box: "|- (\<box>SF(A)_v) = SF(A)_v"
+lemma SF_Box: "\<turnstile> (\<box>SF(A)_v) = SF(A)_v"
by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
-lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
+lemma SFImplWF: "\<turnstile> SF(A)_v \<longrightarrow> WF(A)_v"
apply (unfold SF_def WF_def)
apply (fastforce dest!: DBImplBD [temp_use])
done
@@ -702,28 +702,28 @@
section "\<leadsto>"
-lemma leadsto_init: "|- (Init F) & (F \<leadsto> G) --> \<diamond>G"
+lemma leadsto_init: "\<turnstile> (Init F) & (F \<leadsto> G) \<longrightarrow> \<diamond>G"
apply (unfold leadsto_def)
apply (auto dest!: STL2 [temp_use])
done
-(* |- F & (F \<leadsto> G) --> \<diamond>G *)
+(* \<turnstile> F & (F \<leadsto> G) \<longrightarrow> \<diamond>G *)
lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
-lemma streett_leadsto: "|- (\<box>\<diamond>Init F --> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))"
+lemma streett_leadsto: "\<turnstile> (\<box>\<diamond>Init F \<longrightarrow> \<box>\<diamond>G) = (\<diamond>(F \<leadsto> G))"
apply (unfold leadsto_def)
apply auto
apply (simp add: more_temp_simps)
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
- apply (subgoal_tac "sigma |= \<box>\<diamond>\<diamond>G")
+ apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond>\<diamond>G")
apply (simp add: more_temp_simps)
apply (drule BoxDmdDmdBox [temp_use])
apply assumption
apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
done
-lemma leadsto_infinite: "|- \<box>\<diamond>F & (F \<leadsto> G) --> \<box>\<diamond>G"
+lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F & (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)
@@ -732,18 +732,18 @@
(* In particular, strong fairness is a Streett condition. The following
rules are sometimes easier to use than WF2 or SF2 below.
*)
-lemma leadsto_SF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> SF(A)_v"
+lemma leadsto_SF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> SF(A)_v"
apply (unfold SF_def)
apply (clarsimp elim!: leadsto_infinite [temp_use])
done
-lemma leadsto_WF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> WF(A)_v"
+lemma leadsto_WF: "\<turnstile> (Enabled(<A>_v) \<leadsto> <A>_v) \<longrightarrow> WF(A)_v"
by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use])
(* introduce an invariant into the proof of a leadsto assertion.
- \<box>I --> ((P \<leadsto> Q) = (P /\ I \<leadsto> Q))
+ \<box>I \<longrightarrow> ((P \<leadsto> Q) = (P /\ I \<leadsto> Q))
*)
-lemma INV_leadsto: "|- \<box>I & (P & I \<leadsto> Q) --> (P \<leadsto> Q)"
+lemma INV_leadsto: "\<turnstile> \<box>I & (P & I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4Edup)
@@ -751,24 +751,24 @@
apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
done
-lemma leadsto_classical: "|- (Init F & \<box>\<not>G \<leadsto> G) --> (F \<leadsto> G)"
+lemma leadsto_classical: "\<turnstile> (Init F & \<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: "|- (F \<leadsto> #False) = (\<box>~F)"
+lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>~F)"
apply (unfold leadsto_def)
apply (simp add: boxNotInitD)
done
-lemma leadsto_exists: "|- ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))"
+lemma leadsto_exists: "\<turnstile> ((\<exists>x. F x) \<leadsto> G) = (\<forall>x. (F x \<leadsto> G))"
apply (unfold leadsto_def)
apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use])
done
(* basic leadsto properties, cf. Unity *)
-lemma ImplLeadsto_gen: "|- \<box>(Init F --> Init G) --> (F \<leadsto> G)"
+lemma ImplLeadsto_gen: "\<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)"
apply (unfold leadsto_def)
apply (auto intro!: InitDmd_gen [temp_use]
elim!: STL4E_gen [temp_use] simp: Init_simps)
@@ -777,19 +777,19 @@
lemmas ImplLeadsto =
ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
-lemma ImplLeadsto_simple: "\<And>F G. |- F --> G ==> |- F \<leadsto> G"
+lemma ImplLeadsto_simple: "\<And>F G. \<turnstile> F \<longrightarrow> G \<Longrightarrow> \<turnstile> F \<leadsto> G"
by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
lemma EnsuresLeadsto:
- assumes "|- A & $P --> Q`"
- shows "|- \<box>A --> (P \<leadsto> Q)"
+ assumes "\<turnstile> A & $P \<longrightarrow> Q`"
+ shows "\<turnstile> \<box>A \<longrightarrow> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply (clarsimp elim!: INV_leadsto [temp_use])
apply (erule STL4E_gen)
apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use])
done
-lemma EnsuresLeadsto2: "|- \<box>($P --> Q`) --> (P \<leadsto> Q)"
+lemma EnsuresLeadsto2: "\<turnstile> \<box>($P \<longrightarrow> Q`) \<longrightarrow> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4E_gen)
@@ -797,15 +797,15 @@
done
lemma ensures:
- assumes 1: "|- $P & N --> P` | Q`"
- and 2: "|- ($P & N) & A --> Q`"
- shows "|- \<box>N & \<box>(\<box>P --> \<diamond>A) --> (P \<leadsto> Q)"
+ 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)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4Edup)
apply assumption
apply clarsimp
- apply (subgoal_tac "sigmaa |= \<box>($P --> P` | Q`) ")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` | 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 +815,16 @@
done
lemma ensures_simple:
- "[| |- $P & N --> P` | Q`;
- |- ($P & N) & A --> Q`
- |] ==> |- \<box>N & \<box>\<diamond>A --> (P \<leadsto> Q)"
+ "\<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)"
apply clarsimp
apply (erule (2) ensures [temp_use])
apply (force elim!: STL4E [temp_use])
done
lemma EnsuresInfinite:
- "[| sigma |= \<box>\<diamond>P; sigma |= \<box>A; |- A & $P --> Q` |] ==> sigma |= \<box>\<diamond>Q"
+ "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A & $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
apply (erule leadsto_infinite [temp_use])
apply (erule EnsuresLeadsto [temp_use])
apply assumption
@@ -834,64 +834,64 @@
(*** Gronning's lattice rules (taken from TLP) ***)
section "Lattice rules"
-lemma LatticeReflexivity: "|- F \<leadsto> F"
+lemma LatticeReflexivity: "\<turnstile> F \<leadsto> F"
apply (unfold leadsto_def)
apply (rule necT InitDmd_gen)+
done
-lemma LatticeTransitivity: "|- (G \<leadsto> H) & (F \<leadsto> G) --> (F \<leadsto> H)"
+lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) & (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
apply (unfold leadsto_def)
apply clarsimp
- apply (erule dup_boxE) (* \<box>\<box>(Init G --> H) *)
+ apply (erule dup_boxE) (* \<box>\<box>(Init G \<longrightarrow> H) *)
apply merge_box
apply (clarsimp elim!: STL4E [temp_use])
apply (rule dup_dmdD)
- apply (subgoal_tac "sigmaa |= \<diamond>Init G")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<diamond>Init G")
apply (erule DmdImpl2)
apply assumption
apply (simp add: dmdInitD)
done
-lemma LatticeDisjunctionElim1: "|- (F | G \<leadsto> H) --> (F \<leadsto> H)"
+lemma LatticeDisjunctionElim1: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
apply (unfold leadsto_def)
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunctionElim2: "|- (F | G \<leadsto> H) --> (G \<leadsto> H)"
+lemma LatticeDisjunctionElim2: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
apply (unfold leadsto_def)
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunctionIntro: "|- (F \<leadsto> H) & (G \<leadsto> H) --> (F | G \<leadsto> H)"
+lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) & (G \<leadsto> H) \<longrightarrow> (F | G \<leadsto> H)"
apply (unfold leadsto_def)
apply clarsimp
apply merge_box
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunction: "|- (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
+lemma LatticeDisjunction: "\<turnstile> (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
by (auto intro: LatticeDisjunctionIntro [temp_use]
LatticeDisjunctionElim1 [temp_use]
LatticeDisjunctionElim2 [temp_use])
-lemma LatticeDiamond: "|- (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) --> (A \<leadsto> D)"
+lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma |= (B | C) \<leadsto> D")
+ apply (subgoal_tac "sigma \<Turnstile> (B | C) \<leadsto> D")
apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
done
-lemma LatticeTriangle: "|- (A \<leadsto> D | B) & (B \<leadsto> D) --> (A \<leadsto> D)"
+lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D | B) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma |= (D | B) \<leadsto> D")
+ apply (subgoal_tac "sigma \<Turnstile> (D | B) \<leadsto> D")
apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use])
apply assumption
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
done
-lemma LatticeTriangle2: "|- (A \<leadsto> B | D) & (B \<leadsto> D) --> (A \<leadsto> D)"
+lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B | D) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma |= B | D \<leadsto> D")
+ apply (subgoal_tac "sigma \<Turnstile> B | D \<leadsto> D")
apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use])
apply assumption
apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
@@ -901,10 +901,10 @@
section "Fairness rules"
lemma WF1:
- "[| |- $P & N --> P` | Q`;
- |- ($P & N) & <A>_v --> Q`;
- |- $P & N --> $(Enabled(<A>_v)) |]
- ==> |- \<box>N & WF(A)_v --> (P \<leadsto> Q)"
+ "\<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)"
apply (clarsimp dest!: BoxWFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule (1) STL4Edup)
@@ -917,10 +917,10 @@
(* Sometimes easier to use; designed for action B rather than state predicate Q *)
lemma WF_leadsto:
- assumes 1: "|- N & $P --> $Enabled (<A>_v)"
- and 2: "|- N & <A>_v --> B"
- and 3: "|- \<box>(N & [~A]_v) --> stable P"
- shows "|- \<box>N & WF(A)_v --> (P \<leadsto> B)"
+ 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)"
apply (unfold leadsto_def)
apply (clarsimp dest!: BoxWFI [temp_use])
apply (erule (1) STL4Edup)
@@ -939,10 +939,10 @@
done
lemma SF1:
- "[| |- $P & N --> P` | Q`;
- |- ($P & N) & <A>_v --> Q`;
- |- \<box>P & \<box>N & \<box>F --> \<diamond>Enabled(<A>_v) |]
- ==> |- \<box>N & SF(A)_v & \<box>F --> (P \<leadsto> Q)"
+ "\<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)"
apply (clarsimp dest!: BoxSFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule_tac F = F in dup_boxE)
@@ -957,11 +957,11 @@
done
lemma WF2:
- assumes 1: "|- N & <B>_f --> <M>_g"
- and 2: "|- $P & P` & <N & A>_f --> B"
- and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
- and 4: "|- \<box>(N & [~B]_f) & WF(A)_f & \<box>F & \<diamond>\<box>Enabled(<M>_g) --> \<diamond>\<box>P"
- shows "|- \<box>N & WF(A)_f & \<box>F --> WF(M)_g"
+ 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"
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 +970,7 @@
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
apply (rule classical)
- apply (subgoal_tac "sigmaa |= \<diamond> (($P & P` & N) & <A>_f)")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <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])
@@ -979,8 +979,8 @@
apply assumption+
apply (drule STL6 [temp_use])
apply assumption
- apply (erule_tac V = "sigmaa |= \<diamond>\<box>P" in thin_rl)
- apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
+ 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 merge_temp_box
@@ -995,11 +995,11 @@
done
lemma SF2:
- assumes 1: "|- N & <B>_f --> <M>_g"
- and 2: "|- $P & P` & <N & A>_f --> B"
- and 3: "|- P & Enabled(<M>_g) --> Enabled(<A>_f)"
- and 4: "|- \<box>(N & [~B]_f) & SF(A)_f & \<box>F & \<box>\<diamond>Enabled(<M>_g) --> \<diamond>\<box>P"
- shows "|- \<box>N & SF(A)_f & \<box>F --> SF(M)_g"
+ 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"
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,14 +1008,14 @@
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
apply (rule classical)
- apply (subgoal_tac "sigmaa |= \<diamond> (($P & P` & N) & <A>_f)")
+ apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <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])
apply merge_act_box
apply (frule 4 [temp_use])
apply assumption+
- apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
+ 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)
@@ -1037,8 +1037,8 @@
lemma wf_leadsto:
assumes 1: "wf r"
- and 2: "\<And>x. sigma |= F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y)) "
- shows "sigma |= F x \<leadsto> G"
+ and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y)) "
+ shows "sigma \<Turnstile> F x \<leadsto> G"
apply (rule 1 [THEN wf_induct])
apply (rule LatticeTriangle [temp_use])
apply (rule 2)
@@ -1049,10 +1049,10 @@
done
(* If r is well-founded, state function v cannot decrease forever *)
-lemma wf_not_box_decrease: "\<And>r. wf r ==> |- \<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v"
+lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
apply clarsimp
apply (rule ccontr)
- apply (subgoal_tac "sigma |= (\<exists>x. v=#x) \<leadsto> #False")
+ apply (subgoal_tac "sigma \<Turnstile> (\<exists>x. v=#x) \<leadsto> #False")
apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]])
apply (force simp: Init_defs)
apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
@@ -1061,7 +1061,7 @@
apply (auto simp: square_def angle_def)
done
-(* "wf r ==> |- \<diamond>\<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v" *)
+(* "wf r \<Longrightarrow> \<turnstile> \<diamond>\<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v" *)
lemmas wf_not_dmd_box_decrease =
wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
@@ -1070,14 +1070,14 @@
*)
lemma wf_box_dmd_decrease:
assumes 1: "wf r"
- shows "|- \<box>\<diamond>((v`, $v) : #r) --> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
+ shows "\<turnstile> \<box>\<diamond>((v`, $v) : #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
apply clarsimp
apply (rule ccontr)
apply (simp add: not_angle [try_rewrite] more_temp_simps)
apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]])
apply (drule BoxDmdDmdBox [temp_use])
apply assumption
- apply (subgoal_tac "sigma |= \<box>\<diamond> ((#False) ::action)")
+ apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> ((#False) ::action)")
apply force
apply (erule STL4E)
apply (rule DmdImpl)
@@ -1087,9 +1087,9 @@
(* In particular, for natural numbers, if n decreases infinitely often
then it has to increase infinitely often.
*)
-lemma nat_box_dmd_decrease: "\<And>n::nat stfun. |- \<box>\<diamond>(n` < $n) --> \<box>\<diamond>($n < n`)"
+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 |= \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
+ apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
apply (erule thin_rl)
apply (erule STL4E)
apply (rule DmdImpl)
@@ -1106,11 +1106,11 @@
lemma aallI:
assumes 1: "basevars vs"
- and 2: "(\<And>x. basevars (x,vs) ==> sigma |= F x)"
- shows "sigma |= (\<forall>\<forall>x. F x)"
+ and 2: "(\<And>x. basevars (x,vs) \<Longrightarrow> sigma \<Turnstile> F x)"
+ shows "sigma \<Turnstile> (\<forall>\<forall>x. F x)"
by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use])
-lemma aallE: "|- (\<forall>\<forall>x. F x) --> F x"
+lemma aallE: "\<turnstile> (\<forall>\<forall>x. F x) \<longrightarrow> F x"
apply (unfold aall_def)
apply clarsimp
apply (erule contrapos_np)
@@ -1119,18 +1119,18 @@
(* monotonicity of quantification *)
lemma eex_mono:
- assumes 1: "sigma |= \<exists>\<exists>x. F x"
- and 2: "\<And>x. sigma |= F x --> G x"
- shows "sigma |= \<exists>\<exists>x. G x"
+ assumes 1: "sigma \<Turnstile> \<exists>\<exists>x. F x"
+ and 2: "\<And>x. sigma \<Turnstile> F x \<longrightarrow> G x"
+ shows "sigma \<Turnstile> \<exists>\<exists>x. G x"
apply (rule unit_base [THEN 1 [THEN eexE]])
apply (rule eexI [temp_use])
apply (erule 2 [unfolded intensional_rews, THEN mp])
done
lemma aall_mono:
- assumes 1: "sigma |= \<forall>\<forall>x. F(x)"
- and 2: "\<And>x. sigma |= F(x) --> G(x)"
- shows "sigma |= \<forall>\<forall>x. G(x)"
+ assumes 1: "sigma \<Turnstile> \<forall>\<forall>x. F(x)"
+ and 2: "\<And>x. sigma \<Turnstile> F(x) \<longrightarrow> G(x)"
+ shows "sigma \<Turnstile> \<forall>\<forall>x. G(x)"
apply (rule unit_base [THEN aallI])
apply (rule 2 [unfolded intensional_rews, THEN mp])
apply (rule 1 [THEN aallE [temp_use]])
@@ -1138,12 +1138,12 @@
(* Derived history introduction rule *)
lemma historyI:
- assumes 1: "sigma |= Init I"
- and 2: "sigma |= \<box>N"
+ assumes 1: "sigma \<Turnstile> Init I"
+ and 2: "sigma \<Turnstile> \<box>N"
and 3: "basevars vs"
- and 4: "\<And>h. basevars(h,vs) ==> |- I & h = ha --> HI h"
- and 5: "\<And>h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)"
- shows "sigma |= \<exists>\<exists>h. Init (HI h) & \<box>(HN h)"
+ and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I & 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)"
apply (rule history [temp_use, THEN eexE])
apply (rule 3)
apply (rule eexI [temp_use])
@@ -1161,7 +1161,7 @@
example of a history variable: existence of a clock
*)
-lemma "|- \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
+lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
apply (rule tempI)
apply (rule historyI)
apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+