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;
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@6255
    20
  state :: term
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@6255
    37
     "meta predicate" stvars.
wenzelm@6255
    38
     NOTE: There should not be duplicates in the tuple!
wenzelm@3807
    39
  *)
wenzelm@6255
    40
  stvars    :: "'a stfun => bool"
wenzelm@3807
    41
wenzelm@3807
    42
syntax
wenzelm@6255
    43
  "PRED"    :: lift => 'a                          ("PRED _")
wenzelm@6255
    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@3807
    50
rules
wenzelm@6255
    51
  (* Base variables may be assigned arbitrary (type-correct) values. 
wenzelm@6255
    52
     Note that vs may be a tuple of variables. The rule would be unsound 
wenzelm@6255
    53
     if vs contained duplicates.
wenzelm@6255
    54
  *)
wenzelm@6255
    55
  basevars  "basevars vs ==> EX u. vs u = c"
wenzelm@6255
    56
  base_pair "basevars (x,y) ==> basevars x & basevars y"
wenzelm@6255
    57
  (* Since the unit type has just one value, any state function can be
wenzelm@6255
    58
     regarded as "base". The following axiom can sometimes be useful
wenzelm@6255
    59
     because it gives a trivial solution for "basevars" premises.
wenzelm@6255
    60
  *)
wenzelm@6255
    61
  unit_base "basevars (v::unit stfun)"
wenzelm@3807
    62
wenzelm@3807
    63
end