src/HOL/Modelcheck/EindhovenSyn.thy
author wenzelm
Sat Feb 06 14:50:55 2010 +0100 (2010-02-06)
changeset 35010 d6e492cea6e4
parent 32740 9dd0a2f83429
child 37146 f652333bbf8e
permissions -rw-r--r--
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
     1 (*  Title:      HOL/Modelcheck/EindhovenSyn.thy
     2     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     3     Copyright   1997  TU Muenchen
     4 *)
     5 
     6 theory EindhovenSyn
     7 imports MuCalculus
     8 begin
     9 
    10 syntax (Eindhoven output)
    11   True          :: bool                                 ("TRUE")
    12   False         :: bool                                 ("FALSE")
    13 
    14   Not           :: "bool => bool"                       ("NOT _" [40] 40)
    15   "op &"        :: "[bool, bool] => bool"               (infixr "AND" 35)
    16   "op |"        :: "[bool, bool] => bool"               (infixr "OR" 30)
    17 
    18   All_binder    :: "[idts, bool] => bool"               ("'((3A _./ _)')" [0, 10] 10)
    19   Ex_binder     :: "[idts, bool] => bool"               ("'((3E _./ _)')" [0, 10] 10)
    20    "_lambda"    :: "[pttrns, 'a] => 'b"                 ("(3L _./ _)" 10)
    21 
    22   "_idts"       :: "[idt, idts] => idts"                ("_,/_" [1, 0] 0)
    23   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/_" [1, 0] 0)
    24 
    25   "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3[mu _./ _])" 1000)
    26   "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3[nu _./ _])" 1000)
    27 
    28 ML {*
    29   val trace_eindhoven = Unsynchronized.ref false;
    30 *}
    31 
    32 oracle mc_eindhoven_oracle =
    33 {*
    34 let
    35   val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
    36 
    37   fun call_mc s =
    38     let
    39       val eindhoven_home = getenv "EINDHOVEN_HOME";
    40       val pmu =
    41         if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
    42         else eindhoven_home ^ "/pmu";
    43     in #1 (bash_output ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
    44 in
    45   fn cgoal =>
    46     let
    47       val thy = Thm.theory_of_cterm cgoal;
    48       val goal = Thm.term_of cgoal;
    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"  => cgoal |
    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 (Thm.cterm_of 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 @{theory} "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 
    79 end