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