src/HOL/TLA/Stfun.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 6255 db63752140c7
child 12338 de0f4a63baa5
permissions -rw-r--r--
tuned;
     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