eliminated old defs;
authorwenzelm
Mon Jan 11 22:23:03 2016 +0100 (2016-01-11)
changeset 62146324bc1ffba12
parent 62145 5b946c81dfbf
child 62147 a1b666aaac1a
eliminated old defs;
src/HOL/TLA/Action.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/RPC.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Mon Jan 11 21:21:02 2016 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Mon Jan 11 22:23:03 2016 +0100
     1.3 @@ -9,25 +9,19 @@
     1.4  imports Stfun
     1.5  begin
     1.6  
     1.7 -
     1.8 -(** abstract syntax **)
     1.9 -
    1.10 -type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
    1.11 -type_synonym action   = "bool trfun"
    1.12 +type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a"
    1.13 +type_synonym action = "bool trfun"
    1.14  
    1.15  instance prod :: (world, world) world ..
    1.16  
    1.17 -consts
    1.18 -  (** abstract syntax **)
    1.19 -  before        :: "'a stfun \<Rightarrow> 'a trfun"
    1.20 -  after         :: "'a stfun \<Rightarrow> 'a trfun"
    1.21 -  unch          :: "'a stfun \<Rightarrow> action"
    1.22 +definition enabled :: "action \<Rightarrow> stpred"
    1.23 +  where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A"
    1.24 +
    1.25  
    1.26 -  SqAct         :: "[action, 'a stfun] \<Rightarrow> action"
    1.27 -  AnAct         :: "[action, 'a stfun] \<Rightarrow> action"
    1.28 -  enabled       :: "action \<Rightarrow> stpred"
    1.29 -
    1.30 -(** concrete syntax **)
    1.31 +consts
    1.32 +  before :: "'a stfun \<Rightarrow> 'a trfun"
    1.33 +  after :: "'a stfun \<Rightarrow> 'a trfun"
    1.34 +  unch :: "'a stfun \<Rightarrow> action"
    1.35  
    1.36  syntax
    1.37    (* Syntax for writing action expressions in arbitrary contexts *)
    1.38 @@ -40,8 +34,6 @@
    1.39    (*** Priming: same as "after" ***)
    1.40    "_prime"      :: "lift \<Rightarrow> lift"                    ("(_`)" [100] 99)
    1.41  
    1.42 -  "_SqAct"      :: "[lift, lift] \<Rightarrow> lift"            ("([_]'_(_))" [0,1000] 99)
    1.43 -  "_AnAct"      :: "[lift, lift] \<Rightarrow> lift"            ("(<_>'_(_))" [0,1000] 99)
    1.44    "_Enabled"    :: "lift \<Rightarrow> lift"                    ("(Enabled _)" [100] 100)
    1.45  
    1.46  translations
    1.47 @@ -50,25 +42,30 @@
    1.48    "_after"           ==   "CONST after"
    1.49    "_prime"           =>   "_after"
    1.50    "_unchanged"       ==   "CONST unch"
    1.51 -  "_SqAct"           ==   "CONST SqAct"
    1.52 -  "_AnAct"           ==   "CONST AnAct"
    1.53    "_Enabled"         ==   "CONST enabled"
    1.54 -  "w \<Turnstile> [A]_v"       <=   "_SqAct A v w"
    1.55 -  "w \<Turnstile> <A>_v"       <=   "_AnAct A v w"
    1.56    "s \<Turnstile> Enabled A"   <=   "_Enabled A s"
    1.57    "w \<Turnstile> unchanged f" <=   "_unchanged f w"
    1.58  
    1.59  axiomatization where
    1.60    unl_before:    "(ACT $v) (s,t) \<equiv> v s" and
    1.61    unl_after:     "(ACT v$) (s,t) \<equiv> v t" and
    1.62 -
    1.63    unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
    1.64  
    1.65 -defs
    1.66 -  square_def:    "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
    1.67 -  angle_def:     "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
    1.68 +
    1.69 +definition SqAct :: "[action, 'a stfun] \<Rightarrow> action"
    1.70 +  where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)"
    1.71 +
    1.72 +definition AnAct :: "[action, 'a stfun] \<Rightarrow> action"
    1.73 +  where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)"
    1.74  
    1.75 -  enabled_def:   "s \<Turnstile> Enabled A  \<equiv>  \<exists>u. (s,u) \<Turnstile> A"
    1.76 +syntax
    1.77 +  "_SqAct" :: "[lift, lift] \<Rightarrow> lift"  ("([_]'_(_))" [0, 1000] 99)
    1.78 +  "_AnAct" :: "[lift, lift] \<Rightarrow> lift"  ("(<_>'_(_))" [0, 1000] 99)
    1.79 +translations
    1.80 +  "_SqAct" == "CONST SqAct"
    1.81 +  "_AnAct" == "CONST AnAct"
    1.82 +  "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w"
    1.83 +  "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w"
    1.84  
    1.85  
    1.86  (* The following assertion specializes "intI" for any world type
     2.1 --- a/src/HOL/TLA/Init.thy	Mon Jan 11 21:21:02 2016 +0100
     2.2 +++ b/src/HOL/TLA/Init.thy	Mon Jan 11 22:23:03 2016 +0100
     2.3 @@ -16,25 +16,22 @@
     2.4  
     2.5  type_synonym temporal = "behavior form"
     2.6  
     2.7 -
     2.8  consts
     2.9 -  Initial     :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
    2.10    first_world :: "behavior \<Rightarrow> ('w::world)"
    2.11    st1         :: "behavior \<Rightarrow> state"
    2.12    st2         :: "behavior \<Rightarrow> state"
    2.13  
    2.14 +definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
    2.15 +  where Init_def: "Initial F sigma = F (first_world sigma)"
    2.16 +
    2.17  syntax
    2.18    "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
    2.19    "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
    2.20 -
    2.21  translations
    2.22    "TEMP F"   => "(F::behavior \<Rightarrow> _)"
    2.23    "_Init"    == "CONST Initial"
    2.24    "sigma \<Turnstile> Init F"  <= "_Init F sigma"
    2.25  
    2.26 -defs
    2.27 -  Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
    2.28 -
    2.29  overloading
    2.30    fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
    2.31    fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
     3.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Mon Jan 11 21:21:02 2016 +0100
     3.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Mon Jan 11 22:23:03 2016 +0100
     3.3 @@ -74,10 +74,10 @@
     3.4     unanswered call for that process.
     3.5  *)
     3.6  lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
     3.7 -  by (auto simp: Return_def MC_action_defs)
     3.8 +  by (auto simp: AReturn_def MC_action_defs)
     3.9  
    3.10  lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
    3.11 -  by (auto simp: Call_def MC_action_defs)
    3.12 +  by (auto simp: ACall_def MC_action_defs)
    3.13  
    3.14  
    3.15  (* Enabledness of actions *)
    3.16 @@ -86,7 +86,7 @@
    3.17        \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA   
    3.18           \<longrightarrow> Enabled (MClkFwd send rcv cst p)"
    3.19    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
    3.20 -    @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    3.21 +    @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    3.22      [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
    3.23  
    3.24  lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p)  \<longrightarrow>   
    3.25 @@ -103,7 +103,7 @@
    3.26    apply (tactic \<open>action_simp_tac @{context}
    3.27      [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
    3.28    apply (tactic \<open>action_simp_tac (@{context} addsimps
    3.29 -    [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
    3.30 +    [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}])
    3.31      [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
    3.32    done
    3.33  
     4.1 --- a/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:21:02 2016 +0100
     4.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 22:23:03 2016 +0100
     4.3 @@ -178,7 +178,7 @@
     4.4  *)
     4.5  
     4.6  lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
     4.7 -  by (auto simp: Return_def RM_action_defs)
     4.8 +  by (auto simp: AReturn_def RM_action_defs)
     4.9  
    4.10  (* Enabledness conditions *)
    4.11  
    4.12 @@ -191,7 +191,7 @@
    4.13    apply (tactic
    4.14      \<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
    4.15    apply (tactic
    4.16 -    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
    4.17 +    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
    4.18        @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
    4.19    done
    4.20  
     5.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Jan 11 21:21:02 2016 +0100
     5.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Jan 11 22:23:03 2016 +0100
     5.3 @@ -320,7 +320,7 @@
     5.4  (* ==================== Lemmas about the environment ============================== *)
     5.5  
     5.6  lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
     5.7 -  by (auto simp: ENext_def Call_def)
     5.8 +  by (auto simp: ENext_def ACall_def)
     5.9  
    5.10  (* ==================== Lemmas about the implementation's states ==================== *)
    5.11  
    5.12 @@ -333,7 +333,7 @@
    5.13  
    5.14  lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
    5.15           \<longrightarrow> (S2 rmhist p)$"
    5.16 -  by (force simp: ENext_def Call_def c_def r_def m_def
    5.17 +  by (force simp: ENext_def ACall_def c_def r_def m_def
    5.18      caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
    5.19  
    5.20  lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
    5.21 @@ -352,7 +352,7 @@
    5.22           \<longrightarrow> unchanged (rmhist!p)"
    5.23    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
    5.24      @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
    5.25 -    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
    5.26 +    @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
    5.27  
    5.28  
    5.29  (* ------------------------------ State S2 ---------------------------------------- *)
    5.30 @@ -367,7 +367,7 @@
    5.31           \<and> unchanged (e p, r p, m p, rmhist!p)
    5.32           \<longrightarrow> (S3 rmhist p)$"
    5.33    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
    5.34 -    @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
    5.35 +    @{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
    5.36      @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
    5.37  
    5.38  lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
    5.39 @@ -380,7 +380,7 @@
    5.40           \<longrightarrow> unchanged (rmhist!p)"
    5.41    using [[fast_solver]]
    5.42    by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
    5.43 -    MClkReply_def Return_def S_def S2_def)
    5.44 +    MClkReply_def AReturn_def S_def S2_def)
    5.45  
    5.46  (* ------------------------------ State S3 ---------------------------------------- *)
    5.47  
    5.48 @@ -405,7 +405,7 @@
    5.49           \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
    5.50    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
    5.51      @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
    5.52 -    @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
    5.53 +    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def},
    5.54      @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
    5.55      @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
    5.56  
    5.57 @@ -413,7 +413,7 @@
    5.58           \<and> unchanged (e p, c p, m p)
    5.59           \<longrightarrow> (S6 rmhist p)$"
    5.60    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
    5.61 -    @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
    5.62 +    @{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def},
    5.63      @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
    5.64      @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
    5.65  
    5.66 @@ -422,7 +422,7 @@
    5.67  
    5.68  lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
    5.69    by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
    5.70 -    Return_def r_def rtrner_def S_def S3_def Calling_def)
    5.71 +    AReturn_def r_def rtrner_def S_def S3_def Calling_def)
    5.72  
    5.73  (* ------------------------------ State S4 ---------------------------------------- *)
    5.74  
    5.75 @@ -441,7 +441,7 @@
    5.76           \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
    5.77    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
    5.78      @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
    5.79 -    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
    5.80 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
    5.81      @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
    5.82      @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
    5.83      @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
    5.84 @@ -455,7 +455,7 @@
    5.85           \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
    5.86    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
    5.87      @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
    5.88 -    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
    5.89 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
    5.90      @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
    5.91      @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
    5.92  
    5.93 @@ -471,12 +471,12 @@
    5.94  lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
    5.95           \<and> HNext rmhist p
    5.96           \<longrightarrow> (S5 rmhist p)$"
    5.97 -  by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
    5.98 +  by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def
    5.99      rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
   5.100  
   5.101  lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   5.102    by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
   5.103 -    Return_def m_def rtrner_def S_def S4_def Calling_def)
   5.104 +    AReturn_def m_def rtrner_def S_def S4_def Calling_def)
   5.105  
   5.106  (* ------------------------------ State S5 ---------------------------------------- *)
   5.107  
   5.108 @@ -493,14 +493,14 @@
   5.109  lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
   5.110         \<longrightarrow> (S6 rmhist p)$"
   5.111    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
   5.112 -    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
   5.113 +    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
   5.114      @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
   5.115      @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
   5.116  
   5.117  lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
   5.118           \<longrightarrow> (S6 rmhist p)$"
   5.119    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
   5.120 -    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
   5.121 +    @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
   5.122      @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
   5.123      @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
   5.124  
   5.125 @@ -511,7 +511,7 @@
   5.126           \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   5.127    using [[fast_solver]]
   5.128    by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
   5.129 -    MClkReply_def Return_def S_def S5_def)
   5.130 +    MClkReply_def AReturn_def S_def S5_def)
   5.131  
   5.132  (* ------------------------------ State S6 ---------------------------------------- *)
   5.133  
   5.134 @@ -526,7 +526,7 @@
   5.135           \<and> unchanged (e p,r p,m p)
   5.136           \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
   5.137    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
   5.138 -    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
   5.139 +    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def},
   5.140      @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
   5.141      @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
   5.142  
   5.143 @@ -534,7 +534,7 @@
   5.144           \<and> unchanged (e p,r p,m p)
   5.145           \<longrightarrow> (S1 rmhist p)$"
   5.146    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
   5.147 -    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
   5.148 +    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_def},
   5.149      @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
   5.150      @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
   5.151  
   5.152 @@ -545,7 +545,7 @@
   5.153    by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
   5.154  
   5.155  lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   5.156 -  by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
   5.157 +  by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
   5.158  
   5.159  
   5.160  section "Correctness of predicate-action diagram"
   5.161 @@ -676,7 +676,7 @@
   5.162    apply (drule S6_excl [temp_use])
   5.163    apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
   5.164      apply (force simp: S3_def S_def)
   5.165 -   apply (auto simp: Return_def)
   5.166 +   apply (auto simp: AReturn_def)
   5.167    done
   5.168  
   5.169  lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
   5.170 @@ -724,7 +724,7 @@
   5.171      @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
   5.172    apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   5.173    using [[fast_solver]]
   5.174 -  apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
   5.175 +  apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
   5.176    done
   5.177  
   5.178  lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
   5.179 @@ -733,7 +733,7 @@
   5.180    apply clarsimp
   5.181    apply (drule S5_excl [temp_use] S6_excl [temp_use])+
   5.182    apply (auto simp: e_def c_def m_def resbar_def)
   5.183 -   apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
   5.184 +   apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
   5.185    done
   5.186  
   5.187  lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
   5.188 @@ -741,7 +741,7 @@
   5.189           \<longrightarrow> MemFail memCh (resbar rmhist) p"
   5.190    apply clarsimp
   5.191    apply (drule S6_excl [temp_use])
   5.192 -  apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
   5.193 +  apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
   5.194     apply (auto simp: S5_def S_def)
   5.195    done
   5.196  
   5.197 @@ -752,7 +752,7 @@
   5.198    apply (drule S6_excl [temp_use])+
   5.199    apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
   5.200      @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
   5.201 -    @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
   5.202 +    @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
   5.203      apply simp_all (* simplify if-then-else *)
   5.204      apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
   5.205        [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
   5.206 @@ -909,7 +909,7 @@
   5.207  lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
   5.208           \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   5.209    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
   5.210 -    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
   5.211 +    @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
   5.212  
   5.213  lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
   5.214           \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   5.215 @@ -1088,7 +1088,7 @@
   5.216  lemma MClkReplyS6:
   5.217    "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
   5.218    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
   5.219 -    @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
   5.220 +    @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
   5.221      @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
   5.222  
   5.223  lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
     6.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 21:21:02 2016 +0100
     6.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Mon Jan 11 22:23:03 2016 +0100
     6.3 @@ -37,14 +37,13 @@
     6.4  
     6.5  (* slice through array-valued state function *)
     6.6  
     6.7 -consts
     6.8 -  slice        :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
     6.9 +definition slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
    6.10 +  where "slice x i s \<equiv> x s i"
    6.11 +
    6.12  syntax
    6.13 -  "_slice"    :: "[lift, 'a] \<Rightarrow> lift"      ("(_!_)" [70,70] 70)
    6.14 +  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  ("(_!_)" [70,70] 70)
    6.15  translations
    6.16 -  "_slice"  ==  "CONST slice"
    6.17 -defs
    6.18 -  slice_def:     "(PRED (x!i)) s == x s i"
    6.19 +  "_slice" \<rightleftharpoons> "CONST slice"
    6.20  
    6.21  
    6.22  (* state predicates *)
    6.23 @@ -55,22 +54,24 @@
    6.24  
    6.25  (* actions *)
    6.26  
    6.27 -consts
    6.28 -  ACall      :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
    6.29 -  AReturn    :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
    6.30 +definition ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
    6.31 +  where "ACall ch p v \<equiv> ACT
    6.32 +      \<not> $Calling ch p
    6.33 +    \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
    6.34 +    \<and> (arg<ch!p>$ = $v)"
    6.35 +
    6.36 +definition AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
    6.37 +  where "AReturn ch p v == ACT
    6.38 +      $Calling ch p
    6.39 +    \<and> (rbit<ch!p>$ = $cbit<ch!p>)
    6.40 +    \<and> (res<ch!p>$ = $v)"
    6.41 +
    6.42  syntax
    6.43 -  "_Call"     :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Call _ _ _)" [90,90,90] 90)
    6.44 -  "_Return"   :: "['a, 'b, lift] \<Rightarrow> lift"    ("(Return _ _ _)" [90,90,90] 90)
    6.45 +  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Call _ _ _)" [90,90,90] 90)
    6.46 +  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Return _ _ _)" [90,90,90] 90)
    6.47  translations
    6.48 -  "_Call"   ==  "CONST ACall"
    6.49 -  "_Return" ==  "CONST AReturn"
    6.50 -defs
    6.51 -  Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
    6.52 -                                     \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
    6.53 -                                     \<and> (arg<ch!p>$ = $v)"
    6.54 -  Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
    6.55 -                                     \<and> (rbit<ch!p>$ = $cbit<ch!p>)
    6.56 -                                     \<and> (res<ch!p>$ = $v)"
    6.57 +  "_Call" \<rightleftharpoons> "CONST ACall"
    6.58 +  "_Return" \<rightleftharpoons> "CONST AReturn"
    6.59  
    6.60  
    6.61  (* temporal formulas *)
    6.62 @@ -91,14 +92,14 @@
    6.63  
    6.64  declare slice_def [simp]
    6.65  
    6.66 -lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
    6.67 +lemmas Procedure_defs = caller_def rtrner_def Calling_def ACall_def AReturn_def
    6.68    PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
    6.69  
    6.70  (* Calls and returns change their subchannel *)
    6.71  lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
    6.72 -  by (auto simp: angle_def Call_def caller_def Calling_def)
    6.73 +  by (auto simp: angle_def ACall_def caller_def Calling_def)
    6.74  
    6.75  lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
    6.76 -  by (auto simp: angle_def Return_def rtrner_def Calling_def)
    6.77 +  by (auto simp: angle_def AReturn_def rtrner_def Calling_def)
    6.78  
    6.79  end
     7.1 --- a/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:21:02 2016 +0100
     7.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 22:23:03 2016 +0100
     7.3 @@ -83,7 +83,7 @@
     7.4  *)
     7.5  
     7.6  lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
     7.7 -  by (auto simp: Return_def RPC_action_defs)
     7.8 +  by (auto simp: AReturn_def RPC_action_defs)
     7.9  
    7.10  lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
    7.11    by (auto simp: RPC_action_defs)
    7.12 @@ -101,14 +101,14 @@
    7.13  lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
    7.14      \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
    7.15    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
    7.16 -    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    7.17 +    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    7.18      [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
    7.19  
    7.20  lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
    7.21        \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB  
    7.22           \<longrightarrow> Enabled (RPCReply send rcv rst p)"
    7.23    by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
    7.24 -    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    7.25 +    @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    7.26      [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
    7.27  
    7.28  end