src/HOL/TLA/Memory/MemClerk.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 51717 9e7d1c139569
child 60587 0318b43ee95c
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@41589
     1
(*  Title:      HOL/TLA/Memory/MemClerk.thy
wenzelm@41589
     2
    Author:     Stephan Merz, University of Munich
wenzelm@21624
     3
*)
wenzelm@3807
     4
wenzelm@58889
     5
section {* RPC-Memory example: specification of the memory clerk *}
wenzelm@3807
     6
wenzelm@17309
     7
theory MemClerk
wenzelm@17309
     8
imports Memory RPC MemClerkParameters
wenzelm@17309
     9
begin
wenzelm@3807
    10
wenzelm@42018
    11
(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
wenzelm@42018
    12
type_synonym mClkSndChType = "memChType"
wenzelm@42018
    13
type_synonym mClkRcvChType = "rpcSndChType"
wenzelm@42018
    14
type_synonym mClkStType = "(PrIds => mClkState) stfun"
wenzelm@3807
    15
wenzelm@36866
    16
definition
wenzelm@3807
    17
  (* state predicates *)
wenzelm@3807
    18
  MClkInit      :: "mClkRcvChType => mClkStType => PrIds => stpred"
wenzelm@36866
    19
  where "MClkInit rcv cst p = PRED (cst!p = #clkA  &  ~Calling rcv p)"
wenzelm@3807
    20
wenzelm@36866
    21
definition
wenzelm@3807
    22
  (* actions *)
wenzelm@3807
    23
  MClkFwd       :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
wenzelm@36866
    24
  where "MClkFwd send rcv cst p = ACT
wenzelm@6255
    25
                           $Calling send p
wenzelm@6255
    26
                         & $(cst!p) = #clkA
wenzelm@6255
    27
                         & Call rcv p MClkRelayArg<arg<send!p>>
wenzelm@6255
    28
                         & (cst!p)$ = #clkB
wenzelm@6255
    29
                         & unchanged (rtrner send!p)"
wenzelm@6255
    30
wenzelm@36866
    31
definition
wenzelm@3807
    32
  MClkRetry     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
wenzelm@36866
    33
  where "MClkRetry send rcv cst p = ACT
wenzelm@6255
    34
                           $(cst!p) = #clkB
wenzelm@6255
    35
                         & res<$(rcv!p)> = #RPCFailure
wenzelm@6255
    36
                         & Call rcv p MClkRelayArg<arg<send!p>>
wenzelm@6255
    37
                         & unchanged (cst!p, rtrner send!p)"
wenzelm@6255
    38
wenzelm@36866
    39
definition
wenzelm@3807
    40
  MClkReply     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
wenzelm@36866
    41
  where "MClkReply send rcv cst p = ACT
wenzelm@6255
    42
                           ~$Calling rcv p
wenzelm@6255
    43
                         & $(cst!p) = #clkB
wenzelm@6255
    44
                         & Return send p MClkReplyVal<res<rcv!p>>
wenzelm@6255
    45
                         & (cst!p)$ = #clkA
wenzelm@6255
    46
                         & unchanged (caller rcv!p)"
wenzelm@6255
    47
wenzelm@36866
    48
definition
wenzelm@3807
    49
  MClkNext      :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
wenzelm@36866
    50
  where "MClkNext send rcv cst p = ACT
wenzelm@6255
    51
                        (  MClkFwd send rcv cst p
wenzelm@6255
    52
                         | MClkRetry send rcv cst p
wenzelm@6255
    53
                         | MClkReply send rcv cst p)"
wenzelm@6255
    54
wenzelm@36866
    55
definition
wenzelm@3807
    56
  (* temporal *)
wenzelm@3807
    57
  MClkIPSpec    :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
wenzelm@36866
    58
  where "MClkIPSpec send rcv cst p = TEMP
wenzelm@6255
    59
                           Init MClkInit rcv cst p
wenzelm@6255
    60
                         & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
wenzelm@6255
    61
                         & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
wenzelm@6255
    62
                         & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
wenzelm@3807
    63
wenzelm@36866
    64
definition
wenzelm@6255
    65
  MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
wenzelm@36866
    66
  where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)"
wenzelm@3807
    67
wenzelm@21624
    68
lemmas MC_action_defs =
wenzelm@21624
    69
  MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def
wenzelm@21624
    70
wenzelm@21624
    71
lemmas MC_temp_defs = MClkIPSpec_def MClkISpec_def
wenzelm@21624
    72
wenzelm@21624
    73
(* The Clerk engages in an action for process p only if there is an outstanding,
wenzelm@21624
    74
   unanswered call for that process.
wenzelm@21624
    75
*)
wenzelm@21624
    76
lemma MClkidle: "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"
wenzelm@21624
    77
  by (auto simp: Return_def MC_action_defs)
wenzelm@21624
    78
wenzelm@21624
    79
lemma MClkbusy: "|- $Calling rcv p --> ~MClkNext send rcv cst p"
wenzelm@21624
    80
  by (auto simp: Call_def MC_action_defs)
wenzelm@21624
    81
wenzelm@21624
    82
wenzelm@21624
    83
(* Enabledness of actions *)
wenzelm@21624
    84
wenzelm@21624
    85
lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
wenzelm@21624
    86
      |- Calling send p & ~Calling rcv p & cst!p = #clkA   
wenzelm@21624
    87
         --> Enabled (MClkFwd send rcv cst p)"
wenzelm@51717
    88
  by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
haftmann@26359
    89
    @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
haftmann@26359
    90
    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
wenzelm@21624
    91
wenzelm@21624
    92
lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p)  -->   
wenzelm@21624
    93
         Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
wenzelm@21624
    94
  by (auto elim!: enabled_mono simp: angle_def MClkFwd_def)
wenzelm@21624
    95
wenzelm@21624
    96
lemma MClkReply_change: "|- MClkReply send rcv cst p -->  
wenzelm@21624
    97
         <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
wenzelm@21624
    98
  by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use])
wenzelm@21624
    99
wenzelm@21624
   100
lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
wenzelm@21624
   101
      |- Calling send p & ~Calling rcv p & cst!p = #clkB   
wenzelm@21624
   102
         --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
wenzelm@51717
   103
  apply (tactic {* action_simp_tac @{context}
haftmann@26359
   104
    [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
wenzelm@51717
   105
  apply (tactic {* action_simp_tac (@{context} addsimps
haftmann@26359
   106
    [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
haftmann@26359
   107
    [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
wenzelm@21624
   108
  done
wenzelm@21624
   109
wenzelm@21624
   110
lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
wenzelm@21624
   111
  by (auto simp: MClkReply_def MClkRetry_def)
wenzelm@17309
   112
wenzelm@3807
   113
end