src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
changeset 22819 a7b425bb668c
parent 17244 0b2ff9541727
child 28290 4cc2b6046258
     1.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 26 16:39:14 2007 +0200
     1.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Apr 26 16:39:31 2007 +0200
     1.3 @@ -8,4 +8,34 @@
     1.4  oracle sim_oracle ("term * thm list") =
     1.5    mk_sim_oracle
     1.6  
     1.7 +ML {*
     1.8 +(* call_sim_tac invokes oracle "Sim" *)
     1.9 +fun call_sim_tac thm_list i state = 
    1.10 +let val thy = Thm.theory_of_thm state;
    1.11 +        val (subgoal::_) = Library.drop(i-1,prems_of state);
    1.12 +        val OraAss = sim_oracle thy (subgoal,thm_list);
    1.13 +in cut_facts_tac [OraAss] i state end;
    1.14 +
    1.15 +
    1.16 +val ioa_implements_def = thm "ioa_implements_def";
    1.17 +
    1.18 +(* is_sim_tac makes additionally to call_sim_tac some simplifications,
    1.19 +	which are suitable for implementation realtion formulas *)
    1.20 +fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
    1.21 +  EVERY [REPEAT (etac thin_rl i),
    1.22 +	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
    1.23 +         rtac conjI i,
    1.24 +         rtac conjI (i+1),
    1.25 +	 TRY(call_sim_tac thm_list (i+2)),
    1.26 +	 TRY(atac (i+2)), 
    1.27 +         REPEAT(rtac refl (i+2)),
    1.28 +	 simp_tac (simpset() addsimps (thm_list @
    1.29 +				       comp_simps @ restrict_simps @ hide_simps @
    1.30 +				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
    1.31 +	 simp_tac (simpset() addsimps (thm_list @
    1.32 +				       comp_simps @ restrict_simps @ hide_simps @
    1.33 +				       rename_simps @ ioa_simps @ asig_simps)) (i)]);
    1.34 +
    1.35 +*}
    1.36 +
    1.37  end