src/HOL/Modelcheck/EindhovenSyn.thy
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 32010 cb1a1c94b4cd
child 35010 d6e492cea6e4
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
mueller@6466
     1
(*  Title:      HOL/Modelcheck/EindhovenSyn.thy
mueller@6466
     2
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@6466
     3
    Copyright   1997  TU Muenchen
mueller@6466
     4
*)
mueller@6466
     5
wenzelm@17272
     6
theory EindhovenSyn
wenzelm@17272
     7
imports MuCalculus
wenzelm@17272
     8
begin
mueller@6466
     9
mueller@6466
    10
syntax (Eindhoven output)
wenzelm@17272
    11
  True          :: bool                                 ("TRUE")
wenzelm@17272
    12
  False         :: bool                                 ("FALSE")
mueller@6466
    13
wenzelm@17272
    14
  Not           :: "bool => bool"                       ("NOT _" [40] 40)
wenzelm@17272
    15
  "op &"        :: "[bool, bool] => bool"               (infixr "AND" 35)
wenzelm@17272
    16
  "op |"        :: "[bool, bool] => bool"               (infixr "OR" 30)
mueller@6466
    17
wenzelm@21524
    18
  All_binder    :: "[idts, bool] => bool"               ("'((3A _./ _)')" [0, 10] 10)
wenzelm@21524
    19
  Ex_binder     :: "[idts, bool] => bool"               ("'((3E _./ _)')" [0, 10] 10)
wenzelm@17272
    20
   "_lambda"    :: "[pttrns, 'a] => 'b"                 ("(3L _./ _)" 10)
wenzelm@17272
    21
wenzelm@17272
    22
  "_idts"       :: "[idt, idts] => idts"                ("_,/_" [1, 0] 0)
wenzelm@17272
    23
  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/_" [1, 0] 0)
wenzelm@17272
    24
wenzelm@17272
    25
  "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3[mu _./ _])" 1000)
wenzelm@17272
    26
  "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3[nu _./ _])" 1000)
wenzelm@17272
    27
wenzelm@17272
    28
ML {*
wenzelm@32740
    29
  val trace_eindhoven = Unsynchronized.ref false;
wenzelm@17272
    30
*}
mueller@6466
    31
wenzelm@28290
    32
oracle mc_eindhoven_oracle =
wenzelm@17272
    33
{*
wenzelm@17272
    34
let
wenzelm@26939
    35
  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
mueller@6466
    36
wenzelm@17272
    37
  fun call_mc s =
wenzelm@17272
    38
    let
wenzelm@17272
    39
      val eindhoven_home = getenv "EINDHOVEN_HOME";
wenzelm@17272
    40
      val pmu =
wenzelm@17272
    41
        if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
wenzelm@17272
    42
        else eindhoven_home ^ "/pmu";
wenzelm@26225
    43
    in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
wenzelm@17272
    44
in
wenzelm@28290
    45
  fn cgoal =>
wenzelm@17272
    46
    let
wenzelm@28290
    47
      val thy = Thm.theory_of_cterm cgoal;
wenzelm@28290
    48
      val goal = Thm.term_of cgoal;
wenzelm@17272
    49
      val s = eindhoven_term thy goal;
wenzelm@17272
    50
      val debug = tracing ("MC debugger: " ^ s);
wenzelm@17272
    51
      val result = call_mc s;
wenzelm@17272
    52
    in
wenzelm@17272
    53
      if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
wenzelm@17272
    54
      (case result of
wenzelm@28290
    55
        "TRUE\n"  => cgoal |
wenzelm@17272
    56
        "FALSE\n" => error "MC oracle yields FALSE" |
wenzelm@17272
    57
      _ => error ("MC syntax error: " ^ result))
wenzelm@17272
    58
    end
wenzelm@17272
    59
end
wenzelm@17272
    60
*}
mueller@6466
    61
wenzelm@22819
    62
ML {*
wenzelm@22819
    63
fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
wenzelm@22819
    64
  let
wenzelm@22819
    65
    val thy = Thm.theory_of_thm state;
wenzelm@28290
    66
    val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal));
wenzelm@22819
    67
  in cut_facts_tac [assertion] i THEN atac i end) i state;
wenzelm@22819
    68
wenzelm@22819
    69
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
wenzelm@22819
    70
wenzelm@22819
    71
val pair_eta_expand_proc =
wenzelm@32010
    72
  Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
wenzelm@22819
    73
  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
wenzelm@22819
    74
wenzelm@22819
    75
val Eindhoven_ss =
wenzelm@26342
    76
  @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
wenzelm@22819
    77
*}
wenzelm@22819
    78
mueller@6466
    79
end