src/HOL/TLA/Stfun.thy
 author wenzelm Wed Sep 07 20:22:39 2005 +0200 (2005-09-07) changeset 17309 c43ed29bd197 parent 12607 16b63730cfbb child 21624 6f79647cf536 permissions -rw-r--r--
converted to Isar theory format;
```     1 (*
```
```     2     File:        TLA/Stfun.thy
```
```     3     ID:          \$Id\$
```
```     4     Author:      Stephan Merz
```
```     5     Copyright:   1998 University of Munich
```
```     6
```
```     7     Theory Name: Stfun
```
```     8     Logic Image: HOL
```
```     9
```
```    10 States and state functions for TLA as an "intensional" logic.
```
```    11 *)
```
```    12
```
```    13 theory Stfun
```
```    14 imports Intensional
```
```    15 begin
```
```    16
```
```    17 typedecl state
```
```    18
```
```    19 instance state :: world ..
```
```    20
```
```    21 types
```
```    22   'a stfun = "state => 'a"
```
```    23   stpred  = "bool stfun"
```
```    24
```
```    25
```
```    26 consts
```
```    27   (* Formalizing type "state" would require formulas to be tagged with
```
```    28      their underlying state space and would result in a system that is
```
```    29      much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
```
```    30      over state variables, and therefore one usually works with different
```
```    31      state spaces within a single specification.) Instead, "state" is just
```
```    32      an anonymous type whose only purpose is to provide "Skolem" constants.
```
```    33      Moreover, we do not define a type of state variables separate from that
```
```    34      of arbitrary state functions, again in order to simplify the definition
```
```    35      of flexible quantification later on. Nevertheless, we need to distinguish
```
```    36      state variables, mainly to define the enabledness of actions. The user
```
```    37      identifies (tuples of) "base" state variables in a specification via the
```
```    38      "meta predicate" basevars, which is defined here.
```
```    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 defs
```
```    51   (* Base variables may be assigned arbitrary (type-correct) values.
```
```    52      Note that vs may be a tuple of variables. The correct identification
```
```    53      of base variables is up to the user who must take care not to
```
```    54      introduce an inconsistency. For example, "basevars (x,x)" would
```
```    55      definitely be inconsistent.
```
```    56   *)
```
```    57   basevars_def:  "stvars vs == range vs = UNIV"
```
```    58
```
```    59 ML {* use_legacy_bindings (the_context ()) *}
```
```    60
```
```    61 end
```