equal
deleted
inserted
replaced
1 theory MuIOAOracle |
|
2 imports MuIOA |
|
3 begin |
|
4 |
|
5 oracle sim_oracle = mk_sim_oracle |
|
6 |
|
7 ML {* |
|
8 (* call_sim_tac invokes oracle "Sim" *) |
|
9 fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) => |
|
10 let val OraAss = sim_oracle (csubgoal,thm_list); |
|
11 in cut_facts_tac [OraAss] i end); |
|
12 |
|
13 |
|
14 val ioa_implements_def = thm "ioa_implements_def"; |
|
15 |
|
16 (* is_sim_tac makes additionally to call_sim_tac some simplifications, |
|
17 which are suitable for implementation realtion formulas *) |
|
18 fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) => |
|
19 EVERY [REPEAT (etac thin_rl i), |
|
20 simp_tac (ss addsimps [ioa_implements_def]) i, |
|
21 rtac conjI i, |
|
22 rtac conjI (i+1), |
|
23 TRY(call_sim_tac thm_list (i+2)), |
|
24 TRY(atac (i+2)), |
|
25 REPEAT(rtac refl (i+2)), |
|
26 simp_tac (ss addsimps (thm_list @ |
|
27 comp_simps @ restrict_simps @ hide_simps @ |
|
28 rename_simps @ ioa_simps @ asig_simps)) (i+1), |
|
29 simp_tac (ss addsimps (thm_list @ |
|
30 comp_simps @ restrict_simps @ hide_simps @ |
|
31 rename_simps @ ioa_simps @ asig_simps)) (i)]); |
|
32 |
|
33 *} |
|
34 |
|
35 end |
|