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