src/HOL/TLA/Memory/ProcedureInterface.thy
changeset 60587 0318b43ee95c
parent 58889 5b7a9633cfa8
child 60588 750c533459b1
equal deleted inserted replaced
60586:1d31e3a50373 60587:0318b43ee95c
    56   "_Return" ==  "CONST AReturn"
    56   "_Return" ==  "CONST AReturn"
    57 
    57 
    58 defs
    58 defs
    59   slice_def:     "(PRED (x!i)) s == x s i"
    59   slice_def:     "(PRED (x!i)) s == x s i"
    60 
    60 
    61   caller_def:    "caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
    61   caller_def:    "caller ch   == \<lambda>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))"
    62   rtrner_def:    "rtrner ch   == \<lambda>s p. (rbit (ch s p), res (ch s p))"
    63 
    63 
    64   Calling_def:   "Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
    64   Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
    65   Call_def:      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
    65   Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
    66                                      & (cbit<ch!p>$ ~= $rbit<ch!p>)
    66                                      & (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
    67                                      & (arg<ch!p>$ = $v)"
    67                                      & (arg<ch!p>$ = $v)"
    68   Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
    68   Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
    69                                      & (rbit<ch!p>$ = $cbit<ch!p>)
    69                                      & (rbit<ch!p>$ = $cbit<ch!p>)
    70                                      & (res<ch!p>$ = $v)"
    70                                      & (res<ch!p>$ = $v)"
    71   PLegalCaller_def:      "PLegalCaller ch p == TEMP
    71   PLegalCaller_def:      "PLegalCaller ch p == TEMP
    72                              Init(~ Calling ch p)
    72                              Init(\<not> Calling ch p)
    73                              & [][ ? a. Call ch p a ]_((caller ch)!p)"
    73                              & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
    74   LegalCaller_def:       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
    74   LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
    75   PLegalReturner_def:    "PLegalReturner ch p == TEMP
    75   PLegalReturner_def:    "PLegalReturner ch p == TEMP
    76                                 [][ ? v. Return ch p v ]_((rtrner ch)!p)"
    76                                 \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
    77   LegalReturner_def:     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
    77   LegalReturner_def:     "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)"
    78 
    78 
    79 declare slice_def [simp]
    79 declare slice_def [simp]
    80 
    80 
    81 lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
    81 lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
    82   PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
    82   PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def