--- 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