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