--- a/src/HOL/TLA/Action.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Action.thy Fri Jun 26 11:44:22 2015 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/TLA/Action.thy
+(* Title: HOL/TLA/Action.thy
Author: Stephan Merz
Copyright: 1998 University of Munich
*)
@@ -66,9 +66,9 @@
defs
square_def: "ACT [A]_v == ACT (A | unchanged v)"
- angle_def: "ACT <A>_v == ACT (A & ~ unchanged v)"
+ angle_def: "ACT <A>_v == ACT (A & \<not> unchanged v)"
- enabled_def: "s |= Enabled A == EX u. (s,u) |= A"
+ enabled_def: "s |= Enabled A == \<exists>u. (s,u) |= A"
(* The following assertion specializes "intI" for any world type
@@ -76,7 +76,7 @@
*)
lemma actionI [intro!]:
- assumes "!!s t. (s,t) |= A"
+ assumes "\<And>s t. (s,t) |= A"
shows "|- A"
apply (rule assms intI prod.induct)+
done
@@ -87,11 +87,11 @@
lemma pr_rews [int_rewrite]:
"|- (#c)` = #c"
- "!!f. |- f<x>` = f<x` >"
- "!!f. |- f<x,y>` = f<x`,y` >"
- "!!f. |- f<x,y,z>` = f<x`,y`,z` >"
- "|- (! x. P x)` = (! x. (P x)`)"
- "|- (? x. P x)` = (? x. (P x)`)"
+ "\<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)`)"
by (rule actionI, unfold unl_after intensional_rews, rule refl)+
@@ -137,7 +137,7 @@
lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [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)"
apply (unfold square_def action_rews)
@@ -145,34 +145,34 @@
apply simp_all
done
-lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
+lemma squareCI [intro]: "[| v t \<noteq> v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
apply (unfold square_def action_rews)
apply (rule disjCI)
apply (erule (1) meta_mp)
done
-lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
+lemma angleI [intro]: "\<And>s t. [| A (s,t); v t \<noteq> v s |] ==> (s,t) |= <A>_v"
by (simp add: angle_def)
-lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
+lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t \<noteq> v s |] ==> R |] ==> R"
apply (unfold angle_def action_rews)
apply (erule conjE)
apply simp
done
lemma square_simulation:
- "!!f. [| |- unchanged f & ~B --> unchanged g;
- |- A & ~unchanged g --> B
+ "\<And>f. [| |- unchanged f & \<not>B --> unchanged g;
+ |- A & \<not>unchanged g --> B
|] ==> |- [A]_f --> [B]_g"
apply clarsimp
apply (erule squareE)
apply (auto simp add: square_def)
done
-lemma not_square: "|- (~ [A]_v) = <~A>_v"
+lemma not_square: "|- (\<not> [A]_v) = <\<not>A>_v"
by (auto simp: square_def angle_def)
-lemma not_angle: "|- (~ <A>_v) = [~A]_v"
+lemma not_angle: "|- (\<not> <A>_v) = [\<not>A]_v"
by (auto simp: square_def angle_def)
@@ -181,13 +181,13 @@
lemma enabledI: "|- A --> $Enabled A"
by (auto simp add: enabled_def)
-lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
+lemma enabledE: "[| s |= Enabled A; \<And>u. A (s,u) ==> Q |] ==> Q"
apply (unfold enabled_def)
apply (erule exE)
apply simp
done
-lemma notEnabledD: "|- ~$Enabled G --> ~ G"
+lemma notEnabledD: "|- \<not>$Enabled G --> \<not> G"
by (auto simp add: enabled_def)
(* Monotonicity *)
@@ -203,7 +203,7 @@
(* stronger variant *)
lemma enabled_mono2:
assumes min: "s |= Enabled F"
- and maj: "!!t. F (s,t) ==> G (s,t)"
+ and maj: "\<And>t. F (s,t) ==> G (s,t)"
shows "s |= Enabled G"
apply (rule min [THEN enabledE])
apply (rule enabledI [action_use])
@@ -239,13 +239,13 @@
apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
done
-lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"
+lemma enabled_ex: "|- 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; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
+ "[| basevars vs; \<exists>c. \<forall>u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
apply (erule exE)
apply (erule baseE)
apply (rule enabledI [action_use])
--- a/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 11:44:22 2015 +0200
@@ -21,24 +21,24 @@
defs
BInit_def: "BInit ic q oc == PRED q = #[]"
- Enq_def: "Enq ic q oc == ACT (ic$ ~= $ic)
+ Enq_def: "Enq ic q oc == ACT (ic$ \<noteq> $ic)
& (q$ = $q @ [ ic$ ])
& (oc$ = $oc)"
- Deq_def: "Deq ic q oc == ACT ($q ~= #[])
+ Deq_def: "Deq ic q oc == ACT ($q \<noteq> #[])
& (oc$ = hd< $q >)
& (q$ = tl< $q >)
& (ic$ = $ic)"
Next_def: "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)"
IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc)
- & [][Next ic q oc]_(ic,q,oc)
+ & \<box>[Next ic q oc]_(ic,q,oc)
& WF(Deq ic q oc)_(ic,q,oc)"
- Buffer_def: "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)"
+ Buffer_def: "Buffer ic oc == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
(* ---------------------------- Data lemmas ---------------------------- *)
(*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*)
-lemma tl_not_self [simp]: "xs ~= [] ==> tl xs ~= xs"
+lemma tl_not_self [simp]: "xs \<noteq> [] ==> tl xs \<noteq> xs"
by (auto simp: neq_Nil_conv)
@@ -52,14 +52,14 @@
(* Enabling condition for dequeue -- NOT NEEDED *)
lemma Deq_enabled:
- "!!q. basevars (ic,q,oc) ==> |- Enabled (<Deq ic q oc>_(ic,q,oc)) = (q ~= #[])"
+ "\<And>q. basevars (ic,q,oc) ==> |- 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 ~= #[])"
+ "|- Enabled (<Deq ic q oc>_(ic,q,oc)) --> (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:07:04 2015 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 11:44:22 2015 +0200
@@ -37,7 +37,7 @@
& (out$ = $out)" and
DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)" and
DBuffer_def: "DBuffer == TEMP Init DBInit
- & [][DBNext]_(inp,mid,out,q1,q2)
+ & \<box>[DBNext]_(inp,mid,out,q1,q2)
& WF(DBDeq)_(inp,mid,out,q1,q2)
& WF(DBPass)_(inp,mid,out,q1,q2)"
@@ -72,7 +72,7 @@
done
lemma DBDeq_enabled:
- "|- Enabled (<DBDeq>_(inp,mid,out,q1,q2)) = (q2 ~= #[])"
+ "|- 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)
@@ -82,7 +82,7 @@
by (auto simp: angle_def DBPass_def Deq_def)
lemma DBPass_enabled:
- "|- Enabled (<DBPass>_(inp,mid,out,q1,q2)) = (q1 ~= #[])"
+ "|- 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)
@@ -90,15 +90,15 @@
(* The plan for proving weak fairness at the higher level is to prove
- (0) DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out))
+ (0) DBuffer => (Enabled (Deq inp qc out) \<leadsto> (Deq inp qc out))
which is in turn reduced to the two leadsto conditions
- (1) DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= [])
- (2) DBuffer => (q2 ~= [] ~> DBDeq)
+ (1) DBuffer => (Enabled (Deq inp qc out) \<leadsto> q2 \<noteq> [])
+ (2) DBuffer => (q2 \<noteq> [] \<leadsto> DBDeq)
and the fact that DBDeq implies <Deq inp qc out>_(inp,qc,out)
- (and therefore DBDeq ~> <Deq inp qc out>_(inp,qc,out) trivially holds).
+ (and therefore DBDeq \<leadsto> <Deq inp qc out>_(inp,qc,out) trivially holds).
Condition (1) is reduced to
- (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= [])
+ (1a) DBuffer => (qc \<noteq> [] /\ q2 = [] \<leadsto> q2 \<noteq> [])
by standard leadsto rules (leadsto_classical) and rule Deq_enabledE.
Both (1a) and (2) are proved from DBuffer's WF conditions by standard
@@ -109,8 +109,8 @@
*)
(* Condition (1a) *)
-lemma DBFair_1a: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
- --> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])"
+lemma DBFair_1a: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
+ --> (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: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
- --> (Enabled (<Deq inp qc out>_(inp,qc,out)) ~> q2 ~= #[])"
+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> #[])"
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: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)
- --> (q2 ~= #[] ~> DBDeq)"
+lemma DBFair_2: "|- \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)
+ --> (q2 \<noteq> #[] \<leadsto> DBDeq)"
apply (rule WF_leadsto)
apply (force simp: DBDeq_enabled [temp_use])
apply (force simp: angle_def)
@@ -139,7 +139,7 @@
done
(* High-level fairness *)
-lemma DBFair: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)
+lemma DBFair: "|- \<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)"
apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
--- a/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 11:44:22 2015 +0200
@@ -48,7 +48,7 @@
InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0" and
M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y" and
M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x" and
- Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
+ Phi_def: "Phi == TEMP Init InitPhi & \<box>[M1 | M2]_(x,y)
& WF(M1)_(x,y) & WF(M2)_(x,y)" and
(* definitions for low-level program *)
@@ -69,7 +69,7 @@
N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)" and
N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)" and
Psi_def: "Psi == TEMP Init InitPsi
- & [][N1 | N2]_(x,y,sem,pc1,pc2)
+ & \<box>[N1 | N2]_(x,y,sem,pc1,pc2)
& SF(N1)_(x,y,sem,pc1,pc2)
& SF(N2)_(x,y,sem,pc1,pc2)" and
@@ -110,7 +110,7 @@
lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$"
by (auto simp: PsiInv_defs)
-lemma PsiInv: "|- Psi --> []PsiInv"
+lemma PsiInv: "|- Psi --> \<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,7 +123,7 @@
More realistic examples require user guidance anyway.
*)
-lemma "|- Psi --> []PsiInv"
+lemma "|- Psi --> \<box>PsiInv"
by (auto_invariant simp: PsiInv_defs Psi_defs)
@@ -132,7 +132,7 @@
lemma Init_sim: "|- Psi --> Init InitPhi"
by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
-lemma Step_sim: "|- Psi --> [][M1 | M2]_(x,y)"
+lemma Step_sim: "|- Psi --> \<box>[M1 | M2]_(x,y)"
by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
@@ -154,7 +154,7 @@
the auxiliary lemmas are very similar.
*)
-lemma Stuck_at_b: "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
+lemma Stuck_at_b: "|- \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) --> 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))"
@@ -166,14 +166,14 @@
done
lemma g1_leadsto_a1:
- "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True
- --> (pc1 = #g ~> pc1 = #a)"
+ "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True
+ --> (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 |- []A --> <>Enabled B to |- A --> Enabled B *)
+ (* reduce |- \<box>A --> \<diamond>Enabled B to |- A --> Enabled B *)
apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
dest!: STL2_gen [temp_use] simp: Init_def)
done
@@ -188,8 +188,8 @@
done
lemma g2_leadsto_a2:
- "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
- --> (pc2 = #g ~> pc2 = #a)"
+ "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
+ --> (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})
@@ -207,8 +207,8 @@
done
lemma b2_leadsto_g2:
- "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
- --> (pc2 = #b ~> pc2 = #g)"
+ "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True
+ --> (pc2 = #b \<leadsto> pc2 = #g)"
apply (rule SF1)
apply (tactic
{* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
@@ -220,18 +220,18 @@
(* Combine above lemmas: the second component will eventually reach pc2 = a *)
lemma N2_leadsto_a:
- "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
- --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #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)"
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
apply (rule LatticeReflexivity [temp_use])
apply (rule LatticeTransitivity [temp_use])
apply (auto intro!: b2_leadsto_g2 [temp_use] g2_leadsto_a2 [temp_use])
done
-(* Get rid of disjunction on the left-hand side of ~> above. *)
+(* Get rid of disjunction on the left-hand side of \<leadsto> above. *)
lemma N2_live:
- "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)
- --> <>(pc2 = #a)"
+ "|- \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)
+ --> \<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
@@ -249,9 +249,9 @@
done
lemma a1_leadsto_b1:
- "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
- --> (pc1 = #a ~> pc1 = #b)"
+ "|- \<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)"
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: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
- --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)"
+lemma N1_leadsto_b: "|- \<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)"
apply (auto intro!: LatticeDisjunctionIntro [temp_use])
apply (rule LatticeReflexivity [temp_use])
apply (rule LatticeTransitivity [temp_use])
@@ -273,9 +273,9 @@
simp: split_box_conj)
done
-lemma N1_live: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
- --> <>(pc1 = #b)"
+lemma N1_live: "|- \<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)"
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
@@ -291,8 +291,8 @@
(* Now assemble the bits and pieces to prove that Psi is fair. *)
-lemma Fair_M1_lemma: "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))
- & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)
+lemma Fair_M1_lemma: "|- \<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)"
apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
(* action premises *)
--- a/src/HOL/TLA/Init.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Init.thy Fri Jun 26 11:44:22 2015 +0200
@@ -36,9 +36,9 @@
Init_def: "sigma |= Init F == (first_world sigma) |= F"
defs (overloaded)
- fw_temp_def: "first_world == %sigma. sigma"
+ fw_temp_def: "first_world == \<lambda>sigma. sigma"
fw_stp_def: "first_world == st1"
- fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)"
+ fw_act_def: "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
lemma const_simps [int_rewrite, simp]:
"|- (Init #True) = #True"
@@ -46,14 +46,14 @@
by (auto simp: Init_def)
lemma Init_simps1 [int_rewrite]:
- "!!F. |- (Init ~F) = (~ Init F)"
+ "\<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 (!x. F x)) = (!x. (Init F x))"
- "|- (Init (? x. F x)) = (? x. (Init F x))"
- "|- (Init (?! x. F x)) = (?! x. (Init F x))"
+ "|- (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))"
by (auto simp: Init_def)
lemma Init_stp_act: "|- (Init $P) = (Init P)"
--- a/src/HOL/TLA/Intensional.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Jun 26 11:44:22 2015 +0200
@@ -39,7 +39,7 @@
"" :: "var => lift" ("_")
"_applC" :: "[lift, cargs] => lift" ("(1_/ _)" [1000, 1000] 999)
"" :: "lift => lift" ("'(_')")
- "_lambda" :: "[idts, 'a] => lift" ("(3%_./ _)" [0, 3] 3)
+ "_lambda" :: "[idts, 'a] => lift" ("(3\<lambda>_./ _)" [0, 3] 3)
"_constrain" :: "[lift, type] => lift" ("(_::_)" [4, 0] 3)
"" :: "lift => liftargs" ("_")
"_liftargs" :: "[lift, liftargs] => liftargs" ("_,/ _")
@@ -155,29 +155,17 @@
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50)
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50)
-syntax (HTML output)
- "_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)
- "_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)
-
defs
- Valid_def: "|- A == ALL w. w |= A"
+ Valid_def: "|- A == \<forall>w. w |= 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 |= ALL x. A x == ALL x. (w |= A x)"
- unl_Rex: "w |= EX x. A x == EX x. (w |= A x)"
- unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)"
+ 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)"
subsection {* Lemmas and tactics for "intensional" logics. *}
@@ -192,7 +180,7 @@
apply (erule spec)
done
-lemma intI [intro!]: "(!!w. w |= A) ==> |- A"
+lemma intI [intro!]: "(\<And>w. w |= A) ==> |- A"
apply (unfold Valid_def)
apply (rule allI)
apply (erule meta_spec)
@@ -207,21 +195,21 @@
lemma int_simps:
"|- (x=x) = #True"
- "|- (~#True) = #False" "|- (~#False) = #True" "|- (~~ P) = P"
- "|- ((~P) = P) = #False" "|- (P = (~P)) = #False"
- "|- (P ~= Q) = (P = (~Q))"
+ "|- (\<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) = (~P)" "|- (P --> ~P) = (~P)"
+ "|- (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 & ~P) = #False" "|- (~P & 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 | ~P) = #True" "|- (~P | P) = #True"
- "|- (! x. P) = P" "|- (? x. P) = P"
- "|- (~Q --> ~P) = (P --> Q)"
+ "|- (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))"
apply (unfold Valid_def intensional_rews)
apply blast+
@@ -296,10 +284,10 @@
attribute_setup int_use =
{* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
-lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
+lemma Not_Rall: "|- (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
by (simp add: Valid_def)
-lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)"
+lemma Not_Rex: "|- (\<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:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 11:44:22 2015 +0200
@@ -16,7 +16,7 @@
definition
(* state predicates *)
MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred"
- where "MClkInit rcv cst p = PRED (cst!p = #clkA & ~Calling rcv p)"
+ where "MClkInit rcv cst p = PRED (cst!p = #clkA & \<not>Calling rcv p)"
definition
(* actions *)
@@ -39,7 +39,7 @@
definition
MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
where "MClkReply send rcv cst p = ACT
- ~$Calling rcv p
+ \<not>$Calling rcv p
& $(cst!p) = #clkB
& Return send p MClkReplyVal<res<rcv!p>>
& (cst!p)$ = #clkA
@@ -57,13 +57,13 @@
MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
where "MClkIPSpec send rcv cst p = TEMP
Init MClkInit rcv cst p
- & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
+ & \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
& WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
& SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
definition
MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
- where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)"
+ where "MClkISpec send rcv cst = TEMP (\<forall>p. MClkIPSpec send rcv cst p)"
lemmas MC_action_defs =
MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def
@@ -73,17 +73,17 @@
(* The Clerk engages in an action for process p only if there is an outstanding,
unanswered call for that process.
*)
-lemma MClkidle: "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"
+lemma MClkidle: "|- \<not>$Calling send p & $(cst!p) = #clkA --> \<not>MClkNext send rcv cst p"
by (auto simp: Return_def MC_action_defs)
-lemma MClkbusy: "|- $Calling rcv p --> ~MClkNext send rcv cst p"
+lemma MClkbusy: "|- $Calling rcv p --> \<not>MClkNext send rcv cst p"
by (auto simp: Call_def MC_action_defs)
(* Enabledness of actions *)
-lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>
- |- Calling send p & ~Calling rcv p & cst!p = #clkA
+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)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
@{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
@@ -97,8 +97,8 @@
<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: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>
- |- Calling send p & ~Calling rcv p & cst!p = #clkB
+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))"
apply (tactic {* action_simp_tac @{context}
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
@@ -107,7 +107,7 @@
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
done
-lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
+lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> \<not>MClkRetry send rcv cst p"
by (auto simp: MClkReply_def MClkRetry_def)
end
--- a/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 11:44:22 2015 +0200
@@ -63,31 +63,31 @@
#l : #MemLoc & ((rs!p)$ = $(mm!l))"
(* a read that raises BadArg *)
BadRead_def: "BadRead mm rs p l == ACT
- #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
+ #l \<notin> #MemLoc & ((rs!p)$ = #BadArg)"
(* the read action with l visible *)
ReadInner_def: "ReadInner ch mm rs p l == ACT
$(RdRequest ch p l)
& (GoodRead mm rs p l | BadRead mm rs p l)
& unchanged (rtrner ch ! p)"
(* the read action with l quantified *)
- Read_def: "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
+ Read_def: "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
(* similar definitions for the write action *)
GoodWrite_def: "GoodWrite mm rs p l v == ACT
#l : #MemLoc & #v : #MemVal
& ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
BadWrite_def: "BadWrite mm rs p l v == ACT
- ~ (#l : #MemLoc & #v : #MemVal)
+ \<not> (#l : #MemLoc & #v : #MemVal)
& ((rs!p)$ = #BadArg) & unchanged (mm!l)"
WriteInner_def: "WriteInner ch mm rs p l v == ACT
$(WrRequest ch p l v)
& (GoodWrite mm rs p l v | BadWrite mm rs p l v)
& unchanged (rtrner ch ! p)"
- Write_def: "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
+ Write_def: "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
(* the return action *)
MemReturn_def: "MemReturn ch rs p == ACT
- ( ($(rs!p) ~= #NotAResult)
+ ( ($(rs!p) \<noteq> #NotAResult)
& ((rs!p)$ = #NotAResult)
& Return ch p (rs!p))"
@@ -99,33 +99,33 @@
(* next-state relations for reliable / unreliable memory *)
RNext_def: "RNext ch mm rs p == ACT
( Read ch mm rs p
- | (EX l. Write ch mm rs p l)
+ | (\<exists>l. Write ch mm rs p l)
| MemReturn ch rs p)"
UNext_def: "UNext ch mm rs p == ACT
(RNext ch mm rs p | MemFail ch rs p)"
RPSpec_def: "RPSpec ch mm rs p == TEMP
Init(PInit rs p)
- & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+ & \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
& WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
& WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
UPSpec_def: "UPSpec ch mm rs p == TEMP
Init(PInit rs p)
- & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+ & \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
& WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
& WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
MSpec_def: "MSpec ch mm rs l == TEMP
Init(MInit mm l)
- & [][ EX p. Write ch mm rs p l ]_(mm!l)"
+ & \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
IRSpec_def: "IRSpec ch mm rs == TEMP
- (ALL p. RPSpec ch mm rs p)
- & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
+ (\<forall>p. RPSpec ch mm rs p)
+ & (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l)"
IUSpec_def: "IUSpec ch mm rs == TEMP
- (ALL p. UPSpec ch mm rs p)
- & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
+ (\<forall>p. UPSpec ch mm rs p)
+ & (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l)"
- RSpec_def: "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
- USpec_def: "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
+ 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"
@@ -146,15 +146,15 @@
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 --> [](MemInv mm l)"
+lemma MemoryInvariant: "|- MSpec ch mm rs l --> \<box>(MemInv mm l)"
by (auto_invariant simp: RM_temp_defs RM_action_defs)
(* The invariant is trivial for non-locations *)
-lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
+lemma NonMemLocInvariant: "|- #l \<notin> #MemLoc --> \<box>(MemInv mm l)"
by (auto simp: MemInv_def intro!: necT [temp_use])
lemma MemoryInvariantAll:
- "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))"
+ "|- (\<forall>l. #l : #MemLoc --> MSpec ch mm rs l) --> (\<forall>l. \<box>(MemInv mm l))"
apply clarify
apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
done
@@ -164,7 +164,7 @@
We need this only for the reliable memory.
*)
-lemma Memoryidle: "|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
+lemma Memoryidle: "|- \<not>$(Calling ch p) --> \<not> RNext ch mm rs p"
by (auto simp: Return_def RM_action_defs)
(* Enabledness conditions *)
@@ -172,8 +172,8 @@
lemma MemReturn_change: "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
by (force simp: MemReturn_def angle_def)
-lemma MemReturn_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
- |- Calling ch p & (rs!p ~= #NotAResult)
+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))"
apply (tactic
{* action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
@@ -182,14 +182,14 @@
@{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
done
-lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
+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)"
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: "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==>
+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)"
apply (case_tac "l:MemLoc & v:MemVal")
@@ -197,18 +197,18 @@
intro!: exI elim!: base_enabled [temp_use])+
done
-lemma ReadResult: "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
+lemma ReadResult: "|- Read ch mm rs p & (\<forall>l. $(MemInv mm l)) --> (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)` ~= #NotAResult"
+lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` \<noteq> #NotAResult"
by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)
-lemma ReturnNotReadWrite: "|- (ALL l. $MemInv mm l) & MemReturn ch rs p
- --> ~ Read ch mm rs p & (ALL l. ~ Write ch mm rs p l)"
+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)"
by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l)
- & Enabled (Read ch mm rs p | (? l. Write ch mm rs p 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))"
by (force simp: RNext_def angle_def elim!: enabled_mono2
dest: ReadResult [temp_use] WriteResult [temp_use])
@@ -217,8 +217,8 @@
(* 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: "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==>
- |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l)
+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))"
apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
apply (case_tac "arg (ch w p)")
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 11:44:22 2015 +0200
@@ -63,7 +63,7 @@
definition
(* the environment action *)
ENext :: "PrIds => action"
- where "ENext p = ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
+ where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
definition
@@ -83,24 +83,24 @@
definition
HistP :: "histType => PrIds => temporal"
where "HistP rmhist p = (TEMP Init HInit rmhist p
- & [][HNext rmhist p]_(c p,r p,m p, rmhist!p))"
+ & \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
definition
Hist :: "histType => temporal"
- where "Hist rmhist = TEMP (ALL p. HistP rmhist p)"
+ where "Hist rmhist = TEMP (\<forall>p. HistP rmhist p)"
definition
(* the implementation *)
IPImp :: "PrIds => temporal"
- where "IPImp p = (TEMP ( Init ~Calling memCh p & [][ENext p]_(e p)
+ 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
- & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
+ & (\<forall>l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
definition
ImpInit :: "PrIds => stpred"
- where "ImpInit p = PRED ( ~Calling memCh p
+ where "ImpInit p = PRED ( \<not>Calling memCh p
& MClkInit crCh cst p
& RPCInit rmCh rst p
& PInit ires p)"
@@ -122,7 +122,7 @@
definition
Implementation :: "temporal"
- where "Implementation = (TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
+ where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) & \<box>[ENext p]_(e p))
& MClkISpec memCh crCh cst
& RPCISpec crCh rmCh rst
& IRSpec rmCh mm ires))"
@@ -139,11 +139,11 @@
Calling memCh p = #ecalling
& Calling crCh p = #ccalling
& (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
- & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
+ & (\<not> #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
& Calling rmCh p = #rcalling
& (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
- & (~ #rcalling --> ires!p = #NotAResult)
- & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
+ & (\<not> #rcalling --> ires!p = #NotAResult)
+ & (\<not> #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
& cst!p = #cs
& rst!p = #rs
& (rmhist!p = #hs1 | rmhist!p = #hs2)
@@ -241,9 +241,9 @@
section "History variable"
-lemma HistoryLemma: "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p)
- --> (EEX rmhist. Init(ALL p. HInit rmhist p)
- & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
+lemma HistoryLemma: "|- Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
+ --> (\<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)
apply assumption+
@@ -255,7 +255,7 @@
apply (erule fun_cong)
done
-lemma History: "|- Implementation --> (EEX rmhist. Hist rmhist)"
+lemma History: "|- Implementation --> (\<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 ~= RPCFailure"
+lemma MVOKBAnotRF: "MVOKBA x ==> x \<noteq> RPCFailure"
apply (unfold MVOKBA_def)
apply auto
done
(* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
-lemma MVOKBARFnotNR: "MVOKBARF x ==> x ~= NotAResult"
+lemma MVOKBARFnotNR: "MVOKBARF x ==> 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 & ~S2 rmhist p & ~S3 rmhist p &
- ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
+lemma S1_excl: "|- S1 rmhist p --> 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 & ~S1 rmhist p"
+lemma S2_excl: "|- S2 rmhist p --> 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 & ~S1 rmhist p & ~S2 rmhist p"
+lemma S3_excl: "|- S3 rmhist p --> 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 & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p"
+lemma S4_excl: "|- S4 rmhist p --> 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 & ~S1 rmhist p & ~S2 rmhist p
- & ~S3 rmhist p & ~S4 rmhist p"
+lemma S5_excl: "|- S5 rmhist p --> 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 & ~S1 rmhist p & ~S2 rmhist p
- & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p"
+lemma S6_excl: "|- S6 rmhist p --> 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) --> ~ENext p"
+lemma Envbusy: "|- $(Calling memCh p) --> \<not>ENext p"
by (auto simp: ENext_def Call_def)
(* ==================== Lemmas about the implementation's states ==================== *)
@@ -447,7 +447,7 @@
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
- & HNext rmhist p & (!l. $MemInv mm l)
+ & HNext rmhist p & (\<forall>l. $MemInv mm l)
--> (S4 rmhist p)$ & unchanged (rmhist!p)"
by (auto simp: Read_def dest!: S4ReadInner [temp_use])
@@ -563,7 +563,7 @@
(* 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
- & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist 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)"
apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
(map (temp_elim @{context})
@@ -573,7 +573,7 @@
done
lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
+ & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
--> (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}]) []
@@ -584,7 +584,7 @@
done
lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist 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))
| ((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}]) []
@@ -596,10 +596,10 @@
done
lemma Step1_2_4: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & ~unchanged (e p, c p, r p, m p, rmhist!p)
- & $S4 rmhist p & (!l. $(MemInv mm l))
+ & \<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))
- | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & 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}]) []
(map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
@@ -610,7 +610,7 @@
done
lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist 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))
| ((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}]) []
@@ -621,7 +621,7 @@
done
lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
- & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist 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))
| ((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}]) []
@@ -694,7 +694,7 @@
done
lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
- & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l))
+ & unchanged (e p, c p, r p, rmhist!p) & (\<forall>l. $(MemInv mm l))
--> Read memCh mm (resbar rmhist) p"
by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
@@ -816,7 +816,7 @@
(* 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: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
+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)"
apply (split_idle simp: square_def)
@@ -850,7 +850,7 @@
done
lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (!l. $(MemInv mm l))
+ & (\<forall>l. $(MemInv mm l))
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
apply clarsimp
apply (rule unchanged_safeI)
@@ -900,23 +900,23 @@
*)
lemma S1_RNextdisabled: "|- S1 rmhist p -->
- ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
+ \<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 -->
- ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
+ \<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: "|- []<>S1 rmhist p
+lemma RNext_fair: "|- \<box>\<diamond>S1 rmhist p
--> 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: "|- []<>S1 rmhist p
+lemma Return_fair: "|- \<box>\<diamond>S1 rmhist p
--> 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])
@@ -942,9 +942,9 @@
apply (simp_all add: S_def S2_def)
done
-lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+lemma S2_live: "|- \<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 ~> S3 rmhist p)"
+ --> (S2 rmhist p \<leadsto> S3 rmhist p)"
by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
(* ------------------------------ State S3 ------------------------------ *)
@@ -969,15 +969,15 @@
apply (simp_all add: S_def S3_def)
done
-lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+lemma S3_live: "|- \<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 ~> S4 rmhist p | S6 rmhist p)"
+ --> (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)
- & (ALL l. $MemInv mm l)
+ & (\<forall>l. $MemInv mm l)
--> (S4 rmhist p)$ | (S5 rmhist p)$"
apply split_idle
apply (auto dest!: Step1_2_4 [temp_use])
@@ -986,22 +986,22 @@
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
+ & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l)
--> (S4 rmhist p & ires!p = #NotAResult)$
- | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
+ | ((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)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l))
+ & 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 ~= #NotAResult) | S5 rmhist p)$"
+ --> ((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)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
+ & 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))"
apply (auto simp: m_def intro!: RNext_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1009,30 +1009,30 @@
apply (simp add: S_def S4_def)
done
-lemma S4a_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
+lemma S4a_live: "|- \<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
- ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
+ \<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 ~= #NotAResult)
- & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
- --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
+lemma S4b_successors: "|- $(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)$"
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 ~= #NotAResult)
+lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
& ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
+ & (\<forall>l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
--> (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 ~= #NotAResult)
+lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p \<noteq> #NotAResult)
& ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
- & (ALL l. $MemInv mm l)
+ & (\<forall>l. $MemInv mm l)
--> $Enabled (<MemReturn rmCh ires p>_(m p))"
apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
apply (cut_tac MI_base)
@@ -1040,9 +1040,9 @@
apply (simp add: S_def S4_def)
done
-lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))
+lemma S4b_live: "|- \<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 ~= #NotAResult ~> S5 rmhist p)"
+ --> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
(* ------------------------------ State S5 ------------------------------ *)
@@ -1066,9 +1066,9 @@
apply (simp_all add: S_def S5_def)
done
-lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+lemma S5_live: "|- \<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 ~> S6 rmhist p)"
+ --> (S5 rmhist p \<leadsto> S6 rmhist p)"
by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
(* ------------------------------ State S6 ------------------------------ *)
@@ -1099,11 +1099,11 @@
addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
done
-lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
- & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)
- --> []<>(S1 rmhist p)"
+lemma S6_live: "|- \<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)"
apply clarsimp
- apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
+ apply (subgoal_tac "sigma |= \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
apply (erule InfiniteEnsures)
apply assumption
apply (tactic {* action_simp_tac @{context} []
@@ -1115,26 +1115,26 @@
(* --------------- aggregate leadsto properties----------------------------- *)
-lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p
- ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
+lemma S5S6LeadstoS6: "sigma |= S5 rmhist p \<leadsto> S6 rmhist p
+ ==> sigma |= (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 ~= #NotAResult ~> S5 rmhist p;
- sigma |= S5 rmhist p ~> S6 rmhist p |]
- ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p
- ~> S6 rmhist p"
+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
+ \<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
- ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
- sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
- sigma |= S5 rmhist p ~> S6 rmhist p |]
- ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
+ \<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) |
- (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p")
+ (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 ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in
+ (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p)" in
LatticeTransitivity [temp_use])
apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
apply (rule LatticeDisjunctionIntro [temp_use])
@@ -1144,12 +1144,12 @@
apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
done
-lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
+lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
sigma |= S4 rmhist p & ires!p = #NotAResult
- ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
- sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
- sigma |= S5 rmhist p ~> S6 rmhist p |]
- ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
+ \<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"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (erule LatticeTriangle2 [temp_use])
apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1157,14 +1157,14 @@
intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
done
-lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p;
- sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
+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
- ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
- sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
- sigma |= S5 rmhist p ~> S6 rmhist p |]
+ \<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
- ~> S6 rmhist p"
+ \<leadsto> S6 rmhist p"
apply (rule LatticeDisjunctionIntro [temp_use])
apply (rule LatticeTransitivity [temp_use])
prefer 2 apply assumption
@@ -1173,14 +1173,14 @@
intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
done
-lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p;
- sigma |= S2 rmhist p ~> S3 rmhist p;
- sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
+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
- ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
- sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
- sigma |= S5 rmhist p ~> S6 rmhist p |]
- ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
+ \<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"
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 |= ~S1 rmhist p ~> S6 rmhist p;
- sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
- ==> sigma |= []<>S1 rmhist p"
+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"
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 --> (ALL l. []$MemInv mm l)"
+lemma Step1_5_1a: "|- IPImp p --> (\<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) & [](ImpNext p)
- & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
- --> []ImpInv rmhist p"
+lemma Step1_5_1b: "|- 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"
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]
@@ -1222,9 +1222,9 @@
by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3 [temp_use])
(*** step simulation ***)
-lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
- & $ImpInv rmhist p & (!l. $MemInv mm l))
- --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma Step1_5_2b: "|- \<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)"
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])
@@ -1232,12 +1232,12 @@
(*** Liveness ***)
lemma GoodImpl: "|- IPImp p & HistP rmhist p
--> Init(ImpInit p & HInit rmhist p)
- & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & [](ALL l. $MemInv mm l) & []($ImpInv 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) & [] (ImpNext p) &
- [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)")
+ apply (subgoal_tac "sigma |= 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])
apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
@@ -1251,10 +1251,10 @@
done
(* The implementation is infinitely often in state S1... *)
-lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & [](ALL l. $MemInv mm l)
- & []($ImpInv rmhist p) & ImpLive p
- --> []<>S1 rmhist p"
+lemma Step1_5_3a: "|- \<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"
apply (clarsimp simp: ImpLive_def)
apply (rule S1Infinite)
apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
@@ -1264,13 +1264,13 @@
done
(* ... and therefore satisfies the fairness requirements of the specification *)
-lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3b: "|- \<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)"
by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
-lemma Step1_5_3c: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3c: "|- \<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)"
by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
@@ -1296,25 +1296,25 @@
apply (auto simp: square_def dest: S4Write [temp_use])
done
-lemma Step2_2: "|- (ALL p. ImpNext p)
- & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & (ALL p. $ImpInv rmhist p)
- & [EX q. Write rmCh mm ires q l]_(mm!l)
- --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
+lemma Step2_2: "|- (\<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)"
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: "|- []( (ALL p. ImpNext p)
- & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
- & (ALL p. $ImpInv rmhist p)
- & [EX q. Write rmCh mm ires q l]_(mm!l))
- --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
+lemma Step2_lemma: "|- \<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)"
by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
-lemma Step2: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p)
+lemma Step2: "|- #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
--> MSpec memCh mm (resbar rmhist) l"
apply (auto simp: MSpec_def)
apply (force simp: IPImp_def MSpec_def)
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jun 26 11:44:22 2015 +0200
@@ -27,20 +27,20 @@
axiomatization where
(* basic assumptions about the above constants and predicates *)
- BadArgNoMemVal: "BadArg ~: MemVal" and
- MemFailNoMemVal: "MemFailure ~: MemVal" and
+ BadArgNoMemVal: "BadArg \<notin> MemVal" and
+ MemFailNoMemVal: "MemFailure \<notin> MemVal" and
InitValMemVal: "InitVal : MemVal" and
- NotAResultNotVal: "NotAResult ~: MemVal" and
- NotAResultNotOK: "NotAResult ~= OK" and
- NotAResultNotBA: "NotAResult ~= BadArg" and
- NotAResultNotMF: "NotAResult ~= MemFailure"
+ NotAResultNotVal: "NotAResult \<notin> MemVal" and
+ NotAResultNotOK: "NotAResult \<noteq> OK" and
+ NotAResultNotBA: "NotAResult \<noteq> BadArg" and
+ NotAResultNotMF: "NotAResult \<noteq> MemFailure"
lemmas [simp] =
BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal
NotAResultNotOK NotAResultNotBA NotAResultNotMF
NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric]
-lemma MemValNotAResultE: "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P"
+lemma MemValNotAResultE: "[| x : MemVal; (x \<noteq> NotAResult ==> P) |] ==> P"
using NotAResultNotVal by blast
end
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 11:44:22 2015 +0200
@@ -58,23 +58,23 @@
defs
slice_def: "(PRED (x!i)) s == x s i"
- caller_def: "caller ch == %s p. (cbit (ch s p), arg (ch s p))"
- rtrner_def: "rtrner ch == %s p. (rbit (ch s p), res (ch s p))"
+ caller_def: "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))"
+ rtrner_def: "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))"
- Calling_def: "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >"
- Call_def: "(ACT Call ch p v) == ACT ~ $Calling ch p
- & (cbit<ch!p>$ ~= $rbit<ch!p>)
+ Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
+ Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p
+ & (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
& (arg<ch!p>$ = $v)"
Return_def: "(ACT Return ch p v) == ACT $Calling ch p
& (rbit<ch!p>$ = $cbit<ch!p>)
& (res<ch!p>$ = $v)"
PLegalCaller_def: "PLegalCaller ch p == TEMP
- Init(~ Calling ch p)
- & [][ ? a. Call ch p a ]_((caller ch)!p)"
- LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
+ Init(\<not> Calling ch p)
+ & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+ LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
PLegalReturner_def: "PLegalReturner ch p == TEMP
- [][ ? v. Return ch p v ]_((rtrner ch)!p)"
- LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
+ \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
+ LegalReturner_def: "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
declare slice_def [simp]
--- a/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 11:44:22 2015 +0200
@@ -28,7 +28,7 @@
RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
defs
- RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
+ RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
RPCFwd_def: "RPCFwd send rcv rst p == ACT
$(Calling send p)
@@ -40,18 +40,18 @@
RPCReject_def: "RPCReject send rcv rst p == ACT
$(rst!p) = # rpcA
- & ~IsLegalRcvArg<arg<$(send!p)>>
+ & \<not>IsLegalRcvArg<arg<$(send!p)>>
& Return send p #BadCall
& unchanged ((rst!p), (caller rcv!p))"
RPCFail_def: "RPCFail send rcv rst p == ACT
- ~$(Calling rcv p)
+ \<not>$(Calling rcv p)
& Return send p #RPCFailure
& (rst!p)$ = #rpcA
& unchanged (caller rcv!p)"
RPCReply_def: "RPCReply send rcv rst p == ACT
- ~$(Calling rcv p)
+ \<not>$(Calling rcv p)
& $(rst!p) = #rpcB
& Return send p res<rcv!p>
& (rst!p)$ = #rpcA
@@ -65,10 +65,10 @@
RPCIPSpec_def: "RPCIPSpec send rcv rst p == TEMP
Init RPCInit rcv rst p
- & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+ & \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
& WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
- RPCISpec_def: "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
+ RPCISpec_def: "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
lemmas RPC_action_defs =
@@ -81,10 +81,10 @@
unanswered call for that process.
*)
-lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"
+lemma RPCidle: "|- \<not>$(Calling send p) --> \<not>RPCNext send rcv rst p"
by (auto simp: Return_def RPC_action_defs)
-lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"
+lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> \<not>RPCNext send rcv rst p"
by (auto simp: RPC_action_defs)
(* RPC failure actions are visible. *)
@@ -97,14 +97,14 @@
by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
(* Enabledness of some actions *)
-lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
- |- ~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) ==>
+ |- \<not>Calling rcv p & Calling send p --> 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: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>
- |- ~Calling rcv p & Calling send p & rst!p = #rpcB
+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)"
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
@{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
--- a/src/HOL/TLA/Memory/RPCParameters.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Fri Jun 26 11:44:22 2015 +0200
@@ -30,10 +30,10 @@
axiomatization where
(* RPCFailure is different from MemVals and exceptions *)
- RFNoMemVal: "RPCFailure ~: MemVal" and
- NotAResultNotRF: "NotAResult ~= RPCFailure" and
- OKNotRF: "OK ~= RPCFailure" and
- BANotRF: "BadArg ~= RPCFailure"
+ RFNoMemVal: "RPCFailure \<notin> MemVal" and
+ NotAResultNotRF: "NotAResult \<noteq> RPCFailure" and
+ OKNotRF: "OK \<noteq> RPCFailure" and
+ BANotRF: "BadArg \<noteq> RPCFailure"
defs
IsLegalRcvArg_def: "IsLegalRcvArg ra ==
--- a/src/HOL/TLA/Stfun.thy Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Stfun.thy Fri Jun 26 11:44:22 2015 +0200
@@ -50,13 +50,13 @@
basevars_def: "stvars vs == range vs = UNIV"
-lemma basevars: "!!vs. basevars vs ==> EX u. vs u = c"
+lemma basevars: "\<And>vs. basevars vs ==> \<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: "!!x y. basevars (x,y) ==> basevars x"
+lemma base_pair1: "\<And>x y. basevars (x,y) ==> 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: "!!x y. basevars (x,y) ==> basevars y"
+lemma base_pair2: "\<And>x y. basevars (x,y) ==> 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: "!!x y. basevars (x,y) ==> basevars x & basevars y"
+lemma base_pair: "\<And>x y. basevars (x,y) ==> 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; !!x. v x = c ==> Q |] ==> Q"
+lemma baseE: "[| basevars v; \<And>x. v x = c ==> Q |] ==> 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 "!!v. basevars (v::bool stfun, v) ==> False"
+lemma "\<And>v. basevars (v::bool stfun, v) ==> 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:07:04 2015 +0200
+++ b/src/HOL/TLA/TLA.thy Fri Jun 26 11:44:22 2015 +0200
@@ -60,49 +60,45 @@
"_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
"_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
-syntax (HTML output)
- "_EEx" :: "[idts, lift] => lift" ("(3\<exists>\<exists> _./ _)" [0,10] 10)
- "_AAll" :: "[idts, lift] => lift" ("(3\<forall>\<forall> _./ _)" [0,10] 10)
-
axiomatization where
(* Definitions of derived operators *)
- dmd_def: "\<And>F. TEMP <>F == TEMP ~[]~F"
+ dmd_def: "\<And>F. TEMP \<diamond>F == TEMP \<not>\<box>\<not>F"
axiomatization where
- boxInit: "\<And>F. TEMP []F == TEMP []Init F" and
- leadsto_def: "\<And>F G. TEMP F ~> G == TEMP [](Init F --> <>G)" and
- stable_def: "\<And>P. TEMP stable P == TEMP []($P --> P$)" and
- WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(<A>_v) --> []<><A>_v" and
- SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(<A>_v) --> []<><A>_v" and
- aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)"
+ 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
+ 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. |- [](F --> G) --> ([]F --> []G)" and (* polymorphic *)
- reflT: "\<And>F. |- []F --> F" and (* F::temporal *)
- transT: "\<And>F. |- []F --> [][]F" and (* polymorphic *)
- linT: "\<And>F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and
- discT: "\<And>F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and
- primeI: "\<And>P. |- []P --> Init P`" and
- primeE: "\<And>P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and
- indT: "\<And>P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and
- allT: "\<And>F. |- (ALL x. [](F x)) = ([](ALL x. F x))"
+ 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))"
axiomatization where
- necT: "\<And>F. |- F ==> |- []F" (* polymorphic *)
+ necT: "\<And>F. |- F ==> |- \<box>F" (* polymorphic *)
axiomatization where
(* Flexible quantification: refinement mappings, history variables *)
- eexI: "|- F x --> (EEX x. F x)" and
- eexE: "[| sigma |= (EEX x. F x); basevars vs;
- (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool)
+ 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: "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
+ history: "|- \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x --> h` = hb x)"
(* Specialize intensional introduction/elimination rules for temporal formulas *)
-lemma tempI [intro!]: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
+lemma tempI [intro!]: "(\<And>sigma. sigma |= (F::temporal)) ==> |- F"
apply (rule intI)
apply (erule meta_spec)
done
@@ -145,20 +141,20 @@
(* ------------------------------------------------------------------------- *)
-(*** "Simple temporal logic": only [] and <> ***)
+(*** "Simple temporal logic": only \<box> and \<diamond> ***)
(* ------------------------------------------------------------------------- *)
section "Simple temporal logic"
-(* []~F == []~Init F *)
-lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F
+(* \<box>\<not>F == \<box>\<not>Init F *)
+lemmas boxNotInit = boxInit [of "LIFT \<not>F", unfolded Init_simps] for F
-lemma dmdInit: "TEMP <>F == TEMP <> Init F"
+lemma dmdInit: "TEMP \<diamond>F == TEMP \<diamond> Init F"
apply (unfold dmd_def)
- apply (unfold boxInit [of "LIFT ~F"])
+ apply (unfold boxInit [of "LIFT \<not>F"])
apply (simp (no_asm) add: Init_simps)
done
-lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F
+lemmas dmdNotInit = dmdInit [of "LIFT \<not>F", unfolded Init_simps] for F
(* boxInit and dmdInit cannot be used as rewrites, because they loop.
Non-looping instances for state predicates and actions are occasionally useful.
@@ -180,21 +176,21 @@
lemmas STL2 = reflT
(* The "polymorphic" (generic) variant *)
-lemma STL2_gen: "|- []F --> Init F"
+lemma STL2_gen: "|- \<box>F --> Init F"
apply (unfold boxInit [of F])
apply (rule STL2)
done
-(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *)
+(* see also STL2_pr below: "|- \<box>P --> Init P & Init (P`)" *)
-(* Dual versions for <> *)
-lemma InitDmd: "|- F --> <> F"
+(* Dual versions for \<diamond> *)
+lemma InitDmd: "|- F --> \<diamond> F"
apply (unfold dmd_def)
apply (auto dest!: STL2 [temp_use])
done
-lemma InitDmd_gen: "|- Init F --> <>F"
+lemma InitDmd_gen: "|- Init F --> \<diamond>F"
apply clarsimp
apply (drule InitDmd [temp_use])
apply (simp add: dmdInitD)
@@ -202,17 +198,17 @@
(* ------------------------ STL3 ------------------------------------------- *)
-lemma STL3: "|- ([][]F) = ([]F)"
+lemma STL3: "|- (\<box>\<box>F) = (\<box>F)"
by (auto elim: transT [temp_use] STL2 [temp_use])
(* corresponding elimination rule introduces double boxes:
- [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
+ [| (sigma |= \<box>F); (sigma |= \<box>\<box>F) ==> PROP W |] ==> PROP W
*)
lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
-(* dual versions for <> *)
-lemma DmdDmd: "|- (<><>F) = (<>F)"
+(* dual versions for \<diamond> *)
+lemma DmdDmd: "|- (\<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]
@@ -222,7 +218,7 @@
(* ------------------------ STL4 ------------------------------------------- *)
lemma STL4:
assumes "|- F --> G"
- shows "|- []F --> []G"
+ shows "|- \<box>F --> \<box>G"
apply clarsimp
apply (rule normalT [temp_use])
apply (rule assms [THEN necT, temp_use])
@@ -230,38 +226,38 @@
done
(* Unlifted version as an elimination rule *)
-lemma STL4E: "[| sigma |= []F; |- F --> G |] ==> sigma |= []G"
+lemma STL4E: "[| sigma |= \<box>F; |- F --> G |] ==> sigma |= \<box>G"
by (erule (1) STL4 [temp_use])
-lemma STL4_gen: "|- Init F --> Init G ==> |- []F --> []G"
+lemma STL4_gen: "|- Init F --> Init G ==> |- \<box>F --> \<box>G"
apply (drule STL4)
apply (simp add: boxInitD)
done
-lemma STL4E_gen: "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G"
+lemma STL4E_gen: "[| sigma |= \<box>F; |- Init F --> Init G |] ==> sigma |= \<box>G"
by (erule (1) STL4_gen [temp_use])
(* see also STL4Edup below, which allows an auxiliary boxed formula:
- []A /\ F => G
+ \<box>A /\ F => G
-----------------
- []A /\ []F => []G
+ \<box>A /\ \<box>F => \<box>G
*)
-(* The dual versions for <> *)
+(* The dual versions for \<diamond> *)
lemma DmdImpl:
assumes prem: "|- F --> G"
- shows "|- <>F --> <>G"
+ shows "|- \<diamond>F --> \<diamond>G"
apply (unfold dmd_def)
apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
done
-lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G"
+lemma DmdImplE: "[| sigma |= \<diamond>F; |- F --> G |] ==> sigma |= \<diamond>G"
by (erule (1) DmdImpl [temp_use])
(* ------------------------ STL5 ------------------------------------------- *)
-lemma STL5: "|- ([]F & []G) = ([](F & G))"
+lemma STL5: "|- (\<box>F & \<box>G) = (\<box>(F & G))"
apply auto
- apply (subgoal_tac "sigma |= [] (G --> (F & G))")
+ apply (subgoal_tac "sigma |= \<box> (G --> (F & G))")
apply (erule normalT [temp_use])
apply (fastforce elim!: STL4E [temp_use])+
done
@@ -275,9 +271,9 @@
Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop!
*)
lemma box_conjE:
- assumes "sigma |= []F"
- and "sigma |= []G"
- and "sigma |= [](F&G) ==> PROP R"
+ assumes "sigma |= \<box>F"
+ and "sigma |= \<box>G"
+ and "sigma |= \<box>(F&G) ==> PROP R"
shows "PROP R"
by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
@@ -292,7 +288,7 @@
a bit kludgy in order to simulate "double elim-resolution".
*)
-lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" .
+lemma box_thin: "[| sigma |= \<box>F; PROP W |] ==> PROP W" .
ML {*
fun merge_box_tac i =
@@ -317,29 +313,29 @@
method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
(* rewrite rule to push universal quantification through box:
- (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
+ (sigma |= \<box>(\<forall>x. F x)) = (\<forall>x. (sigma |= \<box>F x))
*)
lemmas all_box = allT [temp_unlift, symmetric]
-lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
+lemma DmdOr: "|- (\<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: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
+lemma exT: "|- (\<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: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
+lemma STL4Edup: "\<And>sigma. [| sigma |= \<box>A; sigma |= \<box>F; |- F & \<box>A --> G |] ==> sigma |= \<box>G"
apply (erule dup_boxE)
apply merge_box
apply (erule STL4E)
apply assumption
done
-lemma DmdImpl2:
- "!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G"
+lemma DmdImpl2:
+ "\<And>sigma. [| sigma |= \<diamond>F; sigma |= \<box>(F --> G) |] ==> sigma |= \<diamond>G"
apply (unfold dmd_def)
apply auto
apply (erule notE)
@@ -348,10 +344,10 @@
done
lemma InfImpl:
- assumes 1: "sigma |= []<>F"
- and 2: "sigma |= []G"
+ assumes 1: "sigma |= \<box>\<diamond>F"
+ and 2: "sigma |= \<box>G"
and 3: "|- F & G --> H"
- shows "sigma |= []<>H"
+ shows "sigma |= \<box>\<diamond>H"
apply (insert 1 2)
apply (erule_tac F = G in dup_boxE)
apply merge_box
@@ -360,7 +356,7 @@
(* ------------------------ STL6 ------------------------------------------- *)
(* Used in the proof of STL6, but useful in itself. *)
-lemma BoxDmd: "|- []F & <>G --> <>([]F & G)"
+lemma BoxDmd: "|- \<box>F & \<diamond>G --> \<diamond>(\<box>F & G)"
apply (unfold dmd_def)
apply clarsimp
apply (erule dup_boxE)
@@ -370,14 +366,14 @@
done
(* weaker than BoxDmd, but more polymorphic (and often just right) *)
-lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)"
+lemma BoxDmd_simple: "|- \<box>F & \<diamond>G --> \<diamond>(F & G)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
apply (fastforce elim!: notE STL4E [temp_use])
done
-lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
+lemma BoxDmd2_simple: "|- \<box>F & \<diamond>G --> \<diamond>(G & F)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
@@ -385,15 +381,15 @@
done
lemma DmdImpldup:
- assumes 1: "sigma |= []A"
- and 2: "sigma |= <>F"
- and 3: "|- []A & F --> G"
- shows "sigma |= <>G"
+ assumes 1: "sigma |= \<box>A"
+ and 2: "sigma |= \<diamond>F"
+ and 3: "|- \<box>A & F --> G"
+ shows "sigma |= \<diamond>G"
apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
apply (rule 3)
done
-lemma STL6: "|- <>[]F & <>[]G --> <>[](F & G)"
+lemma STL6: "|- \<diamond>\<box>F & \<diamond>\<box>G --> \<diamond>\<box>(F & G)"
apply (auto simp: STL5 [temp_rewrite, symmetric])
apply (drule linT [temp_use])
apply assumption
@@ -414,13 +410,13 @@
(* ------------------------ True / False ----------------------------------------- *)
section "Simplification of constants"
-lemma BoxConst: "|- ([]#P) = #P"
+lemma BoxConst: "|- (\<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: "|- (<>#P) = #P"
+lemma DmdConst: "|- (\<diamond>#P) = #P"
apply (unfold dmd_def)
apply (cases P)
apply (simp_all add: BoxConst [try_rewrite])
@@ -432,23 +428,23 @@
(* ------------------------ Further rewrites ----------------------------------------- *)
section "Further rewrites"
-lemma NotBox: "|- (~[]F) = (<>~F)"
+lemma NotBox: "|- (\<not>\<box>F) = (\<diamond>\<not>F)"
by (simp add: dmd_def)
-lemma NotDmd: "|- (~<>F) = ([]~F)"
+lemma NotDmd: "|- (\<not>\<diamond>F) = (\<box>\<not>F)"
by (simp add: dmd_def)
(* These are not declared by default, because they could be harmful,
- e.g. []F & ~[]F becomes []F & <>~F !! *)
+ e.g. \<box>F & \<not>\<box>F becomes \<box>F & \<diamond>\<not>F !! *)
lemmas more_temp_simps1 =
STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite]
NotBox [temp_unlift, THEN eq_reflection]
NotDmd [temp_unlift, THEN eq_reflection]
-lemma BoxDmdBox: "|- ([]<>[]F) = (<>[]F)"
+lemma BoxDmdBox: "|- (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
apply (auto dest!: STL2 [temp_use])
apply (rule ccontr)
- apply (subgoal_tac "sigma |= <>[][]F & <>[]~[]F")
+ apply (subgoal_tac "sigma |= \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
apply (erule thin_rl)
apply auto
apply (drule STL6 [temp_use])
@@ -457,7 +453,7 @@
apply (simp_all add: more_temp_simps1)
done
-lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)"
+lemma DmdBoxDmd: "|- (\<diamond>\<box>\<diamond>F) = (\<box>\<diamond>F)"
apply (unfold dmd_def)
apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
done
@@ -467,11 +463,11 @@
(* ------------------------ Miscellaneous ----------------------------------- *)
-lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)"
+lemma BoxOr: "\<And>sigma. [| sigma |= \<box>F | \<box>G |] ==> sigma |= \<box>(F | G)"
by (fastforce elim!: STL4E [temp_use])
(* "persistently implies infinitely often" *)
-lemma DBImplBD: "|- <>[]F --> []<>F"
+lemma DBImplBD: "|- \<diamond>\<box>F --> \<box>\<diamond>F"
apply clarsimp
apply (rule ccontr)
apply (simp add: more_temp_simps2)
@@ -480,13 +476,13 @@
apply simp
done
-lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)"
+lemma BoxDmdDmdBox: "|- \<box>\<diamond>F & \<diamond>\<box>G --> \<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 |= <>[]~F")
+ apply (subgoal_tac "sigma |= \<diamond>\<box>\<not>F")
apply (force simp: dmd_def)
apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
done
@@ -498,11 +494,11 @@
section "priming"
(* ------------------------ TLA2 ------------------------------------------- *)
-lemma STL2_pr: "|- []P --> Init P & Init P`"
+lemma STL2_pr: "|- \<box>P --> Init P & Init P`"
by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
(* Auxiliary lemma allows priming of boxed actions *)
-lemma BoxPrime: "|- []P --> []($P & P$)"
+lemma BoxPrime: "|- \<box>P --> \<box>($P & P$)"
apply clarsimp
apply (erule dup_boxE)
apply (unfold boxInit_act)
@@ -512,17 +508,17 @@
lemma TLA2:
assumes "|- $P & P$ --> A"
- shows "|- []P --> []A"
+ shows "|- \<box>P --> \<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 |= []P; |- $P & P$ --> A |] ==> sigma |= []A"
+lemma TLA2E: "[| sigma |= \<box>P; |- $P & P$ --> A |] ==> sigma |= \<box>A"
by (erule (1) TLA2 [temp_use])
-lemma DmdPrime: "|- (<>P`) --> (<>P)"
+lemma DmdPrime: "|- (\<diamond>P`) --> (\<diamond>P)"
apply (unfold dmd_def)
apply (fastforce elim!: TLA2E [temp_use])
done
@@ -533,13 +529,13 @@
section "stable, invariant"
lemma ind_rule:
- "[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |]
- ==> sigma |= []F"
+ "[| sigma |= \<box>H; sigma |= Init P; |- H --> (Init P & \<not>\<box>F --> Init(P`) & F) |]
+ ==> sigma |= \<box>F"
apply (rule indT [temp_use])
apply (erule (2) STL4E)
done
-lemma box_stp_act: "|- ([]$P) = ([]P)"
+lemma box_stp_act: "|- (\<box>$P) = (\<box>P)"
by (simp add: boxInit_act Init_simps)
lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
@@ -547,32 +543,32 @@
lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
-lemma INV1:
- "|- (Init P) --> (stable P) --> []P"
+lemma INV1:
+ "|- (Init P) --> (stable P) --> \<box>P"
apply (unfold stable_def boxInit_stp boxInit_act)
apply clarsimp
apply (erule ind_rule)
apply (auto simp: Init_simps elim: ind_rule)
done
-lemma StableT:
- "!!P. |- $P & A --> P` ==> |- []A --> stable P"
+lemma StableT:
+ "\<And>P. |- $P & A --> P` ==> |- \<box>A --> stable P"
apply (unfold stable_def)
apply (fastforce elim!: STL4E [temp_use])
done
-lemma Stable: "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P"
+lemma Stable: "[| sigma |= \<box>A; |- $P & A --> P` |] ==> sigma |= stable P"
by (erule (1) StableT [temp_use])
(* Generalization of INV1 *)
-lemma StableBox: "|- (stable P) --> [](Init P --> []P)"
+lemma StableBox: "|- (stable P) --> \<box>(Init P --> \<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) & <>P --> <>[]P"
+lemma DmdStable: "|- (stable P) & \<diamond>P --> \<diamond>\<box>P"
apply clarsimp
apply (rule DmdImpl2)
prefer 2
@@ -583,7 +579,7 @@
(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
ML {*
-(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
+(* inv_tac reduces goals of the form ... ==> sigma |= \<box>P *)
fun inv_tac ctxt =
SELECT_GOAL
(EVERY
@@ -593,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 --> []Inv.
+ in simple cases it may be able to handle goals like |- MyProg --> \<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.
@@ -613,7 +609,7 @@
Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
*}
-lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
+lemma unless: "|- \<box>($P --> P` | Q`) --> (stable P) | \<diamond>Q"
apply (unfold dmd_def)
apply (clarsimp dest!: BoxPrime [temp_use])
apply merge_box
@@ -625,29 +621,29 @@
(* --------------------- Recursive expansions --------------------------------------- *)
section "recursive expansions"
-(* Recursive expansions of [] and <> for state predicates *)
-lemma BoxRec: "|- ([]P) = (Init P & []P`)"
+(* Recursive expansions of \<box> and \<diamond> for state predicates *)
+lemma BoxRec: "|- (\<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: "|- (<>P) = (Init P | <>P`)"
+lemma DmdRec: "|- (\<diamond>P) = (Init P | \<diamond>P`)"
apply (unfold dmd_def BoxRec [temp_rewrite])
apply (auto simp: Init_simps)
done
-lemma DmdRec2: "!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P"
+lemma DmdRec2: "\<And>sigma. [| sigma |= \<diamond>P; sigma |= \<box>\<not>P` |] ==> sigma |= Init P"
apply (force simp: DmdRec [temp_rewrite] dmd_def)
done
-lemma InfinitePrime: "|- ([]<>P) = ([]<>P`)"
+lemma InfinitePrime: "|- (\<box>\<diamond>P) = (\<box>\<diamond>P`)"
apply auto
apply (rule classical)
apply (rule DBImplBD [temp_use])
- apply (subgoal_tac "sigma |= <>[]P")
+ apply (subgoal_tac "sigma |= \<diamond>\<box>P")
apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
- apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
+ apply (subgoal_tac "sigma |= \<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)
@@ -655,7 +651,7 @@
done
lemma InfiniteEnsures:
- "[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P"
+ "[| sigma |= \<box>N; sigma |= \<box>\<diamond>A; |- A & N --> P` |] ==> sigma |= \<box>\<diamond>P"
apply (unfold InfinitePrime [temp_rewrite])
apply (rule InfImpl)
apply assumption+
@@ -665,27 +661,27 @@
section "fairness"
(* alternative definitions of fairness *)
-lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)"
+lemma WF_alt: "|- 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 = (<>[]~Enabled(<A>_v) | []<><A>_v)"
+lemma SF_alt: "|- 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 --> []WF(A)_v"
+lemma BoxWFI: "|- WF(A)_v --> \<box>WF(A)_v"
by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
-lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
+lemma WF_Box: "|- (\<box>WF(A)_v) = WF(A)_v"
by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
-lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
+lemma BoxSFI: "|- SF(A)_v --> \<box>SF(A)_v"
by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
-lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
+lemma SF_Box: "|- (\<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]
@@ -704,30 +700,30 @@
(* ------------------------------ leads-to ------------------------------ *)
-section "~>"
+section "\<leadsto>"
-lemma leadsto_init: "|- (Init F) & (F ~> G) --> <>G"
+lemma leadsto_init: "|- (Init F) & (F \<leadsto> G) --> \<diamond>G"
apply (unfold leadsto_def)
apply (auto dest!: STL2 [temp_use])
done
-(* |- F & (F ~> G) --> <>G *)
+(* |- F & (F \<leadsto> G) --> \<diamond>G *)
lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
-lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))"
+lemma streett_leadsto: "|- (\<box>\<diamond>Init F --> \<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 |= []<><>G")
+ apply (subgoal_tac "sigma |= \<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: "|- []<>F & (F ~> G) --> []<>G"
+lemma leadsto_infinite: "|- \<box>\<diamond>F & (F \<leadsto> G) --> \<box>\<diamond>G"
apply clarsimp
apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
apply (simp add: dmdInitD)
@@ -736,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) ~> <A>_v) --> SF(A)_v"
+lemma leadsto_SF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> SF(A)_v"
apply (unfold SF_def)
apply (clarsimp elim!: leadsto_infinite [temp_use])
done
-lemma leadsto_WF: "|- (Enabled(<A>_v) ~> <A>_v) --> WF(A)_v"
+lemma leadsto_WF: "|- (Enabled(<A>_v) \<leadsto> <A>_v) --> WF(A)_v"
by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use])
(* introduce an invariant into the proof of a leadsto assertion.
- []I --> ((P ~> Q) = (P /\ I ~> Q))
+ \<box>I --> ((P \<leadsto> Q) = (P /\ I \<leadsto> Q))
*)
-lemma INV_leadsto: "|- []I & (P & I ~> Q) --> (P ~> Q)"
+lemma INV_leadsto: "|- \<box>I & (P & I \<leadsto> Q) --> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4Edup)
@@ -755,24 +751,24 @@
apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
done
-lemma leadsto_classical: "|- (Init F & []~G ~> G) --> (F ~> G)"
+lemma leadsto_classical: "|- (Init F & \<box>\<not>G \<leadsto> G) --> (F \<leadsto> G)"
apply (unfold leadsto_def dmd_def)
apply (force simp: Init_simps elim!: STL4E [temp_use])
done
-lemma leadsto_false: "|- (F ~> #False) = ([]~F)"
+lemma leadsto_false: "|- (F \<leadsto> #False) = (\<box>~F)"
apply (unfold leadsto_def)
apply (simp add: boxNotInitD)
done
-lemma leadsto_exists: "|- ((EX x. F x) ~> G) = (ALL x. (F x ~> G))"
+lemma leadsto_exists: "|- ((\<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: "|- [](Init F --> Init G) --> (F ~> G)"
+lemma ImplLeadsto_gen: "|- \<box>(Init F --> Init G) --> (F \<leadsto> G)"
apply (unfold leadsto_def)
apply (auto intro!: InitDmd_gen [temp_use]
elim!: STL4E_gen [temp_use] simp: Init_simps)
@@ -781,19 +777,19 @@
lemmas ImplLeadsto =
ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
-lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G"
+lemma ImplLeadsto_simple: "\<And>F G. |- F --> G ==> |- F \<leadsto> G"
by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
lemma EnsuresLeadsto:
assumes "|- A & $P --> Q`"
- shows "|- []A --> (P ~> Q)"
+ shows "|- \<box>A --> (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: "|- []($P --> Q`) --> (P ~> Q)"
+lemma EnsuresLeadsto2: "|- \<box>($P --> Q`) --> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4E_gen)
@@ -803,13 +799,13 @@
lemma ensures:
assumes 1: "|- $P & N --> P` | Q`"
and 2: "|- ($P & N) & A --> Q`"
- shows "|- []N & []([]P --> <>A) --> (P ~> Q)"
+ shows "|- \<box>N & \<box>(\<box>P --> \<diamond>A) --> (P \<leadsto> Q)"
apply (unfold leadsto_def)
apply clarsimp
apply (erule STL4Edup)
apply assumption
apply clarsimp
- apply (subgoal_tac "sigmaa |= [] ($P --> P` | Q`) ")
+ apply (subgoal_tac "sigmaa |= \<box>($P --> P` | Q`) ")
apply (drule unless [temp_use])
apply (clarsimp dest!: INV1 [temp_use])
apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
@@ -819,16 +815,16 @@
done
lemma ensures_simple:
- "[| |- $P & N --> P` | Q`;
- |- ($P & N) & A --> Q`
- |] ==> |- []N & []<>A --> (P ~> Q)"
+ "[| |- $P & N --> P` | Q`;
+ |- ($P & N) & A --> Q`
+ |] ==> |- \<box>N & \<box>\<diamond>A --> (P \<leadsto> Q)"
apply clarsimp
apply (erule (2) ensures [temp_use])
apply (force elim!: STL4E [temp_use])
done
lemma EnsuresInfinite:
- "[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q"
+ "[| sigma |= \<box>\<diamond>P; sigma |= \<box>A; |- A & $P --> Q` |] ==> sigma |= \<box>\<diamond>Q"
apply (erule leadsto_infinite [temp_use])
apply (erule EnsuresLeadsto [temp_use])
apply assumption
@@ -838,64 +834,64 @@
(*** Gronning's lattice rules (taken from TLP) ***)
section "Lattice rules"
-lemma LatticeReflexivity: "|- F ~> F"
+lemma LatticeReflexivity: "|- F \<leadsto> F"
apply (unfold leadsto_def)
apply (rule necT InitDmd_gen)+
done
-lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)"
+lemma LatticeTransitivity: "|- (G \<leadsto> H) & (F \<leadsto> G) --> (F \<leadsto> H)"
apply (unfold leadsto_def)
apply clarsimp
- apply (erule dup_boxE) (* [][] (Init G --> H) *)
+ apply (erule dup_boxE) (* \<box>\<box>(Init G --> H) *)
apply merge_box
apply (clarsimp elim!: STL4E [temp_use])
apply (rule dup_dmdD)
- apply (subgoal_tac "sigmaa |= <>Init G")
+ apply (subgoal_tac "sigmaa |= \<diamond>Init G")
apply (erule DmdImpl2)
apply assumption
apply (simp add: dmdInitD)
done
-lemma LatticeDisjunctionElim1: "|- (F | G ~> H) --> (F ~> H)"
+lemma LatticeDisjunctionElim1: "|- (F | G \<leadsto> H) --> (F \<leadsto> H)"
apply (unfold leadsto_def)
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunctionElim2: "|- (F | G ~> H) --> (G ~> H)"
+lemma LatticeDisjunctionElim2: "|- (F | G \<leadsto> H) --> (G \<leadsto> H)"
apply (unfold leadsto_def)
apply (auto simp: Init_simps elim!: STL4E [temp_use])
done
-lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)"
+lemma LatticeDisjunctionIntro: "|- (F \<leadsto> H) & (G \<leadsto> H) --> (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 ~> H) = ((F ~> H) & (G ~> H))"
+lemma LatticeDisjunction: "|- (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 ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)"
+lemma LatticeDiamond: "|- (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) --> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma |= (B | C) ~> D")
+ apply (subgoal_tac "sigma |= (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 ~> D | B) & (B ~> D) --> (A ~> D)"
+lemma LatticeTriangle: "|- (A \<leadsto> D | B) & (B \<leadsto> D) --> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma |= (D | B) ~> D")
+ apply (subgoal_tac "sigma |= (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 ~> B | D) & (B ~> D) --> (A ~> D)"
+lemma LatticeTriangle2: "|- (A \<leadsto> B | D) & (B \<leadsto> D) --> (A \<leadsto> D)"
apply clarsimp
- apply (subgoal_tac "sigma |= B | D ~> D")
+ apply (subgoal_tac "sigma |= 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])
@@ -905,10 +901,10 @@
section "Fairness rules"
lemma WF1:
- "[| |- $P & N --> P` | Q`;
- |- ($P & N) & <A>_v --> Q`;
- |- $P & N --> $(Enabled(<A>_v)) |]
- ==> |- []N & WF(A)_v --> (P ~> Q)"
+ "[| |- $P & N --> P` | Q`;
+ |- ($P & N) & <A>_v --> Q`;
+ |- $P & N --> $(Enabled(<A>_v)) |]
+ ==> |- \<box>N & WF(A)_v --> (P \<leadsto> Q)"
apply (clarsimp dest!: BoxWFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule (1) STL4Edup)
@@ -923,8 +919,8 @@
lemma WF_leadsto:
assumes 1: "|- N & $P --> $Enabled (<A>_v)"
and 2: "|- N & <A>_v --> B"
- and 3: "|- [](N & [~A]_v) --> stable P"
- shows "|- []N & WF(A)_v --> (P ~> B)"
+ and 3: "|- \<box>(N & [~A]_v) --> stable P"
+ shows "|- \<box>N & WF(A)_v --> (P \<leadsto> B)"
apply (unfold leadsto_def)
apply (clarsimp dest!: BoxWFI [temp_use])
apply (erule (1) STL4Edup)
@@ -943,10 +939,10 @@
done
lemma SF1:
- "[| |- $P & N --> P` | Q`;
- |- ($P & N) & <A>_v --> Q`;
- |- []P & []N & []F --> <>Enabled(<A>_v) |]
- ==> |- []N & SF(A)_v & []F --> (P ~> Q)"
+ "[| |- $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)"
apply (clarsimp dest!: BoxSFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule_tac F = F in dup_boxE)
@@ -964,8 +960,8 @@
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: "|- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(<M>_g) --> <>[]P"
- shows "|- []N & WF(A)_f & []F --> WF(M)_g"
+ 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"
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)
@@ -974,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 |= <> (($P & P` & N) & <A>_f)")
+ apply (subgoal_tac "sigmaa |= \<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])
@@ -983,8 +979,8 @@
apply assumption+
apply (drule STL6 [temp_use])
apply assumption
- apply (erule_tac V = "sigmaa |= <>[]P" in thin_rl)
- apply (erule_tac V = "sigmaa |= []F" in thin_rl)
+ apply (erule_tac V = "sigmaa |= \<diamond>\<box>P" in thin_rl)
+ apply (erule_tac V = "sigmaa |= \<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
@@ -1002,26 +998,26 @@
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: "|- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(<M>_g) --> <>[]P"
- shows "|- []N & SF(A)_f & []F --> SF(M)_g"
+ 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"
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 <>Enabled (<M>_g) " in dup_boxE)
+ apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE)
apply merge_temp_box
apply (erule STL4Edup)
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
apply (rule classical)
- apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & <A>_f)")
+ apply (subgoal_tac "sigmaa |= \<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 |= []F" in thin_rl)
+ apply (erule_tac V = "sigmaa |= \<box>F" in thin_rl)
apply (drule BoxSFI [temp_use])
- apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
+ apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE)
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
apply merge_temp_box
apply (erule DmdImpldup)
@@ -1041,8 +1037,8 @@
lemma wf_leadsto:
assumes 1: "wf r"
- and 2: "!!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y)) "
- shows "sigma |= F x ~> G"
+ and 2: "\<And>x. sigma |= F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y)) "
+ shows "sigma |= F x \<leadsto> G"
apply (rule 1 [THEN wf_induct])
apply (rule LatticeTriangle [temp_use])
apply (rule 2)
@@ -1053,10 +1049,10 @@
done
(* If r is well-founded, state function v cannot decrease forever *)
-lemma wf_not_box_decrease: "!!r. wf r ==> |- [][ (v`, $v) : #r ]_v --> <>[][#False]_v"
+lemma wf_not_box_decrease: "\<And>r. wf r ==> |- \<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v"
apply clarsimp
apply (rule ccontr)
- apply (subgoal_tac "sigma |= (EX x. v=#x) ~> #False")
+ apply (subgoal_tac "sigma |= (\<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)
@@ -1065,7 +1061,7 @@
apply (auto simp: square_def angle_def)
done
-(* "wf r ==> |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *)
+(* "wf r ==> |- \<diamond>\<box>[ (v`, $v) : #r ]_v --> \<diamond>\<box>[#False]_v" *)
lemmas wf_not_dmd_box_decrease =
wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
@@ -1074,14 +1070,14 @@
*)
lemma wf_box_dmd_decrease:
assumes 1: "wf r"
- shows "|- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v"
+ shows "|- \<box>\<diamond>((v`, $v) : #r) --> \<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 |= []<> ((#False) ::action)")
+ apply (subgoal_tac "sigma |= \<box>\<diamond> ((#False) ::action)")
apply force
apply (erule STL4E)
apply (rule DmdImpl)
@@ -1091,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: "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)"
+lemma nat_box_dmd_decrease: "\<And>n::nat stfun. |- \<box>\<diamond>(n` < $n) --> \<box>\<diamond>($n < n`)"
apply clarsimp
- apply (subgoal_tac "sigma |= []<><~ ((n`,$n) : #less_than) >_n")
+ apply (subgoal_tac "sigma |= \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
apply (erule thin_rl)
apply (erule STL4E)
apply (rule DmdImpl)
@@ -1110,11 +1106,11 @@
lemma aallI:
assumes 1: "basevars vs"
- and 2: "(!!x. basevars (x,vs) ==> sigma |= F x)"
- shows "sigma |= (AALL x. F x)"
+ and 2: "(\<And>x. basevars (x,vs) ==> sigma |= F x)"
+ shows "sigma |= (\<forall>\<forall>x. F x)"
by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use])
-lemma aallE: "|- (AALL x. F x) --> F x"
+lemma aallE: "|- (\<forall>\<forall>x. F x) --> F x"
apply (unfold aall_def)
apply clarsimp
apply (erule contrapos_np)
@@ -1123,18 +1119,18 @@
(* monotonicity of quantification *)
lemma eex_mono:
- assumes 1: "sigma |= EEX x. F x"
- and 2: "!!x. sigma |= F x --> G x"
- shows "sigma |= EEX x. G x"
+ assumes 1: "sigma |= \<exists>\<exists>x. F x"
+ and 2: "\<And>x. sigma |= F x --> G x"
+ shows "sigma |= \<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 |= AALL x. F(x)"
- and 2: "!!x. sigma |= F(x) --> G(x)"
- shows "sigma |= AALL x. G(x)"
+ assumes 1: "sigma |= \<forall>\<forall>x. F(x)"
+ and 2: "\<And>x. sigma |= F(x) --> G(x)"
+ shows "sigma |= \<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]])
@@ -1143,11 +1139,11 @@
(* Derived history introduction rule *)
lemma historyI:
assumes 1: "sigma |= Init I"
- and 2: "sigma |= []N"
+ and 2: "sigma |= \<box>N"
and 3: "basevars vs"
- and 4: "!!h. basevars(h,vs) ==> |- I & h = ha --> HI h"
- and 5: "!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)"
- shows "sigma |= EEX h. Init (HI h) & [](HN h)"
+ 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)"
apply (rule history [temp_use, THEN eexE])
apply (rule 3)
apply (rule eexI [temp_use])
@@ -1165,7 +1161,7 @@
example of a history variable: existence of a clock
*)
-lemma "|- EEX h. Init(h = #True) & [](h` = (~$h))"
+lemma "|- \<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])+