author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12338 | de0f4a63baa5 |
child 17233 | 41eee2e7b465 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/TLS.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4559 | 4 |
|
12218 | 5 |
Temporal Logic of Steps -- tailored for I/O automata. |
4559 | 6 |
*) |
7 |
||
8 |
||
9 |
TLS = IOA + TL + |
|
10 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
4559 | 12 |
|
13 |
types |
|
14 |
||
15 |
('a,'s)ioa_temp = "('a option,'s)transition temporal" |
|
16 |
('a,'s)step_pred = "('a option,'s)transition predicate" |
|
17 |
's state_pred = "'s predicate" |
|
18 |
||
19 |
consts |
|
20 |
||
21 |
||
22 |
option_lift :: "('a => 'b) => 'b => ('a option => 'b)" |
|
23 |
plift :: "('a => bool) => ('a option => bool)" |
|
24 |
||
25 |
temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "|==" 22) |
|
26 |
xt1 :: "'s predicate => ('a,'s)step_pred" |
|
27 |
xt2 :: "'a option predicate => ('a,'s)step_pred" |
|
28 |
||
29 |
validTE :: "('a,'s)ioa_temp => bool" |
|
30 |
validIOA :: "('a,'s)ioa => ('a,'s)ioa_temp => bool" |
|
31 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
32 |
mkfin :: "'a Seq => 'a Seq" |
4559 | 33 |
|
34 |
ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq" |
|
35 |
ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" |
|
36 |
||
37 |
||
38 |
defs |
|
39 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
40 |
mkfin_def |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
41 |
"mkfin s == if Partial s then @t. Finite t & s = t @@ UU |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
42 |
else s" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
43 |
|
4559 | 44 |
option_lift_def |
45 |
"option_lift f s y == case y of None => s | Some x => (f x)" |
|
46 |
||
47 |
(* plift is used to determine that None action is always false in |
|
48 |
transition predicates *) |
|
49 |
plift_def |
|
50 |
"plift P == option_lift P False" |
|
51 |
||
52 |
temp_sat_def |
|
53 |
"ex |== P == ((ex2seq ex) |= P)" |
|
54 |
||
55 |
xt1_def |
|
56 |
"xt1 P tr == P (fst tr)" |
|
57 |
||
58 |
xt2_def |
|
59 |
"xt2 P tr == P (fst (snd tr))" |
|
60 |
||
61 |
ex2seq_def |
|
10835 | 62 |
"ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))" |
4559 | 63 |
|
64 |
ex2seqC_def |
|
10835 | 65 |
"ex2seqC == (fix$(LAM h ex. (%s. case ex of |
4559 | 66 |
nil => (s,None,s)>>nil |
67 |
| x##xs => (flift1 (%pr. |
|
10835 | 68 |
(s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) |
69 |
$x) |
|
4559 | 70 |
)))" |
71 |
||
72 |
validTE_def |
|
73 |
"validTE P == ! ex. (ex |== P)" |
|
74 |
||
75 |
validIOA_def |
|
76 |
"validIOA A P == ! ex : executions A . (ex |== P)" |
|
77 |
||
5976 | 78 |
|
79 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
80 |
rules |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
81 |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
82 |
mkfin_UU |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
83 |
"mkfin UU = nil" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
84 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
85 |
mkfin_nil |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
86 |
"mkfin nil =nil" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
87 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
88 |
mkfin_cons |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
89 |
"(mkfin (a>>s)) = (a>>(mkfin s))" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
90 |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
91 |
|
4559 | 92 |
|
93 |
end |
|
94 |