author | wenzelm |
Wed, 04 Apr 2007 23:29:33 +0200 | |
changeset 22596 | d0d2af4db18f |
parent 19741 | f65265d71426 |
permissions | -rw-r--r-- |
16152 | 1 |
|
2 |
(* $Id$ *) |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
3 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
4 |
(* call_sim_tac invokes oracle "Sim" *) |
7299 | 5 |
fun call_sim_tac thm_list i state = |
22596 | 6 |
let val thy = Thm.theory_of_thm state; |
15570 | 7 |
val (subgoal::_) = Library.drop(i-1,prems_of state); |
22596 | 8 |
val OraAss = sim_oracle thy (subgoal,thm_list); |
19741 | 9 |
in cut_facts_tac [OraAss] i state end; |
10 |
||
11 |
||
12 |
val ioa_implements_def = thm "ioa_implements_def"; |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
13 |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
14 |
(* is_sim_tac makes additionally to call_sim_tac some simplifications, |
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
15 |
which are suitable for implementation realtion formulas *) |
19741 | 16 |
fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) => |
17 |
EVERY [REPEAT (etac thin_rl i), |
|
18 |
simp_tac (simpset() addsimps [ioa_implements_def]) i, |
|
19 |
rtac conjI i, |
|
20 |
rtac conjI (i+1), |
|
21 |
TRY(call_sim_tac thm_list (i+2)), |
|
22 |
TRY(atac (i+2)), |
|
23 |
REPEAT(rtac refl (i+2)), |
|
24 |
simp_tac (simpset() addsimps (thm_list @ |
|
25 |
comp_simps @ restrict_simps @ hide_simps @ |
|
26 |
rename_simps @ ioa_simps @ asig_simps)) (i+1), |
|
27 |
simp_tac (simpset() addsimps (thm_list @ |
|
28 |
comp_simps @ restrict_simps @ hide_simps @ |
|
29 |
rename_simps @ ioa_simps @ asig_simps)) (i)]); |