author | huffman |
Wed, 04 Mar 2009 17:12:23 -0800 | |
changeset 30273 | ecd6f0ca62ea |
parent 28290 | 4cc2b6046258 |
child 32010 | cb1a1c94b4cd |
permissions | -rw-r--r-- |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/Modelcheck/EindhovenSyn.thy |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
3 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
4 |
Copyright 1997 TU Muenchen |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
5 |
*) |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
6 |
|
17272 | 7 |
theory EindhovenSyn |
8 |
imports MuCalculus |
|
9 |
begin |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
10 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
11 |
syntax (Eindhoven output) |
17272 | 12 |
True :: bool ("TRUE") |
13 |
False :: bool ("FALSE") |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
14 |
|
17272 | 15 |
Not :: "bool => bool" ("NOT _" [40] 40) |
16 |
"op &" :: "[bool, bool] => bool" (infixr "AND" 35) |
|
17 |
"op |" :: "[bool, bool] => bool" (infixr "OR" 30) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
18 |
|
21524 | 19 |
All_binder :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10) |
20 |
Ex_binder :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10) |
|
17272 | 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 |
*} |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
32 |
|
28290 | 33 |
oracle mc_eindhoven_oracle = |
17272 | 34 |
{* |
35 |
let |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26342
diff
changeset
|
36 |
val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global; |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
37 |
|
17272 | 38 |
fun call_mc s = |
39 |
let |
|
40 |
val eindhoven_home = getenv "EINDHOVEN_HOME"; |
|
41 |
val pmu = |
|
42 |
if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set" |
|
43 |
else eindhoven_home ^ "/pmu"; |
|
26225 | 44 |
in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end; |
17272 | 45 |
in |
28290 | 46 |
fn cgoal => |
17272 | 47 |
let |
28290 | 48 |
val thy = Thm.theory_of_cterm cgoal; |
49 |
val goal = Thm.term_of cgoal; |
|
17272 | 50 |
val s = eindhoven_term thy goal; |
51 |
val debug = tracing ("MC debugger: " ^ s); |
|
52 |
val result = call_mc s; |
|
53 |
in |
|
54 |
if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else (); |
|
55 |
(case result of |
|
28290 | 56 |
"TRUE\n" => cgoal | |
17272 | 57 |
"FALSE\n" => error "MC oracle yields FALSE" | |
58 |
_ => error ("MC syntax error: " ^ result)) |
|
59 |
end |
|
60 |
end |
|
61 |
*} |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
62 |
|
22819 | 63 |
ML {* |
64 |
fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) => |
|
65 |
let |
|
66 |
val thy = Thm.theory_of_thm state; |
|
28290 | 67 |
val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal)); |
22819 | 68 |
in cut_facts_tac [assertion] i THEN atac i end) i state; |
69 |
||
70 |
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta")); |
|
71 |
||
72 |
val pair_eta_expand_proc = |
|
73 |
Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"] |
|
74 |
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE); |
|
75 |
||
76 |
val Eindhoven_ss = |
|
26342 | 77 |
@{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; |
22819 | 78 |
*} |
79 |
||
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
80 |
end |