author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 57510 | 8f1dc3b2daa5 |
child 60587 | 0318b43ee95c |
permissions | -rw-r--r-- |
35108 | 1 |
(* Title: HOL/TLA/Init.thy |
2 |
Author: Stephan Merz |
|
3 |
Copyright: 1998 University of Munich |
|
6255 | 4 |
|
35108 | 5 |
Introduces type of temporal formulas. Defines interface between |
6 |
temporal formulas and its "subformulas" (state predicates and |
|
7 |
actions). |
|
6255 | 8 |
*) |
9 |
||
17309 | 10 |
theory Init |
11 |
imports Action |
|
12 |
begin |
|
13 |
||
14 |
typedecl behavior |
|
55382
9218fa411c15
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
42018
diff
changeset
|
15 |
instance behavior :: world .. |
6255 | 16 |
|
42018 | 17 |
type_synonym temporal = "behavior form" |
6255 | 18 |
|
19 |
||
20 |
consts |
|
17309 | 21 |
Initial :: "('w::world => bool) => temporal" |
22 |
first_world :: "behavior => ('w::world)" |
|
23 |
st1 :: "behavior => state" |
|
24 |
st2 :: "behavior => state" |
|
6255 | 25 |
|
26 |
syntax |
|
35108 | 27 |
"_TEMP" :: "lift => 'a" ("(TEMP _)") |
17309 | 28 |
"_Init" :: "lift => lift" ("(Init _)"[40] 50) |
6255 | 29 |
|
30 |
translations |
|
31 |
"TEMP F" => "(F::behavior => _)" |
|
35108 | 32 |
"_Init" == "CONST Initial" |
6255 | 33 |
"sigma |= Init F" <= "_Init F sigma" |
34 |
||
35 |
defs |
|
17309 | 36 |
Init_def: "sigma |= Init F == (first_world sigma) |= F" |
57510 | 37 |
|
38 |
defs (overloaded) |
|
17309 | 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 |