author | wenzelm |
Tue, 02 Jun 2015 09:10:05 +0200 | |
changeset 60357 | bc0827281dc1 |
parent 59498 | 50b60f501b05 |
child 60754 | 02924903a6fd |
permissions | -rw-r--r-- |
4530 | 1 |
(* Title: HOL/IOA/Solve.thy |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow & Konrad Slind |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
3 |
Copyright 1994 TU Muenchen |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
4 |
*) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
5 |
|
58889 | 6 |
section {* Weak possibilities mapping (abstraction) *} |
17288 | 7 |
|
8 |
theory Solve |
|
9 |
imports IOA |
|
10 |
begin |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
26342
diff
changeset
|
12 |
definition is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" where |
17288 | 13 |
"is_weak_pmap f C A == |
14 |
(!s:starts_of(C). f(s):starts_of(A)) & |
|
15 |
(!s t a. reachable C s & |
|
16 |
(s,a,t):trans_of(C) |
|
17 |
--> (if a:externals(asig_of(C)) then |
|
18 |
(f(s),a,f(t)):trans_of(A) |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
19 |
else f(s)=f(t)))" |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
20 |
|
19801 | 21 |
declare mk_trace_thm [simp] trans_in_actions [simp] |
22 |
||
23 |
lemma trace_inclusion: |
|
24 |
"[| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); |
|
25 |
is_weak_pmap f C A |] ==> traces(C) <= traces(A)" |
|
26 |
apply (unfold is_weak_pmap_def traces_def) |
|
27 |
||
28 |
apply (simp (no_asm) add: has_trace_def) |
|
29 |
apply safe |
|
30 |
apply (rename_tac ex1 ex2) |
|
31 |
||
32 |
(* choose same trace, therefore same NF *) |
|
33 |
apply (rule_tac x = "mk_trace C ex1" in exI) |
|
34 |
apply simp |
|
35 |
||
36 |
(* give execution of abstract automata *) |
|
37 |
apply (rule_tac x = "(mk_trace A ex1,%i. f (ex2 i))" in bexI) |
|
38 |
||
39 |
(* Traces coincide *) |
|
40 |
apply (simp (no_asm_simp) add: mk_trace_def filter_oseq_idemp) |
|
41 |
||
42 |
(* Use lemma *) |
|
43 |
apply (frule states_of_exec_reachable) |
|
44 |
||
45 |
(* Now show that it's an execution *) |
|
46 |
apply (simp add: executions_def) |
|
47 |
apply safe |
|
48 |
||
49 |
(* Start states map to start states *) |
|
50 |
apply (drule bspec) |
|
51 |
apply assumption |
|
52 |
||
53 |
(* Show that it's an execution fragment *) |
|
54 |
apply (simp add: is_execution_fragment_def) |
|
55 |
apply safe |
|
56 |
||
57 |
apply (erule_tac x = "ex2 n" in allE) |
|
58 |
apply (erule_tac x = "ex2 (Suc n)" in allE) |
|
59 |
apply (erule_tac x = a in allE) |
|
60 |
apply simp |
|
61 |
done |
|
62 |
||
63 |
(* Lemmata *) |
|
64 |
||
65 |
lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R" |
|
66 |
by blast |
|
67 |
||
68 |
||
69 |
(* fist_order_tautology of externals_of_par *) |
|
70 |
lemma externals_of_par_extra: |
|
71 |
"a:externals(asig_of(A1||A2)) = |
|
72 |
(a:externals(asig_of(A1)) & a:externals(asig_of(A2)) | |
|
73 |
a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) | |
|
74 |
a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))" |
|
75 |
apply (auto simp add: externals_def asig_of_par asig_comp_def asig_inputs_def asig_outputs_def) |
|
76 |
done |
|
77 |
||
78 |
lemma comp1_reachable: "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)" |
|
79 |
apply (simp add: reachable_def) |
|
80 |
apply (erule bexE) |
|
81 |
apply (rule_tac x = |
|
82 |
"(filter_oseq (%a. a:actions (asig_of (C1))) (fst ex) , %i. fst (snd ex i))" in bexI) |
|
83 |
(* fst(s) is in projected execution *) |
|
84 |
apply force |
|
85 |
(* projected execution is indeed an execution *) |
|
86 |
apply (simp cong del: if_weak_cong |
|
87 |
add: executions_def is_execution_fragment_def par_def starts_of_def |
|
88 |
trans_of_def filter_oseq_def |
|
89 |
split add: option.split) |
|
90 |
done |
|
91 |
||
92 |
||
93 |
(* Exact copy of proof of comp1_reachable for the second |
|
94 |
component of a parallel composition. *) |
|
95 |
lemma comp2_reachable: "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)" |
|
96 |
apply (simp add: reachable_def) |
|
97 |
apply (erule bexE) |
|
98 |
apply (rule_tac x = |
|
99 |
"(filter_oseq (%a. a:actions (asig_of (C2))) (fst ex) , %i. snd (snd ex i))" in bexI) |
|
100 |
(* fst(s) is in projected execution *) |
|
101 |
apply force |
|
102 |
(* projected execution is indeed an execution *) |
|
103 |
apply (simp cong del: if_weak_cong |
|
104 |
add: executions_def is_execution_fragment_def par_def starts_of_def |
|
105 |
trans_of_def filter_oseq_def |
|
106 |
split add: option.split) |
|
107 |
done |
|
108 |
||
109 |
declare split_if [split del] if_weak_cong [cong del] |
|
110 |
||
111 |
(*Composition of possibility-mappings *) |
|
112 |
lemma fxg_is_weak_pmap_of_product_IOA: |
|
113 |
"[| is_weak_pmap f C1 A1; |
|
114 |
externals(asig_of(A1))=externals(asig_of(C1)); |
|
115 |
is_weak_pmap g C2 A2; |
|
116 |
externals(asig_of(A2))=externals(asig_of(C2)); |
|
117 |
compat_ioas C1 C2; compat_ioas A1 A2 |] |
|
118 |
==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)" |
|
119 |
apply (unfold is_weak_pmap_def) |
|
120 |
apply (rule conjI) |
|
121 |
(* start_states *) |
|
122 |
apply (simp add: par_def starts_of_def) |
|
123 |
(* transitions *) |
|
124 |
apply (rule allI)+ |
|
125 |
apply (rule imp_conj_lemma) |
|
126 |
apply (simp (no_asm) add: externals_of_par_extra) |
|
127 |
apply (simp (no_asm) add: par_def) |
|
128 |
apply (simp add: trans_of_def) |
|
129 |
apply (simplesubst split_if) |
|
130 |
apply (rule conjI) |
|
131 |
apply (rule impI) |
|
132 |
apply (erule disjE) |
|
133 |
(* case 1 a:e(A1) | a:e(A2) *) |
|
134 |
apply (simp add: comp1_reachable comp2_reachable ext_is_act) |
|
135 |
apply (erule disjE) |
|
136 |
(* case 2 a:e(A1) | a~:e(A2) *) |
|
137 |
apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act2) |
|
138 |
(* case 3 a:~e(A1) | a:e(A2) *) |
|
139 |
apply (simp add: comp1_reachable comp2_reachable ext_is_act ext1_ext2_is_not_act1) |
|
140 |
(* case 4 a:~e(A1) | a~:e(A2) *) |
|
141 |
apply (rule impI) |
|
142 |
apply (subgoal_tac "a~:externals (asig_of (A1)) & a~:externals (asig_of (A2))") |
|
143 |
(* delete auxiliary subgoal *) |
|
144 |
prefer 2 |
|
145 |
apply force |
|
146 |
apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if) |
|
147 |
apply (tactic {* |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
148 |
REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE etac conjE 1) THEN |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
39159
diff
changeset
|
149 |
asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *}) |
19801 | 150 |
done |
151 |
||
152 |
||
153 |
lemma reachable_rename_ioa: "[| reachable (rename C g) s |] ==> reachable C s" |
|
154 |
apply (simp add: reachable_def) |
|
155 |
apply (erule bexE) |
|
156 |
apply (rule_tac x = "((%i. case (fst ex i) of None => None | Some (x) => g x) ,snd ex)" in bexI) |
|
157 |
apply (simp (no_asm)) |
|
158 |
(* execution is indeed an execution of C *) |
|
159 |
apply (simp add: executions_def is_execution_fragment_def par_def |
|
160 |
starts_of_def trans_of_def rename_def split add: option.split) |
|
161 |
apply force |
|
162 |
done |
|
163 |
||
164 |
||
165 |
lemma rename_through_pmap: "[| is_weak_pmap f C A |] |
|
166 |
==> (is_weak_pmap f (rename C g) (rename A g))" |
|
167 |
apply (simp add: is_weak_pmap_def) |
|
168 |
apply (rule conjI) |
|
169 |
apply (simp add: rename_def starts_of_def) |
|
170 |
apply (rule allI)+ |
|
171 |
apply (rule imp_conj_lemma) |
|
172 |
apply (simp (no_asm) add: rename_def) |
|
173 |
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) |
|
174 |
apply safe |
|
175 |
apply (simplesubst split_if) |
|
176 |
apply (rule conjI) |
|
177 |
apply (rule impI) |
|
178 |
apply (erule disjE) |
|
179 |
apply (erule exE) |
|
180 |
apply (erule conjE) |
|
181 |
(* x is input *) |
|
182 |
apply (drule sym) |
|
183 |
apply (drule sym) |
|
184 |
apply simp |
|
185 |
apply hypsubst+ |
|
186 |
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) |
|
187 |
apply assumption |
|
188 |
apply simp |
|
189 |
(* x is output *) |
|
190 |
apply (erule exE) |
|
191 |
apply (erule conjE) |
|
192 |
apply (drule sym) |
|
193 |
apply (drule sym) |
|
194 |
apply simp |
|
195 |
apply hypsubst+ |
|
196 |
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) |
|
197 |
apply assumption |
|
198 |
apply simp |
|
199 |
(* x is internal *) |
|
200 |
apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong) |
|
201 |
apply (rule impI) |
|
202 |
apply (erule conjE) |
|
203 |
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa) |
|
204 |
apply auto |
|
205 |
done |
|
206 |
||
207 |
declare split_if [split] if_weak_cong [cong] |
|
17288 | 208 |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
209 |
end |