src/HOL/TLA/Stfun.thy
 author wenzelm Wed Oct 08 11:50:33 1997 +0200 (1997-10-08) changeset 3807 82a99b090d9d child 6255 db63752140c7 permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
```     1 (*
```
```     2     File:	 TLA/Stfun.thy
```
```     3     Author:      Stephan Merz
```
```     4     Copyright:   1997 University of Munich
```
```     5
```
```     6     Theory Name: Stfun
```
```     7     Logic Image: HOL
```
```     8
```
```     9 States and state functions for TLA
```
```    10 *)
```
```    11
```
```    12 Stfun  =  Prod +
```
```    13
```
```    14 types
```
```    15     state
```
```    16     'a stfun = "state => 'a"
```
```    17     stpred   = "bool stfun"
```
```    18
```
```    19 arities
```
```    20     state :: term
```
```    21
```
```    22 consts
```
```    23   (* For simplicity, we do not syntactically distinguish between state variables
```
```    24      and state functions, and treat "state" as an anonymous type. But we need a
```
```    25      "meta-predicate" to identify "base" state variables that represent the state
```
```    26      components of a system, in particular to define the enabledness of actions.
```
```    27   *)
```
```    28   base_var  :: "'a stfun => bool"
```
```    29
```
```    30   (* lift tupling to state functions *)
```
```    31   pairSF    :: "['a stfun, 'b stfun] => ('a * 'b) stfun"
```
```    32
```
```    33 syntax
```
```    34   "@tupleSF"     :: "args => ('a * 'b) stfun"  ("(1<_>)")
```
```    35
```
```    36 translations
```
```    37   "<x,y,z>"   == "<x, <y,z> >"
```
```    38   "<x,y>"     == "pairSF x y"
```
```    39   "<x>"       => "x"
```
```    40
```
```    41 rules
```
```    42   (* tupling *)
```
```    43   pairSF_def  "<v,w>(s) = (v(s),w(s))"
```
```    44
```
```    45   (* "base" variables may be assigned arbitrary values by states.
```
```    46      NB: It's really stronger than that because "u" doesn't depend
```
```    47          on either c or v. In particular, if "==>" were replaced
```
```    48          with "==", base_pair would (still) not be derivable.
```
```    49   *)
```
```    50   base_var    "base_var v ==> EX u. v u = c"
```
```    51
```
```    52   (* a tuple of variables is "base" if each variable is "base" *)
```
```    53   base_pair   "base_var <v,w> = (base_var v & base_var w)"
```
```    54 end
```
```    55
```
```    56 ML
```