author | blanchet |
Mon, 28 Jun 2010 18:02:36 +0200 | |
changeset 37618 | fa57a87f92a0 |
parent 37578 | 9367cb36b1c4 |
child 37619 | bcb19259f92a |
permissions | -rw-r--r-- |
35865 | 1 |
(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML |
2 |
Author: Jia Meng, Cambridge University Computer Laboratory |
|
3 |
||
4 |
MESON general tactic and proof method. |
|
5 |
*) |
|
6 |
||
7 |
signature MESON_TACTIC = |
|
8 |
sig |
|
9 |
val expand_defs_tac : thm -> tactic |
|
10 |
val meson_general_tac : Proof.context -> thm list -> int -> tactic |
|
11 |
val setup: theory -> theory |
|
12 |
end; |
|
13 |
||
14 |
structure Meson_Tactic : MESON_TACTIC = |
|
15 |
struct |
|
16 |
||
17 |
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*) |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
35865
diff
changeset
|
18 |
fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) = |
37618
fa57a87f92a0
get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet
parents:
37578
diff
changeset
|
19 |
(* FIXME String.isPrefix Clausifier.skolem_prefix a *) true |
35865 | 20 |
| is_absko _ = false; |
21 |
||
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
35865
diff
changeset
|
22 |
fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*) |
35865 | 23 |
is_Free t andalso not (member (op aconv) xs t) |
24 |
| is_okdef _ _ = false |
|
25 |
||
26 |
(*This function tries to cope with open locales, which introduce hypotheses of the form |
|
27 |
Free == t, conjecture clauses, which introduce various hypotheses, and also definitions |
|
28 |
of sko_ functions. *) |
|
29 |
fun expand_defs_tac st0 st = |
|
30 |
let val hyps0 = #hyps (rep_thm st0) |
|
31 |
val hyps = #hyps (crep_thm st) |
|
32 |
val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps |
|
33 |
val defs = filter (is_absko o Thm.term_of) newhyps |
|
34 |
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) |
|
35 |
(map Thm.term_of hyps) |
|
36 |
val fixed = OldTerm.term_frees (concl_of st) @ |
|
37 |
fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) [] |
|
38 |
in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; |
|
39 |
||
40 |
fun meson_general_tac ctxt ths i st0 = |
|
41 |
let |
|
42 |
val thy = ProofContext.theory_of ctxt |
|
43 |
val ctxt0 = Classical.put_claset HOL_cs ctxt |
|
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37574
diff
changeset
|
44 |
in |
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37574
diff
changeset
|
45 |
(Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i |
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37574
diff
changeset
|
46 |
THEN expand_defs_tac st0) st0 |
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37574
diff
changeset
|
47 |
end |
35865 | 48 |
|
49 |
val setup = |
|
50 |
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => |
|
51 |
SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) |
|
52 |
"MESON resolution proof procedure"; |
|
53 |
||
54 |
end; |