src/HOL/Modelcheck/EindhovenSyn.ML
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 7295 fe09a0c5cebe
child 15531 08c8dad8e399
permissions -rw-r--r--
sane interface for simprocs;
     1 (*  Title:      HOL/Modelcheck/EindhovenSyn.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 fun mc_eindhoven_tac i state =
     8 let val sign = #sign (rep_thm state)
     9 in 
    10 case drop(i-1,prems_of state) of
    11    [] => Seq.empty |
    12    subgoal::_ => 
    13 	let val concl = Logic.strip_imp_concl subgoal;
    14 	    val OraAss = invoke_oracle EindhovenSyn.thy "eindhoven_mc" (sign,EindhovenOracleExn concl);
    15 	in
    16 	((cut_facts_tac [OraAss] i) THEN (atac i)) state
    17         end
    18 end;
    19 
    20 
    21 Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
    22   by (rtac ext 1);
    23   by (stac (surjective_pairing RS sym) 1);
    24   by (rtac refl 1);
    25 qed "pair_eta_expand";
    26 
    27 val pair_eta_expand_proc =
    28   Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
    29   (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
    30 
    31 val Eindhoven_ss =
    32   simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    33 
    34 (*check if user has pmu installed*)
    35 fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    36 fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();