author | wenzelm |
Fri, 21 Oct 2005 18:14:38 +0200 | |
changeset 17959 | 8db36a108213 |
parent 17465 | 93fc1211603f |
child 18443 | a1d53af4c4c7 |
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 is_prefix [] s = true |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
98 |
| is_prefix (p::ps) [] = false |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
99 |
| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
100 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
101 |
fun delete_ul [] = [] |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
102 |
| delete_ul (x::xs) = if (is_prefix ("\^["::"["::"4"::"m"::[]) (x::xs)) |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
103 |
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
|
104 |
else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs)) |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
105 |
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
|
106 |
else (x::delete_ul xs)); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
107 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
108 |
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
|
109 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
110 |
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
|
111 |
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
|
112 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
113 |
fun structured_tuple l (Type("*",s::t::_)) = |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
114 |
let |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
115 |
val (r,str) = structured_tuple l s; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
116 |
in |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
117 |
(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
|
118 |
end | |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
119 |
structured_tuple (a::r) t = (r,a) | |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
120 |
structured_tuple [] _ = raise malformed; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
121 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
122 |
fun varlist_of _ _ [] = [] | |
17465 | 123 |
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
|
124 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
125 |
fun string_of [] = "" | |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
126 |
string_of (a::r) = a ^ " " ^ (string_of r); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
127 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
128 |
fun tupel_typed_of _ _ _ [] = "" | |
17465 | 129 |
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
|
130 |
tupel_typed_of sign s n (a::r) = |
17465 | 131 |
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
|
132 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
133 |
fun double_tupel_typed_of _ _ _ _ [] = "" | |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
134 |
double_tupel_typed_of sign s t n [a] = |
17465 | 135 |
s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ |
136 |
t ^ (Int.toString(n)) ^ "::" ^ a | |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
137 |
double_tupel_typed_of sign s t n (a::r) = |
17465 | 138 |
s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ |
139 |
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
|
140 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
141 |
fun tupel_of _ _ _ [] = "" | |
17465 | 142 |
tupel_of sign s n [a] = s ^ (Int.toString(n)) | |
143 |
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
|
144 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
145 |
fun double_tupel_of _ _ _ _ [] = "" | |
17465 | 146 |
double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^ |
147 |
t ^ (Int.toString(n)) | |
|
148 |
double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^ |
|
149 |
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
|
150 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
151 |
fun eq_string _ _ _ [] = "" | |
17465 | 152 |
eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^ |
153 |
t ^ (Int.toString(n)) | |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
154 |
eq_string s t n (a::r) = |
17465 | 155 |
s ^ (Int.toString(n)) ^ " = " ^ |
156 |
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
|
157 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
158 |
fun merge_var_and_type [] [] = "" | |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
159 |
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
|
160 |
merge_var_and_type _ _ = raise malformed; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
161 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
162 |
in |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
163 |
|
17241 | 164 |
fun mk_sim_oracle sign (subgoal,thl) = |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
165 |
(let |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
10128
diff
changeset
|
166 |
val weak_case_congs = DatatypePackage.weak_case_congs_of sign; |
10128 | 167 |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
168 |
val concl = (Logic.strip_imp_concl subgoal); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
169 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
170 |
val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl)); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
171 |
val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl)); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
177 |
val action_type_str = |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
178 |
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
|
179 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
180 |
val abs_state_type_list = |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
181 |
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
|
182 |
val con_state_type_list = |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
183 |
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
|
184 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
185 |
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
|
186 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
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
|
196 |
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
|
197 |
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
|
198 |
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
|
199 |
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
|
200 |
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
|
201 |
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
|
202 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
203 |
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
|
204 |
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
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
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
|
209 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
210 |
val abs_post_str = string_of abs_post_varlist; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
211 |
val abs_u_str = string_of abs_u_varlist; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
212 |
val con_post_str = string_of con_post_varlist; |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
213 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
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
|
217 |
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
|
218 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
219 |
val abs_pre_tupel_struct = snd( |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
220 |
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
|
221 |
val abs_post_tupel_struct = snd( |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
222 |
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
|
223 |
val con_pre_tupel_struct = snd( |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
224 |
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
|
225 |
val con_post_tupel_struct = snd( |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
226 |
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
|
227 |
in |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
228 |
( |
17959 | 229 |
OldGoals.push_proof(); |
7299 | 230 |
Goal |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
231 |
( "(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
|
232 |
"))) --> (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
|
233 |
"))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
234 |
"). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
235 |
"))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
236 |
"). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
237 |
"))) --> (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
|
238 |
")). ((" ^ 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
|
239 |
"))) --> (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
|
240 |
")). ((" ^ 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
|
241 |
"))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
242 |
"). ? (a::(" ^ action_type_str ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
243 |
")). 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
|
244 |
")) --> (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
|
245 |
"). (" ^ 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
|
246 |
") & P(" ^ abs_u_t_tupel ^ ")))" ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
247 |
") --> (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
|
248 |
")). (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
|
249 |
")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
250 |
". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
251 |
"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
|
252 |
")) --> (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
|
253 |
"). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
254 |
". 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
|
255 |
". 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
|
256 |
") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
257 |
". (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
|
258 |
")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))"); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
259 |
by (REPEAT (rtac impI 1)); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
260 |
by (REPEAT (dtac eq_reflection 1)); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
261 |
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) |
10128 | 262 |
by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs) |
7309 | 263 |
delsimps [not_iff,split_part]) |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
264 |
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
265 |
rename_simps @ ioa_simps @ asig_simps)) 1); |
10128 | 266 |
by (full_simp_tac |
267 |
(Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); |
|
268 |
by (REPEAT (if_full_simp_tac |
|
269 |
(simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); |
|
7299 | 270 |
by (call_mucke_tac 1); |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
271 |
(* 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
|
272 |
by (atac 1); |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
273 |
result(); |
17959 | 274 |
OldGoals.pop_proof(); |
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
275 |
Logic.strip_imp_concl subgoal |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
276 |
) |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
277 |
end) |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
278 |
handle malformed => |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
279 |
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
|
280 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
281 |
end |