author | wenzelm |
Thu, 30 Nov 2000 20:04:16 +0100 | |
changeset 10548 | e8c774c12105 |
parent 7295 | fe09a0c5cebe |
child 13462 | 56610e2ba220 |
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 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
7 |
fun mc_eindhoven_tac i state = |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
8 |
let val sign = #sign (rep_thm state) |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
9 |
in |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
10 |
case drop(i-1,prems_of state) of |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
11 |
[] => Seq.empty | |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
12 |
subgoal::_ => |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
13 |
let val concl = Logic.strip_imp_concl subgoal; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
14 |
val OraAss = invoke_oracle EindhovenSyn.thy "eindhoven_mc" (sign,EindhovenOracleExn concl); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
15 |
in |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
16 |
((cut_facts_tac [OraAss] i) THEN (atac i)) state |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
17 |
end |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
18 |
end; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
19 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
20 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
21 |
Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))"; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
22 |
by (rtac ext 1); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
23 |
by (stac (surjective_pairing RS sym) 1); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
24 |
by (rtac refl 1); |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
25 |
qed "pair_eta_expand"; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
26 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
27 |
local |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
28 |
val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
29 |
val rew = mk_meta_eq pair_eta_expand; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
30 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
31 |
fun proc _ _ (Abs _) = Some rew |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
32 |
| proc _ _ _ = None; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
33 |
in |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
34 |
val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
35 |
end; |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
36 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
37 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
38 |
val Eindhoven_ss = |
7295 | 39 |
simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; |
40 |
||
41 |
(*check if user has pmu installed*) |
|
42 |
fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> ""; |
|
43 |
fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else (); |