|
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
|
|
|
20 |
behavior :: term
|
|
|
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
|
|
|
45 |
|
|
|
46 |
ML
|