src/HOL/Modelcheck/EindhovenSyn.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22819 a7b425bb668c
child 24634 38db11874724
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/Modelcheck/EindhovenSyn.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 theory EindhovenSyn
     8 imports MuCalculus
     9 begin
    10 
    11 syntax (Eindhoven output)
    12   True          :: bool                                 ("TRUE")
    13   False         :: bool                                 ("FALSE")
    14 
    15   Not           :: "bool => bool"                       ("NOT _" [40] 40)
    16   "op &"        :: "[bool, bool] => bool"               (infixr "AND" 35)
    17   "op |"        :: "[bool, bool] => bool"               (infixr "OR" 30)
    18 
    19   All_binder    :: "[idts, bool] => bool"               ("'((3A _./ _)')" [0, 10] 10)
    20   Ex_binder     :: "[idts, bool] => bool"               ("'((3E _./ _)')" [0, 10] 10)
    21    "_lambda"    :: "[pttrns, 'a] => 'b"                 ("(3L _./ _)" 10)
    22 
    23   "_idts"       :: "[idt, idts] => idts"                ("_,/_" [1, 0] 0)
    24   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/_" [1, 0] 0)
    25 
    26   "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3[mu _./ _])" 1000)
    27   "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3[nu _./ _])" 1000)
    28 
    29 ML {*
    30   val trace_eindhoven = ref false;
    31 *}
    32 
    33 oracle mc_eindhoven_oracle ("term") =
    34 {*
    35 let
    36   val eindhoven_term =
    37     setmp print_mode ["Eindhoven"] o Sign.string_of_term;
    38 
    39   fun call_mc s =
    40     let
    41       val eindhoven_home = getenv "EINDHOVEN_HOME";
    42       val pmu =
    43         if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
    44         else eindhoven_home ^ "/pmu";
    45     in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
    46 in
    47   fn thy => fn goal =>
    48     let
    49       val s = eindhoven_term thy goal;
    50       val debug = tracing ("MC debugger: " ^ s);
    51       val result = call_mc s;
    52     in
    53       if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
    54       (case result of
    55         "TRUE\n"  => goal |
    56         "FALSE\n" => error "MC oracle yields FALSE" |
    57       _ => error ("MC syntax error: " ^ result))
    58     end
    59 end
    60 *}
    61 
    62 ML {*
    63 fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
    64   let
    65     val thy = Thm.theory_of_thm state;
    66     val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
    67   in cut_facts_tac [assertion] i THEN atac i end) i state;
    68 
    69 val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
    70 
    71 val pair_eta_expand_proc =
    72   Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
    73   (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
    74 
    75 val Eindhoven_ss =
    76   simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
    77 
    78 (*check if user has pmu installed*)
    79 fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    80 fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
    81 *}
    82 
    83 end