src/HOL/TLA/Stfun.thy
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 6255 db63752140c7
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
     1 (* 
     2     File:	 TLA/Stfun.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: Stfun
     7     Logic Image: HOL
     8 
     9 States and state functions for TLA
    10 *)
    11 
    12 Stfun  =  Prod +
    13 
    14 types
    15     state
    16     'a stfun = "state => 'a"
    17     stpred   = "bool stfun"
    18 
    19 arities
    20     state :: term
    21 
    22 consts
    23   (* For simplicity, we do not syntactically distinguish between state variables
    24      and state functions, and treat "state" as an anonymous type. But we need a 
    25      "meta-predicate" to identify "base" state variables that represent the state
    26      components of a system, in particular to define the enabledness of actions.
    27   *)
    28   base_var  :: "'a stfun => bool"
    29 
    30   (* lift tupling to state functions *)
    31   pairSF    :: "['a stfun, 'b stfun] => ('a * 'b) stfun"
    32 
    33 syntax
    34   "@tupleSF"     :: "args => ('a * 'b) stfun"  ("(1<_>)")
    35 
    36 translations
    37   "<x,y,z>"   == "<x, <y,z> >"
    38   "<x,y>"     == "pairSF x y"
    39   "<x>"       => "x"
    40 
    41 rules
    42   (* tupling *)
    43   pairSF_def  "<v,w>(s) = (v(s),w(s))"
    44 
    45   (* "base" variables may be assigned arbitrary values by states.
    46      NB: It's really stronger than that because "u" doesn't depend 
    47          on either c or v. In particular, if "==>" were replaced
    48          with "==", base_pair would (still) not be derivable.
    49   *)
    50   base_var    "base_var v ==> EX u. v u = c"
    51 
    52   (* a tuple of variables is "base" if each variable is "base" *)
    53   base_pair   "base_var <v,w> = (base_var v & base_var w)"
    54 end
    55 
    56 ML