summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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