src/HOL/Modelcheck/EindhovenSyn.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 20257 ebe183ff903d
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
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
wenzelm@17272
     7
fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
wenzelm@17272
     8
  let
wenzelm@17272
     9
    val thy = Thm.theory_of_thm state;
wenzelm@17272
    10
    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
wenzelm@17272
    11
  in cut_facts_tac [assertion] i THEN atac i end) i state;
mueller@6466
    12
mueller@6466
    13
Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
mueller@6466
    14
  by (rtac ext 1);
mueller@6466
    15
  by (stac (surjective_pairing RS sym) 1);
mueller@6466
    16
  by (rtac refl 1);
mueller@6466
    17
qed "pair_eta_expand";
mueller@6466
    18
wenzelm@13462
    19
val pair_eta_expand_proc =
wenzelm@17272
    20
  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
skalberg@15531
    21
  (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE);
mueller@6466
    22
mueller@6466
    23
val Eindhoven_ss =
wenzelm@7295
    24
  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
wenzelm@7295
    25
wenzelm@7295
    26
(*check if user has pmu installed*)
wenzelm@7295
    27
fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
wenzelm@7295
    28
fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();