src/HOL/TLA/Memory/ProcedureInterface.thy
author wenzelm
Sun, 16 Jan 2011 15:53:03 +0100
changeset 41589 bbd861837ebc
parent 35068 544867142ea4
child 42018 878f33040280
permissions -rw-r--r--
tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41589
bbd861837ebc tuned headers;
wenzelm
parents: 35068
diff changeset
     1
(*  Title:      HOL/TLA/Memory/ProcedureInterface.thy
bbd861837ebc tuned headers;
wenzelm
parents: 35068
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 {* Procedure interface for RPC-Memory components *}
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: 12338
diff changeset
     7
theory ProcedureInterface
26351
d5125a62f839 tuned import
haftmann
parents: 21624
diff changeset
     8
imports "../TLA" RPCMemoryParams
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
     9
begin
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    10
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    11
typedecl
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    12
  (* type of channels with argument type 'a and return type 'r.
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    13
     we model a channel as an array of variables (of type chan)
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    14
     rather than a single array-valued variable because the
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    15
     notation gets a little simpler.
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    16
  *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    17
  ('a,'r) chan
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    18
types
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    19
  ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    20
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    21
consts
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    22
  (* data-level functions *)
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    23
  cbit          :: "('a,'r) chan => bit"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    24
  rbit          :: "('a,'r) chan => bit"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    25
  arg           :: "('a,'r) chan => 'a"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    26
  res           :: "('a,'r) chan => 'r"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    27
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    28
  (* state functions *)
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    29
  caller        :: "('a,'r) channel => (PrIds => (bit * 'a)) stfun"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    30
  rtrner        :: "('a,'r) channel => (PrIds => (bit * 'r)) stfun"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    31
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    32
  (* state predicates *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    33
  Calling   :: "('a,'r) channel => PrIds => stpred"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    34
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    35
  (* actions *)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    36
  ACall      :: "('a,'r) channel => PrIds => 'a stfun => action"
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    37
  AReturn    :: "('a,'r) channel => PrIds => 'r stfun => action"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    38
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    39
  (* temporal formulas *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    40
  PLegalCaller      :: "('a,'r) channel => PrIds => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    41
  LegalCaller       :: "('a,'r) channel => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    42
  PLegalReturner    :: "('a,'r) channel => PrIds => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    43
  LegalReturner     :: "('a,'r) channel => temporal"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    44
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    45
  (* slice through array-valued state function *)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    46
  slice        :: "('a => 'b) stfun => 'a => 'b stfun"
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    47
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    48
syntax
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    49
  "_slice"    :: "[lift, 'a] => lift"      ("(_!_)" [70,70] 70)
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    50
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    51
  "_Call"     :: "['a, 'b, lift] => lift"    ("(Call _ _ _)" [90,90,90] 90)
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    52
  "_Return"   :: "['a, 'b, lift] => lift"    ("(Return _ _ _)" [90,90,90] 90)
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    53
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    54
translations
35068
544867142ea4 modernized translations;
wenzelm
parents: 26351
diff changeset
    55
  "_slice"  ==  "CONST slice"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    56
35068
544867142ea4 modernized translations;
wenzelm
parents: 26351
diff changeset
    57
  "_Call"   ==  "CONST ACall"
544867142ea4 modernized translations;
wenzelm
parents: 26351
diff changeset
    58
  "_Return" ==  "CONST AReturn"
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    59
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    60
defs
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    61
  slice_def:     "(PRED (x!i)) s == x s i"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    62
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    63
  caller_def:    "caller ch   == %s p. (cbit (ch s p), arg (ch s p))"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    64
  rtrner_def:    "rtrner ch   == %s p. (rbit (ch s p), res (ch s p))"
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    65
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    66
  Calling_def:   "Calling ch p  == PRED cbit< ch!p > ~= rbit< ch!p >"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    67
  Call_def:      "(ACT Call ch p v)   == ACT  ~ $Calling ch p
9517
f58863b1406a tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents: 6255
diff changeset
    68
                                     & (cbit<ch!p>$ ~= $rbit<ch!p>)
f58863b1406a tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents: 6255
diff changeset
    69
                                     & (arg<ch!p>$ = $v)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    70
  Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
9517
f58863b1406a tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents: 6255
diff changeset
    71
                                     & (rbit<ch!p>$ = $cbit<ch!p>)
f58863b1406a tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents: 6255
diff changeset
    72
                                     & (res<ch!p>$ = $v)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    73
  PLegalCaller_def:      "PLegalCaller ch p == TEMP
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    74
                             Init(~ Calling ch p)
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    75
                             & [][ ? a. Call ch p a ]_((caller ch)!p)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    76
  LegalCaller_def:       "LegalCaller ch == TEMP (! p. PLegalCaller ch p)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    77
  PLegalReturner_def:    "PLegalReturner ch p == TEMP
6255
db63752140c7 updated (Stephan Merz);
wenzelm
parents: 3807
diff changeset
    78
                                [][ ? v. Return ch p v ]_((rtrner ch)!p)"
17309
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    79
  LegalReturner_def:     "LegalReturner ch == TEMP (! p. PLegalReturner ch p)"
c43ed29bd197 converted to Isar theory format;
wenzelm
parents: 12338
diff changeset
    80
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    81
declare slice_def [simp]
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    82
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    83
lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    84
  PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    85
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    86
(* Calls and returns change their subchannel *)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    87
lemma Call_changed: "|- Call ch p v --> <Call ch p v>_((caller ch)!p)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    88
  by (auto simp: angle_def Call_def caller_def Calling_def)
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    89
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    90
lemma Return_changed: "|- Return ch p v --> <Return ch p v>_((rtrner ch)!p)"
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 17309
diff changeset
    91
  by (auto simp: angle_def Return_def rtrner_def Calling_def)
3807
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    92
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz;
wenzelm
parents:
diff changeset
    93
end