thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
1 (* Title: HOL/Tools/Metis/metis_tactics.ML
2 Author: Kong W. Susanto, Cambridge University Computer Laboratory
3 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
4 Author: Jasmin Blanchette, TU Muenchen
5 Copyright Cambridge University 2007
7 HOL setup for the Metis prover.
10 signature METIS_TACTICS =
13 val full_typesN : string
14 val partial_typesN : string
15 val no_typesN : string
16 val really_full_type_enc : string
17 val full_type_enc : string
18 val partial_type_enc : string
19 val no_type_enc : string
20 val full_type_syss : string list
21 val partial_type_syss : string list
22 val trace : bool Config.T
23 val verbose : bool Config.T
24 val new_skolemizer : bool Config.T
25 val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
26 val setup : theory -> theory
29 structure Metis_Tactics : METIS_TACTICS =
34 open Metis_Reconstruct
38 val full_typesN = "full_types"
39 val partial_typesN = "partial_types"
40 val no_typesN = "no_types"
42 val really_full_type_enc = "mangled_tags_heavy"
43 val full_type_enc = "poly_preds_heavy_query"
44 val partial_type_enc = "poly_args"
45 val no_type_enc = "erased"
47 val full_type_syss = [full_type_enc, really_full_type_enc]
48 val partial_type_syss = partial_type_enc :: full_type_syss
50 val type_enc_aliases =
51 [(full_typesN, full_type_syss),
52 (partial_typesN, partial_type_syss),
53 (no_typesN, [no_type_enc])]
55 fun method_call_for_type_enc type_syss =
57 (case AList.find (op =) type_enc_aliases type_syss of
59 | _ => hd type_syss) ^ ")"
62 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
64 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
65 fun have_common_thm ths1 ths2 =
66 exists (member (Term.aconv_untyped o pairself prop_of) ths1)
67 (map Meson.make_meta_clause ths2)
69 (*Determining which axiom clauses are actually used*)
70 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
71 | used_axioms _ _ = NONE
73 (* Lightweight predicate type information comes in two flavors, "t = t'" and
74 "t => t'", where "t" and "t'" are the same term modulo type tags.
75 In Isabelle, type tags are stripped away, so we are left with "t = t" or
76 "t => t". Type tag idempotence is also handled this way. *)
77 fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
78 let val thy = Proof_Context.theory_of ctxt in
79 case hol_clause_from_metis ctxt sym_tab old_skolems mth of
80 Const (@{const_name HOL.eq}, _) $ _ $ t =>
81 t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
82 | Const (@{const_name disj}, _) $ t1 $ t2 =>
83 (if can HOLogic.dest_not t1 then t2 else t1)
84 |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
85 | _ => raise Fail "unexpected tags sym clause"
87 |> Meson.make_meta_clause
90 {ordering = Metis_KnuthBendixOrder.default,
91 orderLiterals = Metis_Clause.UnsignedLiteralOrder,
94 {clause = clause_params,
95 prefactor = #prefactor Metis_Active.default,
96 postfactor = #postfactor Metis_Active.default}
99 variablesWeight = 0.0,
100 literalsWeight = 0.0,
102 val resolution_params = {active = active_params, waiting = waiting_params}
104 (* Main function to start Metis proof and reconstruction *)
105 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
106 let val thy = Proof_Context.theory_of ctxt
108 Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
110 map2 (fn j => fn th =>
111 (Thm.get_name_hint th,
112 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
113 (0 upto length ths0 - 1) ths0
114 val ths = maps (snd o snd) th_cls_pairs
115 val dischargers = map (fst o snd) th_cls_pairs
116 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
117 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
118 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
119 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
120 val (sym_tab, axioms, old_skolems) =
121 prepare_metis_problem ctxt type_enc cls ths
122 fun get_isa_thm mth Isa_Reflexive_or_Trivial =
123 reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
124 | get_isa_thm _ (Isa_Raw ith) = ith
125 val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
126 val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
127 val thms = axioms |> map fst
128 val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
129 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
130 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
132 case filter (fn t => prop_of t aconv @{prop False}) cls of
133 false_th :: _ => [false_th RS @{thm FalseE}]
135 case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
136 |> Metis_Resolution.loop of
137 Metis_Resolution.Contradiction mth =>
138 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
139 Metis_Thm.toString mth)
140 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
141 (*add constraints arising from converting goal to clause form*)
142 val proof = Metis_Proof.proof mth
145 |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
146 val used = map_filter (used_axioms axioms) proof
147 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
148 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
149 val names = th_cls_pairs |> map fst
152 |> map_filter (fn (name, (_, cls)) =>
153 if have_common_thm used cls then SOME name
155 val unused_names = names |> subtract (op =) used_names
157 if not (null cls) andalso not (have_common_thm used cls) then
158 verbose_warning ctxt "The assumptions are inconsistent"
161 if not (null unused_names) then
162 "Unused theorems: " ^ commas_quote unused_names
163 |> verbose_warning ctxt
168 (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
169 [discharge_skolem_premises ctxt dischargers ith])
170 | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
172 | Metis_Resolution.Satisfiable _ =>
173 (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
174 if null fallback_type_syss then
177 raise METIS ("FOL_SOLVE",
178 "No first-order proof with the lemmas supplied");
181 handle METIS (loc, msg) =>
182 case fallback_type_syss of
183 [] => error ("Failed to replay Metis proof in Isabelle." ^
184 (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
187 (verbose_warning ctxt
188 ("Falling back on " ^
189 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
190 FOL_SOLVE fallback_type_syss ctxt cls ths0)
192 fun neg_clausify ctxt =
194 #> Meson.make_clauses_unsorted ctxt
195 #> map Meson_Clausify.introduce_combinators_in_theorem
198 fun preskolem_tac ctxt st0 =
199 (if exists (Meson.has_too_many_clauses ctxt)
200 (Logic.prems_of_goal (prop_of st0) 1) then
201 Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
202 THEN cnf.cnfx_rewrite_tac ctxt 1
206 val type_has_top_sort =
207 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
209 fun generic_metis_tac type_syss ctxt ths i st0 =
211 val _ = trace_msg ctxt (fn () =>
212 "Metis called with theorems\n" ^
213 cat_lines (map (Display.string_of_thm ctxt) ths))
214 fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
216 if exists_type type_has_top_sort (prop_of st0) then
217 verbose_warning ctxt "Proof state contains the universal sort {}"
220 Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
223 fun metis_tac [] = generic_metis_tac partial_type_syss
224 | metis_tac type_syss = generic_metis_tac type_syss
226 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
227 "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
228 We don't do it for nonschematic facts "X" because this breaks a few proofs
229 (in the rare and subtle case where a proof relied on extensionality not being
230 applied) and brings few benefits. *)
232 exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
234 fun method default_type_syss (override_type_syss, ths) ctxt facts =
237 if default_type_syss = full_type_syss then
238 legacy_feature "Old 'metisFT' method -- \
239 \use 'metis (full_types)' instead"
242 val (schem_facts, nonschem_facts) = List.partition has_tvar facts
243 val type_syss = override_type_syss |> the_default default_type_syss
245 HEADGOAL (Method.insert_tac nonschem_facts THEN'
247 o generic_metis_tac type_syss ctxt (schem_facts @ ths))
250 fun setup_method (binding, type_syss) =
251 ((Args.parens (Scan.repeat Parse.short_ident)
252 >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
253 |> Scan.option |> Scan.lift)
254 -- Attrib.thms >> (METHOD oo method type_syss)
255 |> Method.setup binding
258 [((@{binding metis}, partial_type_syss),
259 "Metis for FOL and HOL problems"),
260 ((@{binding metisFT}, full_type_syss),
261 "Metis for FOL/HOL problems with fully-typed translation")]
262 |> fold (uncurry setup_method)