author | wenzelm |
Wed, 14 Sep 2005 23:14:57 +0200 | |
changeset 17394 | a8c9ed3f9818 |
parent 17272 | c63e5220ed77 |
child 20257 | ebe183ff903d |
permissions | -rw-r--r-- |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/Modelcheck/EindhovenSyn.ML |
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 |
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; |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
12 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
13 |
Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))"; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
14 |
by (rtac ext 1); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
15 |
by (stac (surjective_pairing RS sym) 1); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
16 |
by (rtac refl 1); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
17 |
qed "pair_eta_expand"; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
18 |
|
13462 | 19 |
val pair_eta_expand_proc = |
17272 | 20 |
Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"] |
15531 | 21 |
(fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE); |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
22 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
23 |
val Eindhoven_ss = |
7295 | 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 (); |