author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11703 | 6e5de8d4290a |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
6255 | 1 |
(* |
2 |
File: TLA/Init.thy |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1998 University of Munich |
|
5 |
||
6 |
Theory Name: Init |
|
7 |
Logic Image: HOL |
|
8 |
||
9 |
Introduces type of temporal formulas. Defines interface between |
|
10 |
temporal formulas and its "subformulas" (state predicates and actions). |
|
11 |
*) |
|
12 |
||
13 |
Init = Action + |
|
14 |
||
15 |
types |
|
16 |
behavior |
|
17 |
temporal = behavior form |
|
18 |
||
19 |
arities |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11703
diff
changeset
|
20 |
behavior :: type |
6255 | 21 |
|
22 |
instance |
|
23 |
behavior :: world |
|
24 |
||
25 |
consts |
|
26 |
Initial :: ('w::world => bool) => temporal |
|
27 |
first_world :: behavior => ('w::world) |
|
28 |
st1, st2 :: behavior => state |
|
29 |
||
30 |
syntax |
|
31 |
TEMP :: lift => 'a ("(TEMP _)") |
|
32 |
"_Init" :: lift => lift ("(Init _)"[40] 50) |
|
33 |
||
34 |
translations |
|
35 |
"TEMP F" => "(F::behavior => _)" |
|
36 |
"_Init" == "Initial" |
|
37 |
"sigma |= Init F" <= "_Init F sigma" |
|
38 |
||
39 |
defs |
|
40 |
Init_def "sigma |= Init F == (first_world sigma) |= F" |
|
41 |
fw_temp_def "first_world == %sigma. sigma" |
|
42 |
fw_stp_def "first_world == st1" |
|
43 |
fw_act_def "first_world == %sigma. (st1 sigma, st2 sigma)" |
|
44 |
end |