eliminated old defs;

--- a/src/HOL/TLA/Action.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Action.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -9,25 +9,19 @@
 imports Stfun
 begin
 
-
-(** abstract syntax **)
-
-type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
-type_synonym action   = "bool trfun"
+type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a"
+type_synonym action = "bool trfun"
 
 instance prod :: (world, world) world ..
 
-consts
-  (** abstract syntax **)
-  before        :: "'a stfun \<Rightarrow> 'a trfun"
-  after         :: "'a stfun \<Rightarrow> 'a trfun"
-  unch          :: "'a stfun \<Rightarrow> action"
+definition enabled :: "action \<Rightarrow> stpred"
+  where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A"
+
 
-  SqAct         :: "[action, 'a stfun] \<Rightarrow> action"
-  AnAct         :: "[action, 'a stfun] \<Rightarrow> action"
-  enabled       :: "action \<Rightarrow> stpred"
-
-(** concrete syntax **)
+consts
+  before :: "'a stfun \<Rightarrow> 'a trfun"
+  after :: "'a stfun \<Rightarrow> 'a trfun"
+  unch :: "'a stfun \<Rightarrow> action"
 
 syntax
   (* Syntax for writing action expressions in arbitrary contexts *)
@@ -40,8 +34,6 @@
   (*** Priming: same as "after" ***)
   "_prime"      :: "lift \<Rightarrow> lift"                    ("(_`)" [100] 99)
 
-  "_SqAct"      :: "[lift, lift] \<Rightarrow> lift"            ("([_]'_(_))" [0,1000] 99)
-  "_AnAct"      :: "[lift, lift] \<Rightarrow> lift"            ("(<_>'_(_))" [0,1000] 99)
   "_Enabled"    :: "lift \<Rightarrow> lift"                    ("(Enabled _)" [100] 100)
 
 translations
@@ -50,25 +42,30 @@
   "_after"           ==   "CONST after"
   "_prime"           =>   "_after"
   "_unchanged"       ==   "CONST unch"
-  "_SqAct"           ==   "CONST SqAct"
-  "_AnAct"           ==   "CONST AnAct"
   "_Enabled"         ==   "CONST enabled"
-  "w \<Turnstile> [A]_v"       <=   "_SqAct A v w"
-  "w \<Turnstile> <A>_v"       <=   "_AnAct A v w"
   "s \<Turnstile> Enabled A"   <=   "_Enabled A s"
   "w \<Turnstile> unchanged f" <=   "_unchanged f w"
 
 axiomatization where
   unl_before:    "(ACT $v) (s,t) \<equiv> v s" and
   unl_after:     "(ACT v$) (s,t) \<equiv> v t" and
-
   unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
 
-defs
-  square_def:    "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
-  angle_def:     "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
+
+definition SqAct :: "[action, 'a stfun] \<Rightarrow> action"
+  where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)"
+
+definition AnAct :: "[action, 'a stfun] \<Rightarrow> action"
+  where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)"
 
-  enabled_def:   "s \<Turnstile> Enabled A  \<equiv>  \<exists>u. (s,u) \<Turnstile> A"
+syntax
+  "_SqAct" :: "[lift, lift] \<Rightarrow> lift"  ("([_]'_(_))" [0, 1000] 99)
+  "_AnAct" :: "[lift, lift] \<Rightarrow> lift"  ("(<_>'_(_))" [0, 1000] 99)
+translations
+  "_SqAct" == "CONST SqAct"
+  "_AnAct" == "CONST AnAct"
+  "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w"
+  "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w"
 
 
 (* The following assertion specializes "intI" for any world type

--- a/src/HOL/TLA/Init.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Init.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -16,25 +16,22 @@
 
 type_synonym temporal = "behavior form"
 
-
 consts
-  Initial     :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
   first_world :: "behavior \<Rightarrow> ('w::world)"
   st1         :: "behavior \<Rightarrow> state"
   st2         :: "behavior \<Rightarrow> state"
 
+definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
+  where Init_def: "Initial F sigma = F (first_world sigma)"
+
 syntax
   "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
   "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
-
 translations
   "TEMP F"   => "(F::behavior \<Rightarrow> _)"
   "_Init"    == "CONST Initial"
   "sigma \<Turnstile> Init F"  <= "_Init F sigma"
 
-defs
-  Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
-
 overloading
   fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
   fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"

--- a/src/HOL/TLA/Memory/MemClerk.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -74,10 +74,10 @@
    unanswered call for that process.
 *)
 lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
-  by (auto simp: Return_def MC_action_defs)
+  by (auto simp: AReturn_def MC_action_defs)
 
 lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
-  by (auto simp: Call_def MC_action_defs)
+  by (auto simp: ACall_def MC_action_defs)
 
 
 (* Enabledness of actions *)
@@ -86,7 +86,7 @@
       \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA   
          \<longrightarrow> Enabled (MClkFwd send rcv cst p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
-    @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p)  \<longrightarrow>   
@@ -103,7 +103,7 @@
   apply (tactic \<open>action_simp_tac @{context}
     [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
   apply (tactic \<open>action_simp_tac (@{context} addsimps
-    [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
+    [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}])
     [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 

--- a/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -178,7 +178,7 @@
 *)
 
 lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
-  by (auto simp: Return_def RM_action_defs)
+  by (auto simp: AReturn_def RM_action_defs)
 
 (* Enabledness conditions *)
 
@@ -191,7 +191,7 @@
   apply (tactic
     \<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
   apply (tactic
-    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
+    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
       @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 

--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -320,7 +320,7 @@
 (* ==================== Lemmas about the environment ============================== *)
 
 lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
-  by (auto simp: ENext_def Call_def)
+  by (auto simp: ENext_def ACall_def)
 
 (* ==================== Lemmas about the implementation's states ==================== *)
 
@@ -333,7 +333,7 @@
 
 lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
          \<longrightarrow> (S2 rmhist p)$"
-  by (force simp: ENext_def Call_def c_def r_def m_def
+  by (force simp: ENext_def ACall_def c_def r_def m_def
     caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
 
 lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
@@ -352,7 +352,7 @@
          \<longrightarrow> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
     @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
-    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
+    @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
 
 
 (* ------------------------------ State S2 ---------------------------------------- *)
@@ -367,7 +367,7 @@
          \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> (S3 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
-    @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
+    @{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
     @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
@@ -380,7 +380,7 @@
          \<longrightarrow> unchanged (rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
-    MClkReply_def Return_def S_def S2_def)
+    MClkReply_def AReturn_def S_def S2_def)
 
 (* ------------------------------ State S3 ---------------------------------------- *)
 
@@ -405,7 +405,7 @@
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
     @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
-    @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
+    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def},
     @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
     @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -413,7 +413,7 @@
          \<and> unchanged (e p, c p, m p)
          \<longrightarrow> (S6 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
-    @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
+    @{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def},
     @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
     @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -422,7 +422,7 @@
 
 lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
   by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
-    Return_def r_def rtrner_def S_def S3_def Calling_def)
+    AReturn_def r_def rtrner_def S_def S3_def Calling_def)
 
 (* ------------------------------ State S4 ---------------------------------------- *)
 
@@ -441,7 +441,7 @@
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
     @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
-    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
     @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
     @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
@@ -455,7 +455,7 @@
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
     @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
-    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
     @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -471,12 +471,12 @@
 lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
          \<and> HNext rmhist p
          \<longrightarrow> (S5 rmhist p)$"
-  by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
+  by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def
     rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
 
 lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
-    Return_def m_def rtrner_def S_def S4_def Calling_def)
+    AReturn_def m_def rtrner_def S_def S4_def Calling_def)
 
 (* ------------------------------ State S5 ---------------------------------------- *)
 
@@ -493,14 +493,14 @@
 lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
        \<longrightarrow> (S6 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
-    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
+    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
     @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
          \<longrightarrow> (S6 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
-    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
+    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -511,7 +511,7 @@
          \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
-    MClkReply_def Return_def S_def S5_def)
+    MClkReply_def AReturn_def S_def S5_def)
 
 (* ------------------------------ State S6 ---------------------------------------- *)
 
@@ -526,7 +526,7 @@
          \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
-    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
+    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -534,7 +534,7 @@
          \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S1 rmhist p)$"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
-    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
+    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
@@ -545,7 +545,7 @@
   by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
 
 lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
-  by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
+  by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
 
 
 section "Correctness of predicate-action diagram"
@@ -676,7 +676,7 @@
   apply (drule S6_excl [temp_use])
   apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
     apply (force simp: S3_def S_def)
-   apply (auto simp: Return_def)
+   apply (auto simp: AReturn_def)
   done
 
 lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
@@ -724,7 +724,7 @@
     @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
   apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   using [[fast_solver]]
-  apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
+  apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
   done
 
 lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -733,7 +733,7 @@
   apply clarsimp
   apply (drule S5_excl [temp_use] S6_excl [temp_use])+
   apply (auto simp: e_def c_def m_def resbar_def)
-   apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
+   apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
   done
 
 lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -741,7 +741,7 @@
          \<longrightarrow> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])
-  apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
+  apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
    apply (auto simp: S5_def S_def)
   done
 
@@ -752,7 +752,7 @@
   apply (drule S6_excl [temp_use])+
   apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
     @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
-    @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
+    @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
     apply simp_all (* simplify if-then-else *)
     apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
       [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
@@ -909,7 +909,7 @@
 lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
          \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
-    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
+    @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
 
 lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
          \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -1088,7 +1088,7 @@
 lemma MClkReplyS6:
   "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
-    @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
+    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
     @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
 
 lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"

--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -37,14 +37,13 @@
 
 (* slice through array-valued state function *)
 
-consts
-  slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+definition slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+  where "slice x i s \<equiv> x s i"
+
 syntax
-  "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
+  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  ("(_!_)" [70,70] 70)
 translations
-  "_slice"  ==  "CONST slice"
-defs
-  slice_def:     "(PRED (x!i)) s == x s i"
+  "_slice" \<rightleftharpoons> "CONST slice"
 
 
 (* state predicates *)
@@ -55,22 +54,24 @@
 
 (* actions *)
 
-consts
-  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
-  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+definition ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+  where "ACall ch p v \<equiv> ACT
+      \<not> $Calling ch p
+    \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
+    \<and> (arg<ch!p>$ = $v)"
+
+definition AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+  where "AReturn ch p v == ACT
+      $Calling ch p
+    \<and> (rbit<ch!p>$ = $cbit<ch!p>)
+    \<and> (res<ch!p>$ = $v)"
+
 syntax
-  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
-  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
+  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Call _ _ _)" [90,90,90] 90)
+  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Return _ _ _)" [90,90,90] 90)
 translations
-  "_Call"   ==  "CONST ACall"
-  "_Return" ==  "CONST AReturn"
-defs
-  Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
-                                     \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
-                                     \<and> (arg<ch!p>$ = $v)"
-  Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
-                                     \<and> (rbit<ch!p>$ = $cbit<ch!p>)
-                                     \<and> (res<ch!p>$ = $v)"
+  "_Call" \<rightleftharpoons> "CONST ACall"
+  "_Return" \<rightleftharpoons> "CONST AReturn"
 
 
 (* temporal formulas *)
@@ -91,14 +92,14 @@
 
 declare slice_def [simp]
 
-lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
+lemmas Procedure_defs = caller_def rtrner_def Calling_def ACall_def AReturn_def
   PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
 
 (* Calls and returns change their subchannel *)
 lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
-  by (auto simp: angle_def Call_def caller_def Calling_def)
+  by (auto simp: angle_def ACall_def caller_def Calling_def)
 
 lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
-  by (auto simp: angle_def Return_def rtrner_def Calling_def)
+  by (auto simp: angle_def AReturn_def rtrner_def Calling_def)
 
 end

--- a/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -83,7 +83,7 @@
 *)
 
 lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
-  by (auto simp: Return_def RPC_action_defs)
+  by (auto simp: AReturn_def RPC_action_defs)
 
 lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
   by (auto simp: RPC_action_defs)
@@ -101,14 +101,14 @@
 lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
     \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
-    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
       \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB  
          \<longrightarrow> Enabled (RPCReply send rcv rst p)"
   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
-    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 end