1 (* Title: HOL/Tools/Metis/metis_tactic.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_TACTIC =
12 val trace : bool Config.T
13 val verbose : bool Config.T
14 val new_skolemizer : bool Config.T
15 val type_has_top_sort : typ -> bool
17 string list -> string -> Proof.context -> thm list -> int -> tactic
18 val metis_lam_transs : string list
19 val parse_metis_options : (string list option * string option) parser
20 val setup : theory -> theory
23 structure Metis_Tactic : METIS_TACTIC =
29 open Metis_Reconstruct
32 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
34 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
35 fun have_common_thm ths1 ths2 =
36 exists (member (Term.aconv_untyped o pairself prop_of) ths1)
37 (map Meson.make_meta_clause ths2)
39 (*Determining which axiom clauses are actually used*)
40 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
41 | used_axioms _ _ = NONE
43 (* Lightweight predicate type information comes in two flavors, "t = t'" and
44 "t => t'", where "t" and "t'" are the same term modulo type tags.
45 In Isabelle, type tags are stripped away, so we are left with "t = t" or
46 "t => t". Type tag idempotence is also handled this way. *)
47 fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
48 let val thy = Proof_Context.theory_of ctxt in
49 case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
50 Const (@{const_name HOL.eq}, _) $ _ $ t =>
52 val ct = cterm_of thy t
53 val cT = ctyp_of_term ct
54 in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
55 | Const (@{const_name disj}, _) $ t1 $ t2 =>
56 (if can HOLogic.dest_not t1 then t2 else t1)
57 |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
58 | _ => raise Fail "expected reflexive or trivial clause"
60 |> Meson.make_meta_clause
62 fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
64 val thy = Proof_Context.theory_of ctxt
65 val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
66 val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
67 val ct = cterm_of thy (HOLogic.mk_Trueprop t)
68 in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
70 fun introduce_lambda_wrappers_in_theorem ctxt th =
71 if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
75 val th = th |> Drule.eta_contraction_rule
76 fun conv wrap ctxt ct =
77 if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
79 else case term_of ct of
81 Conv.abs_conv (conv false o snd) ctxt ct
83 ? (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
84 | _ => Conv.comb_conv (conv true ctxt) ct
85 val eqth = conv true ctxt (cprop_of th)
86 in Thm.equal_elim eqth th end
89 {ordering = Metis_KnuthBendixOrder.default,
90 orderLiterals = Metis_Clause.UnsignedLiteralOrder,
93 {clause = clause_params,
94 prefactor = #prefactor Metis_Active.default,
95 postfactor = #postfactor Metis_Active.default}
98 variablesWeight = 0.0,
101 val resolution_params = {active = active_params, waiting = waiting_params}
103 (* Main function to start Metis proof and reconstruction *)
104 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
105 let val thy = Proof_Context.theory_of ctxt
107 Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
109 map2 (fn j => fn th =>
110 (Thm.get_name_hint th,
111 Meson_Clausify.cnf_axiom ctxt new_skolemizer
112 (lam_trans = combinatorsN) 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 () => "type_enc = " ^ type_enc)
119 val type_enc = type_enc_from_string Sound type_enc
120 val (sym_tab, axioms0, concealed) =
121 prepare_metis_problem ctxt type_enc lam_trans cls ths
122 fun get_isa_thm mth Isa_Reflexive_or_Trivial =
123 reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
124 | get_isa_thm mth Isa_Lambda_Lifted =
125 lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
126 | get_isa_thm _ (Isa_Raw ith) =
127 ith |> lam_trans = lam_liftingN
128 ? introduce_lambda_wrappers_in_theorem ctxt
129 val axioms = axioms0 |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
130 val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
131 val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
132 val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
133 val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
134 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
136 case filter (fn t => prop_of t aconv @{prop False}) cls of
137 false_th :: _ => [false_th RS @{thm FalseE}]
139 case Metis_Resolution.new resolution_params
140 {axioms = axioms |> map fst, conjecture = []}
141 |> Metis_Resolution.loop of
142 Metis_Resolution.Contradiction mth =>
143 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
144 Metis_Thm.toString mth)
145 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
146 (*add constraints arising from converting goal to clause form*)
147 val proof = Metis_Proof.proof mth
150 |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
152 proof |> map_filter (used_axioms axioms0)
153 |> map_filter (fn Isa_Raw ith => SOME ith | _ => NONE)
154 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
155 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
156 val names = th_cls_pairs |> map fst
159 |> map_filter (fn (name, (_, cls)) =>
160 if have_common_thm used cls then SOME name
162 val unused_names = names |> subtract (op =) used_names
164 if not (null cls) andalso not (have_common_thm used cls) then
165 verbose_warning ctxt "The assumptions are inconsistent"
168 if not (null unused_names) then
169 "Unused theorems: " ^ commas_quote unused_names
170 |> verbose_warning ctxt
175 (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
176 [discharge_skolem_premises ctxt dischargers ith])
177 | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
179 | Metis_Resolution.Satisfiable _ =>
180 (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
181 if null fallback_type_encs then
184 raise METIS ("FOL_SOLVE",
185 "No first-order proof with the lemmas supplied");
188 handle METIS (loc, msg) =>
189 case fallback_type_encs of
190 [] => error ("Failed to replay Metis proof in Isabelle." ^
191 (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
193 | first_fallback :: _ =>
194 (verbose_warning ctxt
195 ("Falling back on " ^
196 quote (metis_call first_fallback lam_trans) ^ "...");
197 FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
199 fun neg_clausify ctxt combinators =
201 #> Meson.make_clauses_unsorted ctxt
202 #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
205 fun preskolem_tac ctxt st0 =
206 (if exists (Meson.has_too_many_clauses ctxt)
207 (Logic.prems_of_goal (prop_of st0) 1) then
208 Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
209 THEN cnf.cnfx_rewrite_tac ctxt 1
213 val type_has_top_sort =
214 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
216 fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
218 val _ = trace_msg ctxt (fn () =>
219 "Metis called with theorems\n" ^
220 cat_lines (map (Display.string_of_thm ctxt) ths))
221 val type_encs = type_encs |> maps unalias_type_enc
223 resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
225 if exists_type type_has_top_sort (prop_of st0) then
226 verbose_warning ctxt "Proof state contains the universal sort {}"
229 Meson.MESON (preskolem_tac ctxt)
230 (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
233 fun metis_tac [] = generic_metis_tac partial_type_encs
234 | metis_tac type_encs = generic_metis_tac type_encs
236 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
237 "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
238 We don't do it for nonschematic facts "X" because this breaks a few proofs
239 (in the rare and subtle case where a proof relied on extensionality not being
240 applied) and brings few benefits. *)
242 exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
244 fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts =
247 if default_type_encs = full_type_encs then
248 legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
251 val (schem_facts, nonschem_facts) = List.partition has_tvar facts
252 val type_encs = override_type_encs |> the_default default_type_encs
253 val lam_trans = lam_trans |> the_default metis_default_lam_trans
255 HEADGOAL (Method.insert_tac nonschem_facts THEN'
256 CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt
260 val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
263 if member (op =) metis_lam_transs s then apsnd (K (SOME s))
264 else apfst (K (SOME [s]))
266 val parse_metis_options =
268 (Args.parens (Parse.short_ident
269 -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
271 (NONE, NONE) |> consider_opt s
272 |> (case s' of SOME s' => consider_opt s' | _ => I)))
275 fun setup_method (binding, type_encs) =
276 Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs)
277 |> Method.setup binding
280 [((@{binding metis}, partial_type_encs),
281 "Metis for FOL and HOL problems"),
282 ((@{binding metisFT}, full_type_encs),
283 "Metis for FOL/HOL problems with fully-typed translation")]
284 |> fold (uncurry setup_method)