author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11703 | 6e5de8d4290a |
child 12607 | 16b63730cfbb |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: TLA/Stfun.thy |
|
3 |
Author: Stephan Merz |
|
6255 | 4 |
Copyright: 1998 University of Munich |
3807 | 5 |
|
6 |
Theory Name: Stfun |
|
7 |
Logic Image: HOL |
|
8 |
||
6255 | 9 |
States and state functions for TLA as an "intensional" logic. |
3807 | 10 |
*) |
11 |
||
6255 | 12 |
Stfun = Intensional + |
3807 | 13 |
|
14 |
types |
|
15 |
state |
|
16 |
'a stfun = "state => 'a" |
|
17 |
stpred = "bool stfun" |
|
18 |
||
19 |
arities |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11703
diff
changeset
|
20 |
state :: type |
6255 | 21 |
|
22 |
instance |
|
23 |
state :: world |
|
3807 | 24 |
|
25 |
consts |
|
6255 | 26 |
(* Formalizing type "state" would require formulas to be tagged with |
27 |
their underlying state space and would result in a system that is |
|
28 |
much harder to use. (Unlike Hoare logic or Unity, TLA has quantification |
|
29 |
over state variables, and therefore one usually works with different |
|
30 |
state spaces within a single specification.) Instead, "state" is just |
|
31 |
an anonymous type whose only purpose is to provide "Skolem" constants. |
|
32 |
Moreover, we do not define a type of state variables separate from that |
|
33 |
of arbitrary state functions, again in order to simplify the definition |
|
34 |
of flexible quantification later on. Nevertheless, we need to distinguish |
|
35 |
state variables, mainly to define the enabledness of actions. The user |
|
36 |
identifies (tuples of) "base" state variables in a specification via the |
|
37 |
"meta predicate" stvars. |
|
38 |
NOTE: There should not be duplicates in the tuple! |
|
3807 | 39 |
*) |
6255 | 40 |
stvars :: "'a stfun => bool" |
3807 | 41 |
|
42 |
syntax |
|
6255 | 43 |
"PRED" :: lift => 'a ("PRED _") |
44 |
"_stvars" :: lift => bool ("basevars _") |
|
3807 | 45 |
|
46 |
translations |
|
6255 | 47 |
"PRED P" => "(P::state => _)" |
48 |
"_stvars" == "stvars" |
|
3807 | 49 |
|
50 |
rules |
|
6255 | 51 |
(* Base variables may be assigned arbitrary (type-correct) values. |
52 |
Note that vs may be a tuple of variables. The rule would be unsound |
|
53 |
if vs contained duplicates. |
|
54 |
*) |
|
55 |
basevars "basevars vs ==> EX u. vs u = c" |
|
56 |
base_pair "basevars (x,y) ==> basevars x & basevars y" |
|
57 |
(* Since the unit type has just one value, any state function can be |
|
58 |
regarded as "base". The following axiom can sometimes be useful |
|
59 |
because it gives a trivial solution for "basevars" premises. |
|
60 |
*) |
|
61 |
unit_base "basevars (v::unit stfun)" |
|
3807 | 62 |
|
63 |
end |