966
|
1 |
(* Title: HOL/IOA/meta_theory/Solve.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Weak possibilities mapping (abstraction)
|
|
7 |
*)
|
|
8 |
|
1052
|
9 |
open Solve;
|
966
|
10 |
|
1266
|
11 |
Addsimps [mk_trace_thm,trans_in_actions];
|
966
|
12 |
|
1052
|
13 |
goalw Solve.thy [is_weak_pmap_def,traces_def]
|
966
|
14 |
"!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \
|
1052
|
15 |
\ is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
|
966
|
16 |
|
1266
|
17 |
by (simp_tac(!simpset addsimps [has_trace_def])1);
|
966
|
18 |
by (safe_tac set_cs);
|
|
19 |
|
1052
|
20 |
(* choose same trace, therefore same NF *)
|
|
21 |
by (res_inst_tac[("x","mk_trace C (fst ex)")] exI 1);
|
1266
|
22 |
by (Asm_full_simp_tac 1);
|
966
|
23 |
|
1052
|
24 |
(* give execution of abstract automata *)
|
|
25 |
by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1);
|
|
26 |
|
|
27 |
(* Traces coincide *)
|
1266
|
28 |
by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1);
|
966
|
29 |
|
|
30 |
(* Use lemma *)
|
|
31 |
by (forward_tac [states_of_exec_reachable] 1);
|
|
32 |
|
|
33 |
(* Now show that it's an execution *)
|
1266
|
34 |
by (asm_full_simp_tac(!simpset addsimps [executions_def]) 1);
|
966
|
35 |
by (safe_tac set_cs);
|
|
36 |
|
|
37 |
(* Start states map to start states *)
|
|
38 |
by (dtac bspec 1);
|
|
39 |
by (atac 1);
|
|
40 |
|
|
41 |
(* Show that it's an execution fragment *)
|
1266
|
42 |
by (asm_full_simp_tac (!simpset addsimps [is_execution_fragment_def])1);
|
966
|
43 |
by (safe_tac HOL_cs);
|
|
44 |
|
|
45 |
by (eres_inst_tac [("x","snd ex n")] allE 1);
|
|
46 |
by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
|
|
47 |
by (eres_inst_tac [("x","a")] allE 1);
|
1266
|
48 |
by (Asm_full_simp_tac 1);
|
966
|
49 |
qed "trace_inclusion";
|
1052
|
50 |
|
|
51 |
(* Lemmata *)
|
|
52 |
|
|
53 |
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
|
|
54 |
by(fast_tac (HOL_cs addDs prems) 1);
|
|
55 |
val imp_conj_lemma = result();
|
|
56 |
|
|
57 |
|
|
58 |
(* fist_order_tautology of externals_of_par *)
|
|
59 |
goal IOA.thy "a:externals(asig_of(A1||A2)) = \
|
|
60 |
\ (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) | \
|
|
61 |
\ a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) | \
|
|
62 |
\ a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
|
1266
|
63 |
by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
|
1052
|
64 |
by (fast_tac set_cs 1);
|
|
65 |
val externals_of_par_extra = result();
|
|
66 |
|
|
67 |
goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
|
1266
|
68 |
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1);
|
1052
|
69 |
by (etac bexE 1);
|
|
70 |
by (res_inst_tac [("x",
|
|
71 |
"(filter_oseq (%a.a:actions(asig_of(C1))) \
|
|
72 |
\ (fst ex), \
|
|
73 |
\ %i.fst (snd ex i))")] bexI 1);
|
|
74 |
(* fst(s) is in projected execution *)
|
1266
|
75 |
by (Simp_tac 1);
|
1052
|
76 |
by (fast_tac HOL_cs 1);
|
|
77 |
(* projected execution is indeed an execution *)
|
1266
|
78 |
by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
|
1052
|
79 |
par_def, starts_of_def,trans_of_def]) 1);
|
1266
|
80 |
by (simp_tac (!simpset addsimps [filter_oseq_def]) 1);
|
1052
|
81 |
by (REPEAT(rtac allI 1));
|
|
82 |
by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
|
|
83 |
by (etac disjE 1);
|
|
84 |
(* case 1: action sequence of || had already a None *)
|
1266
|
85 |
by (Asm_full_simp_tac 1);
|
1052
|
86 |
by (REPEAT(etac exE 1));
|
|
87 |
by (case_tac "y:actions(asig_of(C1))" 1);
|
|
88 |
(* case 2: action sequence of || had Some(a) and
|
|
89 |
filtered sequence also *)
|
1266
|
90 |
by (Asm_full_simp_tac 1);
|
1052
|
91 |
by (rtac impI 1);
|
|
92 |
by (REPEAT(hyp_subst_tac 1));
|
1266
|
93 |
by (Asm_full_simp_tac 1);
|
1052
|
94 |
(* case 3: action sequence pf || had Some(a) but
|
|
95 |
filtered sequence has None *)
|
1266
|
96 |
by (Asm_full_simp_tac 1);
|
1052
|
97 |
qed"comp1_reachable";
|
|
98 |
|
|
99 |
|
|
100 |
(* Exact copy of proof of comp1_reachable for the second
|
|
101 |
component of a parallel composition. *)
|
|
102 |
goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
|
1266
|
103 |
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1);
|
1052
|
104 |
by (etac bexE 1);
|
|
105 |
by (res_inst_tac [("x",
|
|
106 |
"(filter_oseq (%a.a:actions(asig_of(C2)))\
|
|
107 |
\ (fst ex), \
|
|
108 |
\ %i.snd (snd ex i))")] bexI 1);
|
|
109 |
(* fst(s) is in projected execution *)
|
1266
|
110 |
by (Simp_tac 1);
|
1052
|
111 |
by (fast_tac HOL_cs 1);
|
|
112 |
(* projected execution is indeed an execution *)
|
1266
|
113 |
by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
|
1052
|
114 |
par_def, starts_of_def,trans_of_def]) 1);
|
1266
|
115 |
by (simp_tac (!simpset addsimps [filter_oseq_def]) 1);
|
1052
|
116 |
by (REPEAT(rtac allI 1));
|
|
117 |
by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
|
|
118 |
by (etac disjE 1);
|
1266
|
119 |
by (Asm_full_simp_tac 1);
|
1052
|
120 |
by (REPEAT(etac exE 1));
|
|
121 |
by (case_tac "y:actions(asig_of(C2))" 1);
|
1266
|
122 |
by (Asm_full_simp_tac 1);
|
1052
|
123 |
by (rtac impI 1);
|
|
124 |
by (REPEAT(hyp_subst_tac 1));
|
1266
|
125 |
by (Asm_full_simp_tac 1);
|
|
126 |
by (Asm_full_simp_tac 1);
|
1052
|
127 |
qed"comp2_reachable";
|
|
128 |
|
|
129 |
|
|
130 |
(* Composition of possibility-mappings *)
|
|
131 |
|
|
132 |
goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
|
|
133 |
\ externals(asig_of(A1))=externals(asig_of(C1)) &\
|
|
134 |
\ is_weak_pmap g C2 A2 & \
|
|
135 |
\ externals(asig_of(A2))=externals(asig_of(C2)) & \
|
|
136 |
\ compat_ioas C1 C2 & compat_ioas A1 A2 |] \
|
|
137 |
\ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
|
|
138 |
by (rtac conjI 1);
|
|
139 |
(* start_states *)
|
1266
|
140 |
by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1);
|
1052
|
141 |
by (fast_tac set_cs 1);
|
|
142 |
(* transitions *)
|
|
143 |
by (REPEAT (rtac allI 1));
|
|
144 |
by (rtac imp_conj_lemma 1);
|
|
145 |
by (REPEAT(etac conjE 1));
|
1266
|
146 |
by (simp_tac (!simpset addsimps [externals_of_par_extra]) 1);
|
|
147 |
by (simp_tac (!simpset addsimps [par_def]) 1);
|
|
148 |
by (asm_full_simp_tac (!simpset addsimps [trans_of_def]) 1);
|
1052
|
149 |
by (rtac (expand_if RS ssubst) 1);
|
|
150 |
by (rtac conjI 1);
|
|
151 |
by (rtac impI 1);
|
|
152 |
by (etac disjE 1);
|
|
153 |
(* case 1 a:e(A1) | a:e(A2) *)
|
1266
|
154 |
by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable,
|
1052
|
155 |
ext_is_act]) 1);
|
|
156 |
by (etac disjE 1);
|
|
157 |
(* case 2 a:e(A1) | a~:e(A2) *)
|
1266
|
158 |
by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable,
|
1052
|
159 |
ext_is_act,ext1_ext2_is_not_act2]) 1);
|
|
160 |
(* case 3 a:~e(A1) | a:e(A2) *)
|
1266
|
161 |
by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable,
|
1052
|
162 |
ext_is_act,ext1_ext2_is_not_act1]) 1);
|
|
163 |
(* case 4 a:~e(A1) | a~:e(A2) *)
|
|
164 |
by (rtac impI 1);
|
|
165 |
by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
|
|
166 |
(* delete auxiliary subgoal *)
|
1266
|
167 |
by (Asm_full_simp_tac 2);
|
1052
|
168 |
by (fast_tac HOL_cs 2);
|
1266
|
169 |
by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
|
1052
|
170 |
setloop (split_tac [expand_if])) 1);
|
|
171 |
by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
|
1266
|
172 |
asm_full_simp_tac(!simpset addsimps[comp1_reachable,
|
1052
|
173 |
comp2_reachable])1));
|
|
174 |
qed"fxg_is_weak_pmap_of_product_IOA";
|
|
175 |
|
|
176 |
|
|
177 |
goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
|
1266
|
178 |
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1);
|
1052
|
179 |
by (etac bexE 1);
|
|
180 |
by (res_inst_tac [("x",
|
|
181 |
"((%i. case (fst ex i) \
|
|
182 |
\ of None => None\
|
|
183 |
\ | Some(x) => g x) ,snd ex)")] bexI 1);
|
1266
|
184 |
by (Simp_tac 1);
|
1052
|
185 |
(* execution is indeed an execution of C *)
|
1266
|
186 |
by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
|
1052
|
187 |
par_def, starts_of_def,trans_of_def,rename_def]) 1);
|
|
188 |
by (REPEAT(rtac allI 1));
|
|
189 |
by (cut_inst_tac [("x","fst ex n")] opt_cases 1);
|
|
190 |
by (etac disjE 1);
|
|
191 |
(* case 1: action sequence of rename C had already a None *)
|
1266
|
192 |
by (Asm_full_simp_tac 1);
|
1052
|
193 |
(* case 2 *)
|
|
194 |
by (REPEAT(etac exE 1));
|
|
195 |
by (etac conjE 1);
|
|
196 |
by (eres_inst_tac [("x","n")] allE 1);
|
|
197 |
by (eres_inst_tac [("x","y")] allE 1);
|
1266
|
198 |
by (Asm_full_simp_tac 1);
|
1052
|
199 |
by (etac exE 1);
|
|
200 |
by (etac conjE 1);
|
|
201 |
by (dtac sym 1);
|
|
202 |
by (dtac sym 1);
|
|
203 |
by (dtac sym 1);
|
1266
|
204 |
by (Asm_full_simp_tac 1);
|
1052
|
205 |
by (safe_tac HOL_cs);
|
|
206 |
qed"reachable_rename_ioa";
|
|
207 |
|
|
208 |
|
|
209 |
(* HOL Lemmata - must already exist ! *)
|
|
210 |
goal HOL.thy "(~(A|B)) =(~A&~B)";
|
|
211 |
by (fast_tac HOL_cs 1);
|
|
212 |
val disj_demorgan = result();
|
|
213 |
goal HOL.thy "(~(A&B)) =(~A|~B)";
|
|
214 |
by (fast_tac HOL_cs 1);
|
|
215 |
val conj_demorgan = result();
|
|
216 |
goal HOL.thy "(~(? x.P x)) =(! x. (~ (P x)))";
|
|
217 |
by (fast_tac HOL_cs 1);
|
|
218 |
val neg_ex = result();
|
|
219 |
|
|
220 |
|
|
221 |
goal Solve.thy "!!f.[| is_weak_pmap f C A |]\
|
|
222 |
\ ==> (is_weak_pmap f (rename C g) (rename A g))";
|
1266
|
223 |
by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1);
|
1052
|
224 |
by (rtac conjI 1);
|
1266
|
225 |
by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
|
1052
|
226 |
by (REPEAT (rtac allI 1));
|
|
227 |
by (rtac imp_conj_lemma 1);
|
1266
|
228 |
by (simp_tac (!simpset addsimps [rename_def]) 1);
|
|
229 |
by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
|
1052
|
230 |
by (safe_tac set_cs);
|
|
231 |
by (rtac (expand_if RS ssubst) 1);
|
|
232 |
by (rtac conjI 1);
|
|
233 |
by (rtac impI 1);
|
|
234 |
by (etac disjE 1);
|
|
235 |
by (etac exE 1);
|
|
236 |
by (etac conjE 1);
|
|
237 |
(* x is input *)
|
|
238 |
by (dtac sym 1);
|
|
239 |
by (dtac sym 1);
|
1266
|
240 |
by (Asm_full_simp_tac 1);
|
1052
|
241 |
by (REPEAT (hyp_subst_tac 1));
|
|
242 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
|
|
243 |
by (assume_tac 1);
|
1266
|
244 |
by (Asm_full_simp_tac 1);
|
1052
|
245 |
(* x is output *)
|
|
246 |
by (etac exE 1);
|
|
247 |
by (etac conjE 1);
|
|
248 |
by (dtac sym 1);
|
|
249 |
by (dtac sym 1);
|
1266
|
250 |
by (Asm_full_simp_tac 1);
|
1052
|
251 |
by (REPEAT (hyp_subst_tac 1));
|
|
252 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
|
|
253 |
by (assume_tac 1);
|
1266
|
254 |
by (Asm_full_simp_tac 1);
|
1052
|
255 |
(* x is internal *)
|
1266
|
256 |
by (simp_tac (!simpset addsimps [disj_demorgan,neg_ex,conj_demorgan] addcongs [conj_cong]) 1);
|
1052
|
257 |
by (rtac impI 1);
|
|
258 |
by (etac conjE 1);
|
|
259 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
|
|
260 |
by (assume_tac 1);
|
|
261 |
by (eres_inst_tac [("x","s")] allE 1);
|
|
262 |
by (eres_inst_tac [("x","t")] allE 1);
|
|
263 |
by (eres_inst_tac [("x","x")] allE 1);
|
|
264 |
by (eres_inst_tac [("x","x")] allE 1);
|
1266
|
265 |
by (Asm_full_simp_tac 1);
|
1052
|
266 |
qed"rename_through_pmap";
|