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
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 TLA/Stfun.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@6255
     4
    Copyright:   1998 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: Stfun
wenzelm@3807
     7
    Logic Image: HOL
wenzelm@3807
     8
wenzelm@6255
     9
States and state functions for TLA as an "intensional" logic.
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@6255
    12
Stfun  =  Intensional +
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@3807
    15
    state
wenzelm@3807
    16
    'a stfun = "state => 'a"
wenzelm@3807
    17
    stpred   = "bool stfun"
wenzelm@3807
    18
wenzelm@3807
    19
arities
wenzelm@12338
    20
  state :: type
wenzelm@6255
    21
wenzelm@6255
    22
instance
wenzelm@6255
    23
  state :: world
wenzelm@3807
    24
wenzelm@3807
    25
consts
wenzelm@6255
    26
  (* Formalizing type "state" would require formulas to be tagged with
wenzelm@6255
    27
     their underlying state space and would result in a system that is
wenzelm@6255
    28
     much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
wenzelm@6255
    29
     over state variables, and therefore one usually works with different
wenzelm@6255
    30
     state spaces within a single specification.) Instead, "state" is just
wenzelm@6255
    31
     an anonymous type whose only purpose is to provide "Skolem" constants.
wenzelm@6255
    32
     Moreover, we do not define a type of state variables separate from that
wenzelm@6255
    33
     of arbitrary state functions, again in order to simplify the definition
wenzelm@6255
    34
     of flexible quantification later on. Nevertheless, we need to distinguish
wenzelm@6255
    35
     state variables, mainly to define the enabledness of actions. The user
wenzelm@6255
    36
     identifies (tuples of) "base" state variables in a specification via the
wenzelm@12607
    37
     "meta predicate" basevars, which is defined here.
wenzelm@3807
    38
  *)
wenzelm@6255
    39
  stvars    :: "'a stfun => bool"
wenzelm@3807
    40
wenzelm@3807
    41
syntax
wenzelm@6255
    42
  "PRED"    :: lift => 'a                          ("PRED _")
wenzelm@6255
    43
  "_stvars" :: lift => bool                        ("basevars _")
wenzelm@3807
    44
wenzelm@3807
    45
translations
wenzelm@6255
    46
  "PRED P"   =>  "(P::state => _)"
wenzelm@6255
    47
  "_stvars"  ==  "stvars"
wenzelm@3807
    48
wenzelm@12607
    49
defs
wenzelm@6255
    50
  (* Base variables may be assigned arbitrary (type-correct) values. 
wenzelm@12607
    51
     Note that vs may be a tuple of variables. The correct identification
wenzelm@12607
    52
     of base variables is up to the user who must take care not to
wenzelm@12607
    53
     introduce an inconsistency. For example, "basevars (x,x)" would
wenzelm@12607
    54
     definitely be inconsistent.
wenzelm@6255
    55
  *)
wenzelm@12607
    56
  basevars_def	"stvars vs == range vs = UNIV"
wenzelm@3807
    57
wenzelm@3807
    58
end