wenzelm@3807: (*
wenzelm@3807: File: TLA/Stfun.thy
wenzelm@3807: Author: Stephan Merz
wenzelm@6255: Copyright: 1998 University of Munich
wenzelm@3807:
wenzelm@3807: Theory Name: Stfun
wenzelm@3807: Logic Image: HOL
wenzelm@3807:
wenzelm@6255: States and state functions for TLA as an "intensional" logic.
wenzelm@3807: *)
wenzelm@3807:
wenzelm@6255: Stfun = Intensional +
wenzelm@3807:
wenzelm@3807: types
wenzelm@3807: state
wenzelm@3807: 'a stfun = "state => 'a"
wenzelm@3807: stpred = "bool stfun"
wenzelm@3807:
wenzelm@3807: arities
wenzelm@12338: state :: type
wenzelm@6255:
wenzelm@6255: instance
wenzelm@6255: state :: world
wenzelm@3807:
wenzelm@3807: consts
wenzelm@6255: (* Formalizing type "state" would require formulas to be tagged with
wenzelm@6255: their underlying state space and would result in a system that is
wenzelm@6255: much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
wenzelm@6255: over state variables, and therefore one usually works with different
wenzelm@6255: state spaces within a single specification.) Instead, "state" is just
wenzelm@6255: an anonymous type whose only purpose is to provide "Skolem" constants.
wenzelm@6255: Moreover, we do not define a type of state variables separate from that
wenzelm@6255: of arbitrary state functions, again in order to simplify the definition
wenzelm@6255: of flexible quantification later on. Nevertheless, we need to distinguish
wenzelm@6255: state variables, mainly to define the enabledness of actions. The user
wenzelm@6255: identifies (tuples of) "base" state variables in a specification via the
wenzelm@12607: "meta predicate" basevars, which is defined here.
wenzelm@3807: *)
wenzelm@6255: stvars :: "'a stfun => bool"
wenzelm@3807:
wenzelm@3807: syntax
wenzelm@6255: "PRED" :: lift => 'a ("PRED _")
wenzelm@6255: "_stvars" :: lift => bool ("basevars _")
wenzelm@3807:
wenzelm@3807: translations
wenzelm@6255: "PRED P" => "(P::state => _)"
wenzelm@6255: "_stvars" == "stvars"
wenzelm@3807:
wenzelm@12607: defs
wenzelm@6255: (* Base variables may be assigned arbitrary (type-correct) values.
wenzelm@12607: Note that vs may be a tuple of variables. The correct identification
wenzelm@12607: of base variables is up to the user who must take care not to
wenzelm@12607: introduce an inconsistency. For example, "basevars (x,x)" would
wenzelm@12607: definitely be inconsistent.
wenzelm@6255: *)
wenzelm@12607: basevars_def "stvars vs == range vs = UNIV"
wenzelm@3807:
wenzelm@3807: end