src/HOL/TLA/Stfun.thy
 author wenzelm Thu Mar 11 13:20:35 1999 +0100 (1999-03-11) changeset 6349 f7750d816c21 parent 6255 db63752140c7 child 11703 6e5de8d4290a permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
```     1 (*
```
```     2     File:	 TLA/Stfun.thy
```
```     3     Author:      Stephan Merz
```
```     4     Copyright:   1998 University of Munich
```
```     5
```
```     6     Theory Name: Stfun
```
```     7     Logic Image: HOL
```
```     8
```
```     9 States and state functions for TLA as an "intensional" logic.
```
```    10 *)
```
```    11
```
```    12 Stfun  =  Intensional +
```
```    13
```
```    14 types
```
```    15     state
```
```    16     'a stfun = "state => 'a"
```
```    17     stpred   = "bool stfun"
```
```    18
```
```    19 arities
```
```    20   state :: term
```
```    21
```
```    22 instance
```
```    23   state :: world
```
```    24
```
```    25 consts
```
```    26   (* Formalizing type "state" would require formulas to be tagged with
```
```    27      their underlying state space and would result in a system that is
```
```    28      much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
```
```    29      over state variables, and therefore one usually works with different
```
```    30      state spaces within a single specification.) Instead, "state" is just
```
```    31      an anonymous type whose only purpose is to provide "Skolem" constants.
```
```    32      Moreover, we do not define a type of state variables separate from that
```
```    33      of arbitrary state functions, again in order to simplify the definition
```
```    34      of flexible quantification later on. Nevertheless, we need to distinguish
```
```    35      state variables, mainly to define the enabledness of actions. The user
```
```    36      identifies (tuples of) "base" state variables in a specification via the
```
```    37      "meta predicate" stvars.
```
```    38      NOTE: There should not be duplicates in the tuple!
```
```    39   *)
```
```    40   stvars    :: "'a stfun => bool"
```
```    41
```
```    42 syntax
```
```    43   "PRED"    :: lift => 'a                          ("PRED _")
```
```    44   "_stvars" :: lift => bool                        ("basevars _")
```
```    45
```
```    46 translations
```
```    47   "PRED P"   =>  "(P::state => _)"
```
```    48   "_stvars"  ==  "stvars"
```
```    49
```
```    50 rules
```
```    51   (* Base variables may be assigned arbitrary (type-correct) values.
```
```    52      Note that vs may be a tuple of variables. The rule would be unsound
```
```    53      if vs contained duplicates.
```
```    54   *)
```
```    55   basevars  "basevars vs ==> EX u. vs u = c"
```
```    56   base_pair "basevars (x,y) ==> basevars x & basevars y"
```
```    57   (* Since the unit type has just one value, any state function can be
```
```    58      regarded as "base". The following axiom can sometimes be useful
```
```    59      because it gives a trivial solution for "basevars" premises.
```
```    60   *)
```
```    61   unit_base "basevars (v::unit stfun)"
```
```    62
```
```    63 end
```
```    64
```
```    65 ML
```