author | wenzelm |
Fri, 02 Sep 2005 17:23:59 +0200 | |
changeset 17233 | 41eee2e7b465 |
parent 14981 | e73f8140af78 |
child 17955 | 3b34516662c6 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
3071 | 5 |
|
17233 | 6 |
Delsimps (ex_simps @ all_simps); |
3071 | 7 |
Delsimps [split_paired_All]; |
8 |
||
9 |
(* ----------------------------------------------------------------------------------- *) |
|
10 |
||
11 |
||
12 |
section "recursive equations of operators"; |
|
13 |
||
14 |
||
15 |
(* ---------------------------------------------------------------- *) |
|
16 |
(* ProjA2 *) |
|
17 |
(* ---------------------------------------------------------------- *) |
|
18 |
||
19 |
||
10835 | 20 |
Goal "ProjA2$UU = UU"; |
4098 | 21 |
by (simp_tac (simpset() addsimps [ProjA2_def]) 1); |
3071 | 22 |
qed"ProjA2_UU"; |
23 |
||
10835 | 24 |
Goal "ProjA2$nil = nil"; |
4098 | 25 |
by (simp_tac (simpset() addsimps [ProjA2_def]) 1); |
3071 | 26 |
qed"ProjA2_nil"; |
27 |
||
10835 | 28 |
Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs"; |
4098 | 29 |
by (simp_tac (simpset() addsimps [ProjA2_def]) 1); |
3071 | 30 |
qed"ProjA2_cons"; |
31 |
||
32 |
||
33 |
(* ---------------------------------------------------------------- *) |
|
34 |
(* ProjB2 *) |
|
35 |
(* ---------------------------------------------------------------- *) |
|
36 |
||
37 |
||
10835 | 38 |
Goal "ProjB2$UU = UU"; |
4098 | 39 |
by (simp_tac (simpset() addsimps [ProjB2_def]) 1); |
3071 | 40 |
qed"ProjB2_UU"; |
41 |
||
10835 | 42 |
Goal "ProjB2$nil = nil"; |
4098 | 43 |
by (simp_tac (simpset() addsimps [ProjB2_def]) 1); |
3071 | 44 |
qed"ProjB2_nil"; |
45 |
||
10835 | 46 |
Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs"; |
4098 | 47 |
by (simp_tac (simpset() addsimps [ProjB2_def]) 1); |
3071 | 48 |
qed"ProjB2_cons"; |
49 |
||
50 |
||
51 |
||
52 |
(* ---------------------------------------------------------------- *) |
|
53 |
(* Filter_ex2 *) |
|
54 |
(* ---------------------------------------------------------------- *) |
|
55 |
||
56 |
||
10835 | 57 |
Goal "Filter_ex2 sig$UU=UU"; |
4098 | 58 |
by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1); |
3071 | 59 |
qed"Filter_ex2_UU"; |
60 |
||
10835 | 61 |
Goal "Filter_ex2 sig$nil=nil"; |
4098 | 62 |
by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1); |
3071 | 63 |
qed"Filter_ex2_nil"; |
64 |
||
10835 | 65 |
Goal "Filter_ex2 sig$(at >> xs) = \ |
17233 | 66 |
\ (if (fst at:actions sig) \ |
67 |
\ then at >> (Filter_ex2 sig$xs) \ |
|
10835 | 68 |
\ else Filter_ex2 sig$xs)"; |
3071 | 69 |
|
4098 | 70 |
by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1); |
3071 | 71 |
qed"Filter_ex2_cons"; |
72 |
||
73 |
||
74 |
(* ---------------------------------------------------------------- *) |
|
75 |
(* stutter2 *) |
|
76 |
(* ---------------------------------------------------------------- *) |
|
77 |
||
78 |
||
5068 | 79 |
Goal "stutter2 sig = (LAM ex. (%s. case ex of \ |
3071 | 80 |
\ nil => TT \ |
17233 | 81 |
\ | x##xs => (flift1 \ |
3521 | 82 |
\ (%p.(If Def ((fst p)~:actions sig) \ |
3071 | 83 |
\ then Def (s=(snd p)) \ |
84 |
\ else TT fi) \ |
|
10835 | 85 |
\ andalso (stutter2 sig$xs) (snd p)) \ |
86 |
\ $x) \ |
|
3071 | 87 |
\ ))"; |
88 |
by (rtac trans 1); |
|
3457 | 89 |
by (rtac fix_eq2 1); |
90 |
by (rtac stutter2_def 1); |
|
91 |
by (rtac beta_cfun 1); |
|
4098 | 92 |
by (simp_tac (simpset() addsimps [flift1_def]) 1); |
3071 | 93 |
qed"stutter2_unfold"; |
94 |
||
10835 | 95 |
Goal "(stutter2 sig$UU) s=UU"; |
3071 | 96 |
by (stac stutter2_unfold 1); |
97 |
by (Simp_tac 1); |
|
98 |
qed"stutter2_UU"; |
|
99 |
||
10835 | 100 |
Goal "(stutter2 sig$nil) s = TT"; |
3071 | 101 |
by (stac stutter2_unfold 1); |
102 |
by (Simp_tac 1); |
|
103 |
qed"stutter2_nil"; |
|
104 |
||
10835 | 105 |
Goal "(stutter2 sig$(at>>xs)) s = \ |
3521 | 106 |
\ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \ |
17233 | 107 |
\ andalso (stutter2 sig$xs) (snd at))"; |
4423 | 108 |
by (rtac trans 1); |
3071 | 109 |
by (stac stutter2_unfold 1); |
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
5068
diff
changeset
|
110 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1); |
3071 | 111 |
by (Simp_tac 1); |
112 |
qed"stutter2_cons"; |
|
113 |
||
114 |
||
115 |
Addsimps [stutter2_UU,stutter2_nil,stutter2_cons]; |
|
116 |
||
117 |
||
118 |
(* ---------------------------------------------------------------- *) |
|
119 |
(* stutter *) |
|
120 |
(* ---------------------------------------------------------------- *) |
|
121 |
||
5068 | 122 |
Goal "stutter sig (s, UU)"; |
4098 | 123 |
by (simp_tac (simpset() addsimps [stutter_def]) 1); |
3071 | 124 |
qed"stutter_UU"; |
125 |
||
5068 | 126 |
Goal "stutter sig (s, nil)"; |
4098 | 127 |
by (simp_tac (simpset() addsimps [stutter_def]) 1); |
3071 | 128 |
qed"stutter_nil"; |
129 |
||
5068 | 130 |
Goal "stutter sig (s, (a,t)>>ex) = \ |
3521 | 131 |
\ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))"; |
4833 | 132 |
by (simp_tac (simpset() addsimps [stutter_def]) 1); |
3071 | 133 |
qed"stutter_cons"; |
134 |
||
135 |
(* ----------------------------------------------------------------------------------- *) |
|
136 |
||
137 |
Delsimps [stutter2_UU,stutter2_nil,stutter2_cons]; |
|
138 |
||
139 |
val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons, |
|
140 |
ProjB2_UU,ProjB2_nil,ProjB2_cons, |
|
141 |
Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons, |
|
142 |
stutter_UU,stutter_nil,stutter_cons]; |
|
143 |
||
144 |
Addsimps compoex_simps; |
|
145 |
||
146 |
||
147 |
||
148 |
(* ------------------------------------------------------------------ *) |
|
149 |
(* The following lemmata aim for *) |
|
150 |
(* COMPOSITIONALITY on EXECUTION Level *) |
|
151 |
(* ------------------------------------------------------------------ *) |
|
152 |
||
153 |
||
154 |
(* --------------------------------------------------------------------- *) |
|
155 |
(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *) |
|
156 |
(* --------------------------------------------------------------------- *) |
|
157 |
||
5068 | 158 |
Goal "!s. is_exec_frag (A||B) (s,xs) \ |
10835 | 159 |
\ --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &\ |
160 |
\ is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"; |
|
3071 | 161 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
162 |
by (pair_induct_tac "xs" [is_exec_frag_def] 1); |
3071 | 163 |
(* main case *) |
164 |
ren "ss a t" 1; |
|
165 |
by (safe_tac set_cs); |
|
4833 | 166 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1)); |
3071 | 167 |
qed"lemma_1_1a"; |
168 |
||
169 |
||
170 |
(* --------------------------------------------------------------------- *) |
|
171 |
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) |
|
172 |
(* --------------------------------------------------------------------- *) |
|
173 |
||
5068 | 174 |
Goal "!s. is_exec_frag (A||B) (s,xs) \ |
10835 | 175 |
\ --> stutter (asig_of A) (fst s,ProjA2$xs) &\ |
17233 | 176 |
\ stutter (asig_of B) (snd s,ProjB2$xs)"; |
3071 | 177 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
178 |
by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1); |
3071 | 179 |
(* main case *) |
180 |
by (safe_tac set_cs); |
|
4833 | 181 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1)); |
3071 | 182 |
qed"lemma_1_1b"; |
183 |
||
184 |
||
185 |
(* --------------------------------------------------------------------- *) |
|
186 |
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *) |
|
187 |
(* --------------------------------------------------------------------- *) |
|
188 |
||
5068 | 189 |
Goal "!s. (is_exec_frag (A||B) (s,xs) \ |
3842 | 190 |
\ --> Forall (%x. fst x:act (A||B)) xs)"; |
3071 | 191 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
192 |
by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1); |
3071 | 193 |
(* main case *) |
194 |
by (safe_tac set_cs); |
|
17233 | 195 |
by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ |
3071 | 196 |
[actions_asig_comp,asig_of_par]) 1)); |
197 |
qed"lemma_1_1c"; |
|
198 |
||
199 |
||
200 |
(* ----------------------------------------------------------------------- *) |
|
201 |
(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) |
|
202 |
(* ----------------------------------------------------------------------- *) |
|
203 |
||
17233 | 204 |
Goal |
10835 | 205 |
"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &\ |
206 |
\ is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &\ |
|
207 |
\ stutter (asig_of A) (fst s,(ProjA2$xs)) & \ |
|
208 |
\ stutter (asig_of B) (snd s,(ProjB2$xs)) & \ |
|
3842 | 209 |
\ Forall (%x. fst x:act (A||B)) xs \ |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
210 |
\ --> is_exec_frag (A||B) (s,xs)"; |
3071 | 211 |
|
212 |
by (pair_induct_tac "xs" [Forall_def,sforall_def, |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
213 |
is_exec_frag_def, stutter_def] 1); |
4681 | 214 |
by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]) 1); |
3071 | 215 |
by (safe_tac set_cs); |
216 |
(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *) |
|
217 |
by (rotate_tac ~4 1); |
|
4681 | 218 |
by (Asm_full_simp_tac 1); |
3071 | 219 |
by (rotate_tac ~4 1); |
4681 | 220 |
by (Asm_full_simp_tac 1); |
3071 | 221 |
qed"lemma_1_2"; |
222 |
||
223 |
||
224 |
(* ------------------------------------------------------------------ *) |
|
225 |
(* COMPOSITIONALITY on EXECUTION Level *) |
|
226 |
(* Main Theorem *) |
|
227 |
(* ------------------------------------------------------------------ *) |
|
228 |
||
229 |
||
17233 | 230 |
Goal |
11655 | 231 |
"(ex:executions(A||B)) =\ |
3521 | 232 |
\(Filter_ex (asig_of A) (ProjA ex) : executions A &\ |
233 |
\ Filter_ex (asig_of B) (ProjB ex) : executions B &\ |
|
234 |
\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\ |
|
3842 | 235 |
\ Forall (%x. fst x:act (A||B)) (snd ex))"; |
3071 | 236 |
|
4098 | 237 |
by (simp_tac (simpset() addsimps [executions_def,ProjB_def, |
3071 | 238 |
Filter_ex_def,ProjA_def,starts_of_par]) 1); |
239 |
by (pair_tac "ex" 1); |
|
240 |
by (rtac iffI 1); |
|
241 |
(* ==> *) |
|
242 |
by (REPEAT (etac conjE 1)); |
|
4098 | 243 |
by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp, |
3071 | 244 |
lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1); |
245 |
(* <== *) |
|
246 |
by (REPEAT (etac conjE 1)); |
|
4098 | 247 |
by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1); |
3071 | 248 |
qed"compositionality_ex"; |
249 |
||
250 |
||
3521 | 251 |
(* ------------------------------------------------------------------ *) |
252 |
(* COMPOSITIONALITY on EXECUTION Level *) |
|
253 |
(* For Modules *) |
|
254 |
(* ------------------------------------------------------------------ *) |
|
255 |
||
5068 | 256 |
Goalw [Execs_def,par_execs_def] |
3521 | 257 |
|
258 |
"Execs (A||B) = par_execs (Execs A) (Execs B)"; |
|
259 |
||
4098 | 260 |
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1); |
4423 | 261 |
by (rtac set_ext 1); |
4098 | 262 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1); |
3521 | 263 |
qed"compositionality_ex_modules"; |