src/HOL/TLA/Memory/RPC.thy
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 41589 bbd861837ebc
child 42018 878f33040280
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41589
bbd861837ebc tuned headers;
wenzelm
parents: 39159
diff changeset
     1
(*  Title:      HOL/TLA/Memory/RPC.thy
bbd861837ebc tuned headers;
wenzelm
parents: 39159
diff changeset
     2
    Author:     Stephan Merz, University of Munich
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
     3
*)
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     4
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
     5
header {* RPC-Memory example: RPC specification *}
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
     6
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
     7
theory RPC
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
     8
imports RPCParameters ProcedureInterface Memory
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
     9
begin
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    10
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    11
types
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    12
  rpcSndChType  = "(rpcOp,Vals) channel"
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    13
  rpcRcvChType  = "memChType"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    14
  rpcStType     = "(PrIds => rpcState) stfun"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    15
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    16
consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    17
  (* state predicates *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    18
  RPCInit      :: "rpcRcvChType => rpcStType => PrIds => stpred"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    19
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    20
  (* actions *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    21
  RPCFwd     :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    22
  RPCReject  :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    23
  RPCFail    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    24
  RPCReply   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    25
  RPCNext    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    26
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    27
  (* temporal *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    28
  RPCIPSpec   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    29
  RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    30
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    31
defs
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    32
  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    33
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    34
  RPCFwd_def:        "RPCFwd send rcv rst p == ACT
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    35
                         $(Calling send p)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    36
                         & $(rst!p) = # rpcA
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    37
                         & IsLegalRcvArg<arg<$(send!p)>>
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    38
                         & Call rcv p RPCRelayArg<arg<send!p>>
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    39
                         & (rst!p)$ = # rpcB
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    40
                         & unchanged (rtrner send!p)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    41
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    42
  RPCReject_def:     "RPCReject send rcv rst p == ACT
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    43
                           $(rst!p) = # rpcA
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    44
                         & ~IsLegalRcvArg<arg<$(send!p)>>
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    45
                         & Return send p #BadCall
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    46
                         & unchanged ((rst!p), (caller rcv!p))"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    47
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    48
  RPCFail_def:       "RPCFail send rcv rst p == ACT
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    49
                           ~$(Calling rcv p)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    50
                         & Return send p #RPCFailure
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    51
                         & (rst!p)$ = #rpcA
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    52
                         & unchanged (caller rcv!p)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    53
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    54
  RPCReply_def:      "RPCReply send rcv rst p == ACT
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    55
                           ~$(Calling rcv p)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    56
                         & $(rst!p) = #rpcB
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    57
                         & Return send p res<rcv!p>
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    58
                         & (rst!p)$ = #rpcA
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    59
                         & unchanged (caller rcv!p)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    60
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    61
  RPCNext_def:       "RPCNext send rcv rst p == ACT
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    62
                        (  RPCFwd send rcv rst p
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    63
                         | RPCReject send rcv rst p
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    64
                         | RPCFail send rcv rst p
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    65
                         | RPCReply send rcv rst p)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    66
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    67
  RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    68
                           Init RPCInit rcv rst p
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    69
                         & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    70
                         & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    71
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    72
  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 11703
diff changeset
    73
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    74
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    75
lemmas RPC_action_defs =
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    76
  RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    77
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    78
lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    79
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    80
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    81
(* The RPC component engages in an action for process p only if there is an outstanding,
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    82
   unanswered call for that process.
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    83
*)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    84
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    85
lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    86
  by (auto simp: Return_def RPC_action_defs)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    87
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    88
lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    89
  by (auto simp: RPC_action_defs)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    90
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    91
(* RPC failure actions are visible. *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    92
lemma RPCFail_vis: "|- RPCFail send rcv rst p -->  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    93
    <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    94
  by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    95
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    96
lemma RPCFail_Next_enabled: "|- Enabled (RPCFail send rcv rst p) -->  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    97
    Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    98
  by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    99
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   100
(* Enabledness of some actions *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   101
lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   102
    |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 26342
diff changeset
   103
  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
0dec18004e75 more antiquotations;
wenzelm
parents: 26342
diff changeset
   104
    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
0dec18004e75 more antiquotations;
wenzelm
parents: 26342
diff changeset
   105
    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   106
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   107
lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   108
      |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
   109
         --> Enabled (RPCReply send rcv rst p)"
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 26342
diff changeset
   110
  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
0dec18004e75 more antiquotations;
wenzelm
parents: 26342
diff changeset
   111
    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
0dec18004e75 more antiquotations;
wenzelm
parents: 26342
diff changeset
   112
    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
   113
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
   114
end