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
```