src/HOL/TLA/Memory/RPC.thy

 imports RPCParameters ProcedureInterface Memory
 begin
 
 type_synonym rpcSndChType = "(rpcOp,Vals) channel"
 type_synonym rpcRcvChType = "memChType"
-type_synonym rpcStType = "(PrIds => rpcState) stfun"
+type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
 
 consts
   (* state predicates *)
-  RPCInit      :: "rpcRcvChType => rpcStType => PrIds => stpred"
+  RPCInit      :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
 
   (* actions *)
-  RPCFwd     :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
-  RPCReject  :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
-  RPCFail    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
-  RPCReply   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
-  RPCNext    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
+  RPCFwd     :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  RPCReject  :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  RPCFail    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  RPCReply   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
+  RPCNext    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
 
   (* temporal *)
-  RPCIPSpec   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
-  RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
+  RPCIPSpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
+  RPCISpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
 
 defs
   RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
 
   RPCFwd_def:        "RPCFwd send rcv rst p == ACT

 
 (* The RPC component engages in an action for process p only if there is an outstanding,
    unanswered call for that process.
 *)
 
-lemma RPCidle: "|- \<not>$(Calling send p) --> \<not>RPCNext send rcv rst p"
+lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
   by (auto simp: Return_def RPC_action_defs)
 
-lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> \<not>RPCNext send rcv rst p"
+lemma RPCbusy: "\<turnstile> $(Calling rcv p) & $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
   by (auto simp: RPC_action_defs)
 
 (* RPC failure actions are visible. *)
-lemma RPCFail_vis: "|- RPCFail send rcv rst p -->  
+lemma RPCFail_vis: "\<turnstile> RPCFail send rcv rst p \<longrightarrow>  
     <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
   by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)
 
-lemma RPCFail_Next_enabled: "|- Enabled (RPCFail send rcv rst p) -->  
+lemma RPCFail_Next_enabled: "\<turnstile> Enabled (RPCFail send rcv rst p) \<longrightarrow>  
     Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
   by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
 
 (* Enabledness of some actions *)
-lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
-    |- \<not>Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
+lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
+    \<turnstile> \<not>Calling rcv p & Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
 
-lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
-      |- \<not>Calling rcv p & Calling send p & rst!p = #rpcB  
-         --> Enabled (RPCReply send rcv rst p)"
+lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
+      \<turnstile> \<not>Calling rcv p & Calling send p & rst!p = #rpcB  
+         \<longrightarrow> Enabled (RPCReply send rcv rst p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
 
 end