src/HOL/TLA/Stfun.thy
changeset 6255 db63752140c7
parent 3807 82a99b090d9d
child 11703 6e5de8d4290a
     1.1 --- a/src/HOL/TLA/Stfun.thy	Mon Feb 08 13:02:42 1999 +0100
     1.2 +++ b/src/HOL/TLA/Stfun.thy	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -1,15 +1,15 @@
     1.4  (* 
     1.5      File:	 TLA/Stfun.thy
     1.6      Author:      Stephan Merz
     1.7 -    Copyright:   1997 University of Munich
     1.8 +    Copyright:   1998 University of Munich
     1.9  
    1.10      Theory Name: Stfun
    1.11      Logic Image: HOL
    1.12  
    1.13 -States and state functions for TLA
    1.14 +States and state functions for TLA as an "intensional" logic.
    1.15  *)
    1.16  
    1.17 -Stfun  =  Prod +
    1.18 +Stfun  =  Intensional +
    1.19  
    1.20  types
    1.21      state
    1.22 @@ -17,40 +17,49 @@
    1.23      stpred   = "bool stfun"
    1.24  
    1.25  arities
    1.26 -    state :: term
    1.27 +  state :: term
    1.28 +
    1.29 +instance
    1.30 +  state :: world
    1.31  
    1.32  consts
    1.33 -  (* For simplicity, we do not syntactically distinguish between state variables
    1.34 -     and state functions, and treat "state" as an anonymous type. But we need a 
    1.35 -     "meta-predicate" to identify "base" state variables that represent the state
    1.36 -     components of a system, in particular to define the enabledness of actions.
    1.37 +  (* Formalizing type "state" would require formulas to be tagged with
    1.38 +     their underlying state space and would result in a system that is
    1.39 +     much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
    1.40 +     over state variables, and therefore one usually works with different
    1.41 +     state spaces within a single specification.) Instead, "state" is just
    1.42 +     an anonymous type whose only purpose is to provide "Skolem" constants.
    1.43 +     Moreover, we do not define a type of state variables separate from that
    1.44 +     of arbitrary state functions, again in order to simplify the definition
    1.45 +     of flexible quantification later on. Nevertheless, we need to distinguish
    1.46 +     state variables, mainly to define the enabledness of actions. The user
    1.47 +     identifies (tuples of) "base" state variables in a specification via the
    1.48 +     "meta predicate" stvars.
    1.49 +     NOTE: There should not be duplicates in the tuple!
    1.50    *)
    1.51 -  base_var  :: "'a stfun => bool"
    1.52 -
    1.53 -  (* lift tupling to state functions *)
    1.54 -  pairSF    :: "['a stfun, 'b stfun] => ('a * 'b) stfun"
    1.55 +  stvars    :: "'a stfun => bool"
    1.56  
    1.57  syntax
    1.58 -  "@tupleSF"     :: "args => ('a * 'b) stfun"  ("(1<_>)")
    1.59 +  "PRED"    :: lift => 'a                          ("PRED _")
    1.60 +  "_stvars" :: lift => bool                        ("basevars _")
    1.61  
    1.62  translations
    1.63 -  "<x,y,z>"   == "<x, <y,z> >"
    1.64 -  "<x,y>"     == "pairSF x y"
    1.65 -  "<x>"       => "x"
    1.66 +  "PRED P"   =>  "(P::state => _)"
    1.67 +  "_stvars"  ==  "stvars"
    1.68  
    1.69  rules
    1.70 -  (* tupling *)
    1.71 -  pairSF_def  "<v,w>(s) = (v(s),w(s))"
    1.72 +  (* Base variables may be assigned arbitrary (type-correct) values. 
    1.73 +     Note that vs may be a tuple of variables. The rule would be unsound 
    1.74 +     if vs contained duplicates.
    1.75 +  *)
    1.76 +  basevars  "basevars vs ==> EX u. vs u = c"
    1.77 +  base_pair "basevars (x,y) ==> basevars x & basevars y"
    1.78 +  (* Since the unit type has just one value, any state function can be
    1.79 +     regarded as "base". The following axiom can sometimes be useful
    1.80 +     because it gives a trivial solution for "basevars" premises.
    1.81 +  *)
    1.82 +  unit_base "basevars (v::unit stfun)"
    1.83  
    1.84 -  (* "base" variables may be assigned arbitrary values by states.
    1.85 -     NB: It's really stronger than that because "u" doesn't depend 
    1.86 -         on either c or v. In particular, if "==>" were replaced
    1.87 -         with "==", base_pair would (still) not be derivable.
    1.88 -  *)
    1.89 -  base_var    "base_var v ==> EX u. v u = c"
    1.90 -
    1.91 -  (* a tuple of variables is "base" if each variable is "base" *)
    1.92 -  base_pair   "base_var <v,w> = (base_var v & base_var w)"
    1.93  end
    1.94  
    1.95  ML