17309
|
1 |
(*
|
|
2 |
File: TLA/Init.thy
|
|
3 |
ID: $Id$
|
6255
|
4 |
Author: Stephan Merz
|
|
5 |
Copyright: 1998 University of Munich
|
|
6 |
|
|
7 |
Introduces type of temporal formulas. Defines interface between
|
|
8 |
temporal formulas and its "subformulas" (state predicates and actions).
|
|
9 |
*)
|
|
10 |
|
17309
|
11 |
theory Init
|
|
12 |
imports Action
|
|
13 |
begin
|
|
14 |
|
|
15 |
typedecl behavior
|
|
16 |
instance behavior :: world ..
|
6255
|
17 |
|
|
18 |
types
|
17309
|
19 |
temporal = "behavior form"
|
6255
|
20 |
|
|
21 |
|
|
22 |
consts
|
17309
|
23 |
Initial :: "('w::world => bool) => temporal"
|
|
24 |
first_world :: "behavior => ('w::world)"
|
|
25 |
st1 :: "behavior => state"
|
|
26 |
st2 :: "behavior => state"
|
6255
|
27 |
|
|
28 |
syntax
|
17309
|
29 |
TEMP :: "lift => 'a" ("(TEMP _)")
|
|
30 |
"_Init" :: "lift => lift" ("(Init _)"[40] 50)
|
6255
|
31 |
|
|
32 |
translations
|
|
33 |
"TEMP F" => "(F::behavior => _)"
|
|
34 |
"_Init" == "Initial"
|
|
35 |
"sigma |= Init F" <= "_Init F sigma"
|
|
36 |
|
|
37 |
defs
|
17309
|
38 |
Init_def: "sigma |= Init F == (first_world sigma) |= F"
|
|
39 |
fw_temp_def: "first_world == %sigma. sigma"
|
|
40 |
fw_stp_def: "first_world == st1"
|
|
41 |
fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)"
|
|
42 |
|
21624
|
43 |
lemma const_simps [int_rewrite, simp]:
|
|
44 |
"|- (Init #True) = #True"
|
|
45 |
"|- (Init #False) = #False"
|
|
46 |
by (auto simp: Init_def)
|
|
47 |
|
26304
|
48 |
lemma Init_simps1 [int_rewrite]:
|
21624
|
49 |
"!!F. |- (Init ~F) = (~ Init F)"
|
|
50 |
"|- (Init (P --> Q)) = (Init P --> Init Q)"
|
|
51 |
"|- (Init (P & Q)) = (Init P & Init Q)"
|
|
52 |
"|- (Init (P | Q)) = (Init P | Init Q)"
|
|
53 |
"|- (Init (P = Q)) = ((Init P) = (Init Q))"
|
|
54 |
"|- (Init (!x. F x)) = (!x. (Init F x))"
|
|
55 |
"|- (Init (? x. F x)) = (? x. (Init F x))"
|
|
56 |
"|- (Init (?! x. F x)) = (?! x. (Init F x))"
|
|
57 |
by (auto simp: Init_def)
|
|
58 |
|
|
59 |
lemma Init_stp_act: "|- (Init $P) = (Init P)"
|
|
60 |
by (auto simp add: Init_def fw_act_def fw_stp_def)
|
|
61 |
|
26304
|
62 |
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
|
21624
|
63 |
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
|
|
64 |
|
|
65 |
lemma Init_temp: "|- (Init F) = F"
|
|
66 |
by (auto simp add: Init_def fw_temp_def)
|
|
67 |
|
26304
|
68 |
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
|
21624
|
69 |
|
|
70 |
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
|
|
71 |
lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
|
|
72 |
by (simp add: Init_def fw_stp_def)
|
|
73 |
|
|
74 |
lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
|
|
75 |
by (simp add: Init_def fw_act_def)
|
|
76 |
|
|
77 |
lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
|
17309
|
78 |
|
6255
|
79 |
end
|