author | blanchet |
Wed, 26 Jan 2022 14:05:36 +0100 | |
changeset 75009 | d2f97439f53e |
parent 74075 | a5bab59d580b |
permissions | -rw-r--r-- |
39948 | 1 |
(* Title: HOL/Tools/Meson/meson_tactic.ML |
2 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
4 |
||
5 |
The "meson" proof method for HOL. |
|
6 |
*) |
|
7 |
||
8 |
signature MESON_TACTIC = |
|
9 |
sig |
|
10 |
val meson_general_tac : Proof.context -> thm list -> int -> tactic |
|
11 |
end; |
|
12 |
||
13 |
structure Meson_Tactic : MESON_TACTIC = |
|
14 |
struct |
|
15 |
||
16 |
fun meson_general_tac ctxt ths = |
|
42793 | 17 |
let val ctxt' = put_claset HOL_cs ctxt |
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
18 |
in |
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
19 |
Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt' |
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
20 |
false true 0) ths) |
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
21 |
end |
39948 | 22 |
|
75009
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
23 |
(* This is part of a workaround to avoid freezing schematic variables in \<^text>\<open>using\<close> facts. See |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
24 |
\<^file>\<open>~~/src/HOL/Tools/Metis/metis_tactic.ML\<close> for details. *) |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
25 |
val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
26 |
|
58817 | 27 |
val _ = |
28 |
Theory.setup |
|
75009
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
29 |
(Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt0 => |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
30 |
CONTEXT_METHOD (fn facts => fn (ctxt, st) => |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
31 |
let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
32 |
st |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
33 |
|> HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN' |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
34 |
CHANGED_PROP o meson_general_tac ctxt0 (schem_facts @ ths)) |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
35 |
|> TACTIC_CONTEXT ctxt |
d2f97439f53e
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)
blanchet
parents:
74075
diff
changeset
|
36 |
end))) |
58817 | 37 |
"MESON resolution proof procedure") |
39948 | 38 |
|
39 |
end; |