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
     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 = SUBGOAL (fn (goal, _) =>
     8   let
     9     val thy = Thm.theory_of_thm state;
    10     val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
    11   in cut_facts_tac [assertion] i THEN atac i end) i state;
    12 
    13 Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
    14   by (rtac ext 1);
    15   by (stac (surjective_pairing RS sym) 1);
    16   by (rtac refl 1);
    17 qed "pair_eta_expand";
    18 
    19 val pair_eta_expand_proc =
    20   Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
    21   (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE);
    22 
    23 val Eindhoven_ss =
    24   simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    25 
    26 (*check if user has pmu installed*)
    27 fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    28 fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();