author | paulson |
Mon, 07 Oct 1996 10:47:01 +0200 | |
changeset 2063 | 2395bc55b3e6 |
parent 2018 | bcd69cc47cf0 |
child 2513 | d708d8cdc8e8 |
permissions | -rw-r--r-- |
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); |
1894 | 18 |
by (safe_tac (!claset)); |
966 | 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); |
1894 | 35 |
by (safe_tac (!claset)); |
966 | 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); |
1894 | 43 |
by (safe_tac (!claset)); |
966 | 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"; |
|
1894 | 54 |
by(fast_tac (!claset addDs prems) 1); |
1052 | 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); |
1894 | 64 |
by (Fast_tac 1); |
1052 | 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); |
1894 | 76 |
by (Fast_tac 1); |
1052 | 77 |
(* projected execution is indeed an execution *) |
2018
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
78 |
by (asm_full_simp_tac |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
79 |
(!simpset addsimps [executions_def,is_execution_fragment_def, |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
80 |
par_def,starts_of_def,trans_of_def,filter_oseq_def] |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
81 |
setloop (split_tac[expand_if,expand_option_case])) 1); |
1052 | 82 |
qed"comp1_reachable"; |
83 |
||
84 |
||
85 |
(* Exact copy of proof of comp1_reachable for the second |
|
86 |
component of a parallel composition. *) |
|
87 |
goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"; |
|
1266 | 88 |
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); |
1052 | 89 |
by (etac bexE 1); |
90 |
by (res_inst_tac [("x", |
|
91 |
"(filter_oseq (%a.a:actions(asig_of(C2)))\ |
|
92 |
\ (fst ex), \ |
|
93 |
\ %i.snd (snd ex i))")] bexI 1); |
|
94 |
(* fst(s) is in projected execution *) |
|
1266 | 95 |
by (Simp_tac 1); |
1894 | 96 |
by (Fast_tac 1); |
1052 | 97 |
(* projected execution is indeed an execution *) |
2018
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
98 |
by (asm_full_simp_tac |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
99 |
(!simpset addsimps [executions_def,is_execution_fragment_def, |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
100 |
par_def,starts_of_def,trans_of_def,filter_oseq_def] |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
101 |
setloop (split_tac[expand_if,expand_option_case])) 1); |
1052 | 102 |
qed"comp2_reachable"; |
103 |
||
104 |
||
105 |
(* Composition of possibility-mappings *) |
|
106 |
||
107 |
goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \ |
|
108 |
\ externals(asig_of(A1))=externals(asig_of(C1)) &\ |
|
109 |
\ is_weak_pmap g C2 A2 & \ |
|
110 |
\ externals(asig_of(A2))=externals(asig_of(C2)) & \ |
|
111 |
\ compat_ioas C1 C2 & compat_ioas A1 A2 |] \ |
|
112 |
\ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"; |
|
113 |
by (rtac conjI 1); |
|
114 |
(* start_states *) |
|
1266 | 115 |
by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1); |
1894 | 116 |
by (Fast_tac 1); |
1052 | 117 |
(* transitions *) |
118 |
by (REPEAT (rtac allI 1)); |
|
119 |
by (rtac imp_conj_lemma 1); |
|
120 |
by (REPEAT(etac conjE 1)); |
|
1266 | 121 |
by (simp_tac (!simpset addsimps [externals_of_par_extra]) 1); |
122 |
by (simp_tac (!simpset addsimps [par_def]) 1); |
|
123 |
by (asm_full_simp_tac (!simpset addsimps [trans_of_def]) 1); |
|
1052 | 124 |
by (rtac (expand_if RS ssubst) 1); |
125 |
by (rtac conjI 1); |
|
126 |
by (rtac impI 1); |
|
127 |
by (etac disjE 1); |
|
128 |
(* case 1 a:e(A1) | a:e(A2) *) |
|
1266 | 129 |
by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, |
1052 | 130 |
ext_is_act]) 1); |
131 |
by (etac disjE 1); |
|
132 |
(* case 2 a:e(A1) | a~:e(A2) *) |
|
1266 | 133 |
by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, |
1052 | 134 |
ext_is_act,ext1_ext2_is_not_act2]) 1); |
135 |
(* case 3 a:~e(A1) | a:e(A2) *) |
|
1266 | 136 |
by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, |
1052 | 137 |
ext_is_act,ext1_ext2_is_not_act1]) 1); |
138 |
(* case 4 a:~e(A1) | a~:e(A2) *) |
|
139 |
by (rtac impI 1); |
|
140 |
by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1); |
|
141 |
(* delete auxiliary subgoal *) |
|
1266 | 142 |
by (Asm_full_simp_tac 2); |
1894 | 143 |
by (Fast_tac 2); |
1266 | 144 |
by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong] |
1052 | 145 |
setloop (split_tac [expand_if])) 1); |
146 |
by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN |
|
1266 | 147 |
asm_full_simp_tac(!simpset addsimps[comp1_reachable, |
1052 | 148 |
comp2_reachable])1)); |
149 |
qed"fxg_is_weak_pmap_of_product_IOA"; |
|
150 |
||
151 |
||
152 |
goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s"; |
|
1266 | 153 |
by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); |
1052 | 154 |
by (etac bexE 1); |
155 |
by (res_inst_tac [("x", |
|
156 |
"((%i. case (fst ex i) \ |
|
157 |
\ of None => None\ |
|
158 |
\ | Some(x) => g x) ,snd ex)")] bexI 1); |
|
1266 | 159 |
by (Simp_tac 1); |
1052 | 160 |
(* execution is indeed an execution of C *) |
2018
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
161 |
by (asm_full_simp_tac |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
162 |
(!simpset addsimps [executions_def,is_execution_fragment_def, |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
163 |
par_def,starts_of_def,trans_of_def,rename_def] |
bcd69cc47cf0
Moved Option into core HOL which caused a few local changes.
nipkow
parents:
1949
diff
changeset
|
164 |
setloop (split_tac[expand_option_case])) 1); |
2063 | 165 |
by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1); |
1052 | 166 |
qed"reachable_rename_ioa"; |
167 |
||
168 |
||
169 |
goal Solve.thy "!!f.[| is_weak_pmap f C A |]\ |
|
170 |
\ ==> (is_weak_pmap f (rename C g) (rename A g))"; |
|
1266 | 171 |
by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1); |
1052 | 172 |
by (rtac conjI 1); |
1266 | 173 |
by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1); |
1052 | 174 |
by (REPEAT (rtac allI 1)); |
175 |
by (rtac imp_conj_lemma 1); |
|
1266 | 176 |
by (simp_tac (!simpset addsimps [rename_def]) 1); |
177 |
by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1); |
|
1894 | 178 |
by (safe_tac (!claset)); |
1052 | 179 |
by (rtac (expand_if RS ssubst) 1); |
180 |
by (rtac conjI 1); |
|
181 |
by (rtac impI 1); |
|
182 |
by (etac disjE 1); |
|
183 |
by (etac exE 1); |
|
184 |
by (etac conjE 1); |
|
185 |
(* x is input *) |
|
186 |
by (dtac sym 1); |
|
187 |
by (dtac sym 1); |
|
1266 | 188 |
by (Asm_full_simp_tac 1); |
1052 | 189 |
by (REPEAT (hyp_subst_tac 1)); |
190 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); |
|
191 |
by (assume_tac 1); |
|
1266 | 192 |
by (Asm_full_simp_tac 1); |
1052 | 193 |
(* x is output *) |
194 |
by (etac exE 1); |
|
195 |
by (etac conjE 1); |
|
196 |
by (dtac sym 1); |
|
197 |
by (dtac sym 1); |
|
1266 | 198 |
by (Asm_full_simp_tac 1); |
1052 | 199 |
by (REPEAT (hyp_subst_tac 1)); |
200 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); |
|
201 |
by (assume_tac 1); |
|
1266 | 202 |
by (Asm_full_simp_tac 1); |
1052 | 203 |
(* x is internal *) |
1949
1badf0b08040
Simplified some proofs for compatibility with miniscoping
paulson
parents:
1894
diff
changeset
|
204 |
by (simp_tac (!simpset addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] |
1badf0b08040
Simplified some proofs for compatibility with miniscoping
paulson
parents:
1894
diff
changeset
|
205 |
addcongs [conj_cong]) 1); |
1052 | 206 |
by (rtac impI 1); |
207 |
by (etac conjE 1); |
|
208 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); |
|
1949
1badf0b08040
Simplified some proofs for compatibility with miniscoping
paulson
parents:
1894
diff
changeset
|
209 |
by (Auto_tac()); |
1052 | 210 |
qed"rename_through_pmap"; |