src/HOL/TLA/Stfun.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 12607 16b63730cfbb child 17309 c43ed29bd197 permissions -rw-r--r--
import -> imports
```     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 :: type
```
```    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" basevars, which is defined here.
```
```    38   *)
```
```    39   stvars    :: "'a stfun => bool"
```
```    40
```
```    41 syntax
```
```    42   "PRED"    :: lift => 'a                          ("PRED _")
```
```    43   "_stvars" :: lift => bool                        ("basevars _")
```
```    44
```
```    45 translations
```
```    46   "PRED P"   =>  "(P::state => _)"
```
```    47   "_stvars"  ==  "stvars"
```
```    48
```
```    49 defs
```
```    50   (* Base variables may be assigned arbitrary (type-correct) values.
```
```    51      Note that vs may be a tuple of variables. The correct identification
```
```    52      of base variables is up to the user who must take care not to
```
```    53      introduce an inconsistency. For example, "basevars (x,x)" would
```
```    54      definitely be inconsistent.
```
```    55   *)
```
```    56   basevars_def	"stvars vs == range vs = UNIV"
```
```    57
```
```    58 end
```