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