author | wenzelm |
Thu, 22 Nov 2007 14:51:34 +0100 | |
changeset 25456 | 6f79698f294d |
parent 19741 | f65265d71426 |
child 26339 | 7825c83c9eff |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/TLS.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
4559 | 5 |
|
17233 | 6 |
header {* Temporal Logic of Steps -- tailored for I/O automata *} |
4559 | 7 |
|
17233 | 8 |
theory TLS |
9 |
imports IOA TL |
|
10 |
begin |
|
4559 | 11 |
|
17233 | 12 |
defaultsort type |
4559 | 13 |
|
14 |
types |
|
17233 | 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" |
|
4559 | 18 |
|
19 |
consts |
|
20 |
||
21 |
option_lift :: "('a => 'b) => 'b => ('a option => 'b)" |
|
22 |
plift :: "('a => bool) => ('a option => bool)" |
|
17233 | 23 |
|
4559 | 24 |
temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "|==" 22) |
25 |
xt1 :: "'s predicate => ('a,'s)step_pred" |
|
26 |
xt2 :: "'a option predicate => ('a,'s)step_pred" |
|
27 |
||
28 |
validTE :: "('a,'s)ioa_temp => bool" |
|
29 |
validIOA :: "('a,'s)ioa => ('a,'s)ioa_temp => bool" |
|
30 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
31 |
mkfin :: "'a Seq => 'a Seq" |
4559 | 32 |
|
33 |
ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq" |
|
17233 | 34 |
ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)" |
4559 | 35 |
|
36 |
||
37 |
defs |
|
38 |
||
17233 | 39 |
mkfin_def: |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
40 |
"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
|
41 |
else s" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
42 |
|
17233 | 43 |
option_lift_def: |
4559 | 44 |
"option_lift f s y == case y of None => s | Some x => (f x)" |
45 |
||
17233 | 46 |
(* plift is used to determine that None action is always false in |
4559 | 47 |
transition predicates *) |
17233 | 48 |
plift_def: |
4559 | 49 |
"plift P == option_lift P False" |
50 |
||
17233 | 51 |
temp_sat_def: |
4559 | 52 |
"ex |== P == ((ex2seq ex) |= P)" |
53 |
||
17233 | 54 |
xt1_def: |
4559 | 55 |
"xt1 P tr == P (fst tr)" |
56 |
||
17233 | 57 |
xt2_def: |
4559 | 58 |
"xt2 P tr == P (fst (snd tr))" |
59 |
||
17233 | 60 |
ex2seq_def: |
10835 | 61 |
"ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))" |
4559 | 62 |
|
17233 | 63 |
ex2seqC_def: |
64 |
"ex2seqC == (fix$(LAM h ex. (%s. case ex of |
|
4559 | 65 |
nil => (s,None,s)>>nil |
66 |
| x##xs => (flift1 (%pr. |
|
17233 | 67 |
(s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) |
10835 | 68 |
$x) |
4559 | 69 |
)))" |
70 |
||
17233 | 71 |
validTE_def: |
4559 | 72 |
"validTE P == ! ex. (ex |== P)" |
73 |
||
17233 | 74 |
validIOA_def: |
4559 | 75 |
"validIOA A P == ! ex : executions A . (ex |== P)" |
76 |
||
5976 | 77 |
|
17233 | 78 |
axioms |
5976 | 79 |
|
17233 | 80 |
mkfin_UU: |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
81 |
"mkfin UU = nil" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
82 |
|
17233 | 83 |
mkfin_nil: |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
84 |
"mkfin nil =nil" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
85 |
|
17233 | 86 |
mkfin_cons: |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
87 |
"(mkfin (a>>s)) = (a>>(mkfin s))" |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
4577
diff
changeset
|
88 |
|
19741 | 89 |
|
90 |
lemmas [simp del] = ex_simps all_simps split_paired_Ex |
|
91 |
declare Let_def [simp] |
|
92 |
||
93 |
ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *} |
|
94 |
||
95 |
||
96 |
subsection {* ex2seqC *} |
|
97 |
||
98 |
lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of |
|
99 |
nil => (s,None,s)>>nil |
|
100 |
| x##xs => (flift1 (%pr. |
|
101 |
(s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr)) |
|
102 |
$x) |
|
103 |
))" |
|
104 |
apply (rule trans) |
|
105 |
apply (rule fix_eq2) |
|
106 |
apply (rule ex2seqC_def) |
|
107 |
apply (rule beta_cfun) |
|
108 |
apply (simp add: flift1_def) |
|
109 |
done |
|
110 |
||
111 |
lemma ex2seqC_UU: "(ex2seqC $UU) s=UU" |
|
112 |
apply (subst ex2seqC_unfold) |
|
113 |
apply simp |
|
114 |
done |
|
115 |
||
116 |
lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)>>nil" |
|
117 |
apply (subst ex2seqC_unfold) |
|
118 |
apply simp |
|
119 |
done |
|
120 |
||
121 |
lemma ex2seqC_cons: "(ex2seqC $((a,t)>>xs)) s = |
|
122 |
(s,Some a,t)>> ((ex2seqC$xs) t)" |
|
123 |
apply (rule trans) |
|
124 |
apply (subst ex2seqC_unfold) |
|
125 |
apply (simp add: Consq_def flift1_def) |
|
126 |
apply (simp add: Consq_def flift1_def) |
|
127 |
done |
|
128 |
||
129 |
declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp] |
|
130 |
||
131 |
||
132 |
||
133 |
declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp] |
|
134 |
||
135 |
lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)>>nil" |
|
136 |
apply (simp add: ex2seq_def) |
|
137 |
done |
|
138 |
||
139 |
lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)>>nil" |
|
140 |
apply (simp add: ex2seq_def) |
|
141 |
done |
|
142 |
||
143 |
lemma ex2seq_cons: "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)" |
|
144 |
apply (simp add: ex2seq_def) |
|
145 |
done |
|
146 |
||
147 |
declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del] |
|
148 |
declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp] |
|
149 |
||
150 |
||
151 |
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil" |
|
152 |
apply (tactic {* pair_tac "exec" 1 *}) |
|
153 |
apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
154 |
apply (tactic {* pair_tac "a" 1 *}) |
|
155 |
done |
|
156 |
||
157 |
||
158 |
subsection {* Interface TL -- TLS *} |
|
159 |
||
160 |
(* uses the fact that in executions states overlap, which is lost in |
|
161 |
after the translation via ex2seq !! *) |
|
162 |
||
163 |
lemma TL_TLS: |
|
164 |
"[| ! s a t. (P s) & s-a--A-> t --> (Q t) |] |
|
165 |
==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) |
|
166 |
.--> (Next (Init (%(s,a,t).Q s))))" |
|
167 |
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def) |
|
168 |
||
169 |
apply (tactic "clarify_tac set_cs 1") |
|
170 |
apply (simp split add: split_if) |
|
171 |
(* TL = UU *) |
|
172 |
apply (rule conjI) |
|
173 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
174 |
apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
175 |
apply (tactic {* pair_tac "a" 1 *}) |
|
176 |
apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
177 |
apply (tactic {* pair_tac "a" 1 *}) |
|
178 |
(* TL = nil *) |
|
179 |
apply (rule conjI) |
|
180 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
181 |
apply (tactic {* Seq_case_tac "y" 1 *}) |
|
182 |
apply (simp add: unlift_def) |
|
183 |
apply fast |
|
184 |
apply (simp add: unlift_def) |
|
185 |
apply fast |
|
186 |
apply (simp add: unlift_def) |
|
187 |
apply (tactic {* pair_tac "a" 1 *}) |
|
188 |
apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
189 |
apply (tactic {* pair_tac "a" 1 *}) |
|
190 |
(* TL =cons *) |
|
191 |
apply (simp add: unlift_def) |
|
192 |
||
193 |
apply (tactic {* pair_tac "ex" 1 *}) |
|
194 |
apply (tactic {* Seq_case_simp_tac "y" 1 *}) |
|
195 |
apply (tactic {* pair_tac "a" 1 *}) |
|
196 |
apply (tactic {* Seq_case_simp_tac "s" 1 *}) |
|
197 |
apply blast |
|
198 |
apply fastsimp |
|
199 |
apply (tactic {* pair_tac "a" 1 *}) |
|
200 |
apply fastsimp |
|
201 |
done |
|
4559 | 202 |
|
203 |
end |