1 |
|
2 (* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy). |
|
3 There, implementation relations for I/O automatons are proved using |
|
4 the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *) |
|
5 |
|
6 exception SimFailureExn of string; |
|
7 |
|
8 val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"]; |
|
9 val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def", |
|
10 thm "asig_internals_def", thm "actions_def"]; |
|
11 val comp_simps = [thm "par_def", thm "asig_comp_def"]; |
|
12 val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"]; |
|
13 val hide_simps = [thm "hide_def", thm "hide_asig_def"]; |
|
14 val rename_simps = [thm "rename_def", thm "rename_set_def"]; |
|
15 |
|
16 local |
|
17 |
|
18 exception malformed; |
|
19 |
|
20 fun fst_type (Type("*",[a,_])) = a | |
|
21 fst_type _ = raise malformed; |
|
22 fun snd_type (Type("*",[_,a])) = a | |
|
23 snd_type _ = raise malformed; |
|
24 |
|
25 fun element_type (Type("set",[a])) = a | |
|
26 element_type t = raise malformed; |
|
27 |
|
28 fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = |
|
29 let |
|
30 val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA)); |
|
31 val sig_typ = fst_type aut_typ; |
|
32 val int_typ = fst_type sig_typ |
|
33 in |
|
34 Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $ |
|
35 (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA) |
|
36 end |
|
37 | |
|
38 IntC sg t = |
|
39 error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t)); |
|
40 |
|
41 fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = |
|
42 let |
|
43 val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA)); |
|
44 val st_typ = fst_type(snd_type aut_typ) |
|
45 in |
|
46 Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA |
|
47 end |
|
48 | |
|
49 StartC sg t = |
|
50 error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t)); |
|
51 |
|
52 fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = |
|
53 let |
|
54 val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA)); |
|
55 val tr_typ = fst_type(snd_type(snd_type aut_typ)) |
|
56 in |
|
57 Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA |
|
58 end |
|
59 | |
|
60 TransC sg t = |
|
61 error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t)); |
|
62 |
|
63 fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) = |
|
64 let |
|
65 val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA)); |
|
66 val sig_typ = fst_type aut_typ; |
|
67 val int_typ = fst_type sig_typ |
|
68 in |
|
69 Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $ |
|
70 (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA) |
|
71 end |
|
72 | |
|
73 IntA sg t = |
|
74 error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t)); |
|
75 |
|
76 fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) = |
|
77 let |
|
78 val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA)); |
|
79 val st_typ = fst_type(snd_type aut_typ) |
|
80 in |
|
81 Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA |
|
82 end |
|
83 | |
|
84 StartA sg t = |
|
85 error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t)); |
|
86 |
|
87 fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) = |
|
88 let |
|
89 val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA)); |
|
90 val tr_typ = fst_type(snd_type(snd_type aut_typ)) |
|
91 in |
|
92 Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA |
|
93 end |
|
94 | |
|
95 TransA sg t = |
|
96 error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t)); |
|
97 |
|
98 fun delete_ul [] = [] |
|
99 | delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs)) |
|
100 then (let val (_::_::_::s) = xs in delete_ul s end) |
|
101 else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) |
|
102 then (let val (_::_::_::s) = xs in delete_ul s end) |
|
103 else (x::delete_ul xs)); |
|
104 |
|
105 fun delete_ul_string s = implode(delete_ul (explode s)); |
|
106 |
|
107 fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) | |
|
108 type_list_of sign a = [(Sign.string_of_typ sign a)]; |
|
109 |
|
110 fun structured_tuple l (Type("*",s::t::_)) = |
|
111 let |
|
112 val (r,str) = structured_tuple l s; |
|
113 in |
|
114 (fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")") |
|
115 end | |
|
116 structured_tuple (a::r) t = (r,a) | |
|
117 structured_tuple [] _ = raise malformed; |
|
118 |
|
119 fun varlist_of _ _ [] = [] | |
|
120 varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r); |
|
121 |
|
122 fun string_of [] = "" | |
|
123 string_of (a::r) = a ^ " " ^ (string_of r); |
|
124 |
|
125 fun tupel_typed_of _ _ _ [] = "" | |
|
126 tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a | |
|
127 tupel_typed_of sign s n (a::r) = |
|
128 s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r); |
|
129 |
|
130 fun double_tupel_typed_of _ _ _ _ [] = "" | |
|
131 double_tupel_typed_of sign s t n [a] = |
|
132 s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ |
|
133 t ^ (Int.toString(n)) ^ "::" ^ a | |
|
134 double_tupel_typed_of sign s t n (a::r) = |
|
135 s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ |
|
136 t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r); |
|
137 |
|
138 fun tupel_of _ _ _ [] = "" | |
|
139 tupel_of sign s n [a] = s ^ (Int.toString(n)) | |
|
140 tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r); |
|
141 |
|
142 fun double_tupel_of _ _ _ _ [] = "" | |
|
143 double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^ |
|
144 t ^ (Int.toString(n)) | |
|
145 double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^ |
|
146 t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r); |
|
147 |
|
148 fun eq_string _ _ _ [] = "" | |
|
149 eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^ |
|
150 t ^ (Int.toString(n)) | |
|
151 eq_string s t n (a::r) = |
|
152 s ^ (Int.toString(n)) ^ " = " ^ |
|
153 t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r); |
|
154 |
|
155 fun merge_var_and_type [] [] = "" | |
|
156 merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) | |
|
157 merge_var_and_type _ _ = raise malformed; |
|
158 |
|
159 in |
|
160 |
|
161 fun mk_sim_oracle sign (subgoal, thl) = ( |
|
162 let |
|
163 val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign; |
|
164 val concl = Logic.strip_imp_concl subgoal; |
|
165 val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl)); |
|
166 val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl)); |
|
167 val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl)); |
|
168 val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl)); |
|
169 val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl)); |
|
170 val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl)); |
|
171 |
|
172 val action_type_str = |
|
173 Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl))))); |
|
174 |
|
175 val abs_state_type_list = |
|
176 type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl))))); |
|
177 val con_state_type_list = |
|
178 type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl))))); |
|
179 |
|
180 val tupel_eq = eq_string "s" "t" 0 abs_state_type_list; |
|
181 |
|
182 val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list; |
|
183 val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list; |
|
184 val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list; |
|
185 val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list; |
|
186 |
|
187 val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list; |
|
188 val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list; |
|
189 val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list; |
|
190 val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list; |
|
191 val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list; |
|
192 val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list; |
|
193 val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list; |
|
194 val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list; |
|
195 val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list; |
|
196 val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list; |
|
197 |
|
198 val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list; |
|
199 val abs_post_varlist = varlist_of 0 "t" abs_state_type_list; |
|
200 val abs_u_varlist = varlist_of 0 "u" abs_state_type_list; |
|
201 val abs_v_varlist = varlist_of 0 "v" abs_state_type_list; |
|
202 val con_pre_varlist = varlist_of 0 "cs" con_state_type_list; |
|
203 val con_post_varlist = varlist_of 0 "ct" con_state_type_list; |
|
204 |
|
205 val abs_post_str = string_of abs_post_varlist; |
|
206 val abs_u_str = string_of abs_u_varlist; |
|
207 val con_post_str = string_of con_post_varlist; |
|
208 |
|
209 val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list; |
|
210 val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list; |
|
211 val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list; |
|
212 val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list; |
|
213 |
|
214 val abs_pre_tupel_struct = snd( |
|
215 structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl)))))); |
|
216 val abs_post_tupel_struct = snd( |
|
217 structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl)))))); |
|
218 val con_pre_tupel_struct = snd( |
|
219 structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl)))))); |
|
220 val con_post_tupel_struct = snd( |
|
221 structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl)))))); |
|
222 in |
|
223 ( |
|
224 OldGoals.push_proof(); |
|
225 Goal |
|
226 ( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^ |
|
227 "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ |
|
228 "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^ |
|
229 "). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^ |
|
230 "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^ |
|
231 "). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^ |
|
232 "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ |
|
233 ")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^ |
|
234 "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ |
|
235 ")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^ |
|
236 "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ |
|
237 "). ? (a::(" ^ action_type_str ^ |
|
238 ")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^ |
|
239 ")) --> (IntStepStar_of_A = mu (% P (" ^ abs_s_t_tupel_typed ^ |
|
240 "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^ |
|
241 ") & P(" ^ abs_u_t_tupel ^ ")))" ^ |
|
242 ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ |
|
243 ")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ |
|
244 ")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^ |
|
245 ". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^ |
|
246 "Trans_of_A (" ^ abs_u_v_tupel ^ ") a & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^ |
|
247 ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ |
|
248 "). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^ |
|
249 ". Trans_of_C (" ^ con_s_t_tupel ^ ") a -->" ^ " (? " ^ abs_post_str ^ |
|
250 ". Move_of_A (" ^ abs_s_t_tupel ^ ") a & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^ |
|
251 ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^ |
|
252 ". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^ |
|
253 ")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))"); |
|
254 by (REPEAT (rtac impI 1)); |
|
255 by (REPEAT (dtac eq_reflection 1)); |
|
256 (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) |
|
257 by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs) |
|
258 delsimps [not_iff,split_part]) |
|
259 addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ |
|
260 rename_simps @ ioa_simps @ asig_simps)) 1); |
|
261 by (full_simp_tac |
|
262 (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); |
|
263 by (REPEAT (if_full_simp_tac |
|
264 (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); |
|
265 by (call_mucke_tac 1); |
|
266 (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *) |
|
267 by (atac 1); |
|
268 result(); |
|
269 OldGoals.pop_proof(); |
|
270 Logic.strip_imp_concl subgoal |
|
271 ) |
|
272 end) |
|
273 handle malformed => |
|
274 error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal)); |
|
275 |
|
276 end |
|