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