|
1 (* |
|
2 Folgende Theoremlisten wurden in MuIOA.ML definiert: |
|
3 val ioa_simps = [asig_of_def,starts_of_def,trans_of_def]; |
|
4 val asig_simps = [asig_inputs_def,asig_outputs_def,asig_internals_def,actions_def]; |
|
5 val comp_simps = [par_def,asig_comp_def]; |
|
6 val restrict_simps = [restrict_def,restrict_asig_def]; |
|
7 val hide_simps = [hide_def,hide_asig_def]; |
|
8 val rename_simps = [rename_def,rename_set_def]; |
|
9 *) |
|
10 |
|
11 (* call_sim_tac invokes oracle "Sim" *) |
|
12 fun call_sim_tac theory thm_list i state = |
|
13 let val sign = #sign (rep_thm state); |
|
14 val (subgoal::_) = drop(i-1,prems_of state); |
|
15 val OraAss = invoke_oracle theory "Sim" (sign,SimOracleExn (subgoal,theory,thm_list)); |
|
16 in |
|
17 (cut_facts_tac [OraAss] i) state |
|
18 end; |
|
19 |
|
20 (* is_sim_tac makes additionally to call_sim_tac some simplifications, |
|
21 which are suitable for implementation realtion formulas *) |
|
22 fun is_sim_tac theory thm_list i state = |
|
23 let val sign = #sign (rep_thm state); |
|
24 in |
|
25 case drop(i-1,prems_of state) of |
|
26 [] => PureGeneral.Seq.empty | |
|
27 subgoal::_ => EVERY[REPEAT(etac thin_rl i), |
|
28 simp_tac (simpset() addsimps [ioa_implements_def]) i, |
|
29 rtac conjI i, |
|
30 rtac conjI (i+1), |
|
31 TRY(call_sim_tac theory thm_list (i+2)), |
|
32 TRY(atac (i+2)), |
|
33 REPEAT(rtac refl (i+2)), |
|
34 simp_tac (simpset() addsimps (thm_list @ |
|
35 comp_simps @ restrict_simps @ hide_simps @ |
|
36 rename_simps @ ioa_simps @ asig_simps)) (i+1), |
|
37 simp_tac (simpset() addsimps (thm_list @ |
|
38 comp_simps @ restrict_simps @ hide_simps @ |
|
39 rename_simps @ ioa_simps @ asig_simps)) (i)] state |
|
40 end; |