src/HOL/TLA/Memory/ProcedureInterface.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 58889 5b7a9633cfa8
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/ProcedureInterface.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* Procedure interface for RPC-Memory components *}
     6 
     7 theory ProcedureInterface
     8 imports "../TLA" RPCMemoryParams
     9 begin
    10 
    11 typedecl ('a,'r) chan
    12   (* type of channels with argument type 'a and return type 'r.
    13      we model a channel as an array of variables (of type chan)
    14      rather than a single array-valued variable because the
    15      notation gets a little simpler.
    16   *)
    17 type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
    18 
    19 consts
    20   (* data-level functions *)
    21   cbit          :: "('a,'r) chan => bit"
    22   rbit          :: "('a,'r) chan => bit"
    23   arg           :: "('a,'r) chan => 'a"
    24   res           :: "('a,'r) chan => 'r"
    25 
    26   (* state functions *)
    27   caller        :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
    28   rtrner        :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
    29 
    30   (* state predicates *)
    31   Calling   :: "('a,'r) channel => PrIds => stpred"
    32 
    33   (* actions *)
    34   ACall      :: "('a,'r) channel => PrIds => 'a stfun => action"
    35   AReturn    :: "('a,'r) channel => PrIds => 'r stfun => action"
    36 
    37   (* temporal formulas *)
    38   PLegalCaller      :: "('a,'r) channel => PrIds => temporal"
    39   LegalCaller       :: "('a,'r) channel => temporal"
    40   PLegalReturner    :: "('a,'r) channel => PrIds => temporal"
    41   LegalReturner     :: "('a,'r) channel => temporal"
    42 
    43   (* slice through array-valued state function *)
    44   slice        :: "('a => 'b) stfun => 'a => 'b stfun"
    45 
    46 syntax
    47   "_slice"    :: "[lift, 'a] => lift"      ("(_!_)" [70,70] 70)
    48 
    49   "_Call"     :: "['a, 'b, lift] => lift"    ("(Call _ _ _)" [90,90,90] 90)
    50   "_Return"   :: "['a, 'b, lift] => lift"    ("(Return _ _ _)" [90,90,90] 90)
    51 
    52 translations
    53   "_slice"  ==  "CONST slice"
    54 
    55   "_Call"   ==  "CONST ACall"
    56   "_Return" ==  "CONST AReturn"
    57 
    58 defs
    59   slice_def:     "(PRED (x!i)) s == x s i"
    60 
    61   caller_def:    "caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
    62   rtrner_def:    "rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
    63 
    64   Calling_def:   "Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
    65   Call_def:      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
    66                                      & (cbit<ch!p>$ ~= $rbit<ch!p>)
    67                                      & (arg<ch!p>$ = $v)"
    68   Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
    69                                      & (rbit<ch!p>$ = $cbit<ch!p>)
    70                                      & (res<ch!p>$ = $v)"
    71   PLegalCaller_def:      "PLegalCaller ch p == TEMP
    72                              Init(~ Calling ch p)
    73                              & [][ ? a. Call ch p a ]_((caller ch)!p)"
    74   LegalCaller_def:       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
    75   PLegalReturner_def:    "PLegalReturner ch p == TEMP
    76                                 [][ ? v. Return ch p v ]_((rtrner ch)!p)"
    77   LegalReturner_def:     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
    78 
    79 declare slice_def [simp]
    80 
    81 lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
    82   PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
    83 
    84 (* Calls and returns change their subchannel *)
    85 lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"
    86   by (auto simp: angle_def Call_def caller_def Calling_def)
    87 
    88 lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"
    89   by (auto simp: angle_def Return_def rtrner_def Calling_def)
    90 
    91 end