author | haftmann |
Tue, 23 Feb 2010 10:11:16 +0100 | |
changeset 35318 | e1b61c5fd494 |
parent 35108 | e384e27c229f |
child 42018 | 878f33040280 |
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 |
|
35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset
|
15 |
arities behavior :: world |
6255 | 16 |
|
17 |
types |
|
17309 | 18 |
temporal = "behavior form" |
6255 | 19 |
|
20 |
||
21 |
consts |
|
17309 | 22 |
Initial :: "('w::world => bool) => temporal" |
23 |
first_world :: "behavior => ('w::world)" |
|
24 |
st1 :: "behavior => state" |
|
25 |
st2 :: "behavior => state" |
|
6255 | 26 |
|
27 |
syntax |
|
35108 | 28 |
"_TEMP" :: "lift => 'a" ("(TEMP _)") |
17309 | 29 |
"_Init" :: "lift => lift" ("(Init _)"[40] 50) |
6255 | 30 |
|
31 |
translations |
|
32 |
"TEMP F" => "(F::behavior => _)" |
|
35108 | 33 |
"_Init" == "CONST Initial" |
6255 | 34 |
"sigma |= Init F" <= "_Init F sigma" |
35 |
||
36 |
defs |
|
17309 | 37 |
Init_def: "sigma |= Init F == (first_world sigma) |= F" |
38 |
fw_temp_def: "first_world == %sigma. sigma" |
|
39 |
fw_stp_def: "first_world == st1" |
|
40 |
fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)" |
|
41 |
||
21624 | 42 |
lemma const_simps [int_rewrite, simp]: |
43 |
"|- (Init #True) = #True" |
|
44 |
"|- (Init #False) = #False" |
|
45 |
by (auto simp: Init_def) |
|
46 |
||
26304 | 47 |
lemma Init_simps1 [int_rewrite]: |
21624 | 48 |
"!!F. |- (Init ~F) = (~ Init F)" |
49 |
"|- (Init (P --> Q)) = (Init P --> Init Q)" |
|
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 (!x. F x)) = (!x. (Init F x))" |
|
54 |
"|- (Init (? x. F x)) = (? x. (Init F x))" |
|
55 |
"|- (Init (?! x. F x)) = (?! x. (Init F x))" |
|
56 |
by (auto simp: Init_def) |
|
57 |
||
58 |
lemma Init_stp_act: "|- (Init $P) = (Init P)" |
|
59 |
by (auto simp add: Init_def fw_act_def fw_stp_def) |
|
60 |
||
26304 | 61 |
lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1 |
21624 | 62 |
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric] |
63 |
||
64 |
lemma Init_temp: "|- (Init F) = F" |
|
65 |
by (auto simp add: Init_def fw_temp_def) |
|
66 |
||
26304 | 67 |
lemmas Init_simps = Init_temp [int_rewrite] Init_simps2 |
21624 | 68 |
|
69 |
(* Trivial instances of the definitions that avoid introducing lambda expressions. *) |
|
70 |
lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)" |
|
71 |
by (simp add: Init_def fw_stp_def) |
|
72 |
||
73 |
lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)" |
|
74 |
by (simp add: Init_def fw_act_def) |
|
75 |
||
76 |
lemmas Init_defs = Init_stp Init_act Init_temp [int_use] |
|
17309 | 77 |
|
6255 | 78 |
end |