src/HOL/Modelcheck/EindhovenSyn.thy
changeset 22819 a7b425bb668c
parent 21524 7843e2fd14a9
child 24634 38db11874724
     1.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 26 16:39:14 2007 +0200
     1.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Apr 26 16:39:31 2007 +0200
     1.3 @@ -59,4 +59,25 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 +ML {*
     1.8 +fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
     1.9 +  let
    1.10 +    val thy = Thm.theory_of_thm state;
    1.11 +    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
    1.12 +  in cut_facts_tac [assertion] i THEN atac i end) i state;
    1.13 +
    1.14 +val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
    1.15 +
    1.16 +val pair_eta_expand_proc =
    1.17 +  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
    1.18 +  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
    1.19 +
    1.20 +val Eindhoven_ss =
    1.21 +  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    1.22 +
    1.23 +(*check if user has pmu installed*)
    1.24 +fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    1.25 +fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
    1.26 +*}
    1.27 +
    1.28  end