src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML
changeset 22819 a7b425bb668c
parent 22818 c0695a818c09
child 22820 e6803064a469
     1.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML	Thu Apr 26 16:39:14 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,29 +0,0 @@
     1.4 -
     1.5 -(* $Id$ *)
     1.6 -
     1.7 -(* call_sim_tac invokes oracle "Sim" *)
     1.8 -fun call_sim_tac thm_list i state = 
     1.9 -let val thy = Thm.theory_of_thm state;
    1.10 -        val (subgoal::_) = Library.drop(i-1,prems_of state);
    1.11 -        val OraAss = sim_oracle thy (subgoal,thm_list);
    1.12 -in cut_facts_tac [OraAss] i state end;
    1.13 -
    1.14 -
    1.15 -val ioa_implements_def = thm "ioa_implements_def";
    1.16 -
    1.17 -(* is_sim_tac makes additionally to call_sim_tac some simplifications,
    1.18 -	which are suitable for implementation realtion formulas *)
    1.19 -fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
    1.20 -  EVERY [REPEAT (etac thin_rl i),
    1.21 -	 simp_tac (simpset() addsimps [ioa_implements_def]) i,
    1.22 -         rtac conjI i,
    1.23 -         rtac conjI (i+1),
    1.24 -	 TRY(call_sim_tac thm_list (i+2)),
    1.25 -	 TRY(atac (i+2)), 
    1.26 -         REPEAT(rtac refl (i+2)),
    1.27 -	 simp_tac (simpset() addsimps (thm_list @
    1.28 -				       comp_simps @ restrict_simps @ hide_simps @
    1.29 -				       rename_simps @  ioa_simps @ asig_simps)) (i+1),
    1.30 -	 simp_tac (simpset() addsimps (thm_list @
    1.31 -				       comp_simps @ restrict_simps @ hide_simps @
    1.32 -				       rename_simps @ ioa_simps @ asig_simps)) (i)]);