# HG changeset patch # User blanchet # Date 1392572773 -3600 # Node ID 241c6a2fdda135f88e5b76872e014a583d64c9ee # Parent f6fc6d5339f1df86ddd3cc534f980c4bae1c5589 added a version of the Metis tactic that returns the unused facts diff -r f6fc6d5339f1 -r 241c6a2fdda1 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Sun Feb 16 18:39:42 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Feb 16 18:46:13 2014 +0100 @@ -13,6 +13,8 @@ val verbose : bool Config.T val new_skolem : bool Config.T val advisory_simp : bool Config.T + val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm -> + thm list * thm Seq.seq val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic val metis_lam_transs : string list val parse_metis_options : (string list option * string option) parser @@ -143,7 +145,7 @@ exception METIS_UNPROVABLE of unit (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = +fun FOL_SOLVE unused (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) @@ -161,7 +163,7 @@ val ths = maps (snd o snd) th_cls_pairs val dischargers = map (fst o snd) th_cls_pairs val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) - val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_of_string Strict type_enc @@ -173,11 +175,11 @@ lam_lifted_of_metis ctxt type_enc sym_tab concealed mth | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) - val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES") + val _ = trace_msg ctxt (K "ISABELLE CLAUSES") val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms - val _ = trace_msg ctxt (fn () => "METIS CLAUSES") + val _ = trace_msg ctxt (K "METIS CLAUSES") val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms - val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") + val _ = trace_msg ctxt (K "START METIS PROVE PROCESS") val ordering = if Config.get ctxt advisory_simp then kbo_advisory_simp_ordering (ord_info ()) @@ -186,63 +188,52 @@ fun fall_back () = (verbose_warning ctxt ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "..."); - FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0) + FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0) in (case filter (fn t => prop_of t aconv @{prop False}) cls of - false_th :: _ => [false_th RS @{thm FalseE}] - | [] => - case Metis_Resolution.new (resolution_params ordering) - {axioms = axioms |> map fst, conjecture = []} - |> Metis_Resolution.loop of - Metis_Resolution.Contradiction mth => - let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ - Metis_Thm.toString mth) - val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt - (*add constraints arising from converting goal to clause form*) - val proof = Metis_Proof.proof mth - val result = - axioms - |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof - val used = proof |> map_filter (used_axioms axioms) - val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used - val names = th_cls_pairs |> map fst - val used_names = - th_cls_pairs - |> map_filter (fn (name, (_, cls)) => - if have_common_thm used cls then SOME name - else NONE) - val unused_names = names |> subtract (op =) used_names - in - if not (null cls) andalso not (have_common_thm used cls) then - verbose_warning ctxt "The assumptions are inconsistent" - else - (); - if not (null unused_names) then - "Unused theorems: " ^ commas_quote unused_names - |> verbose_warning ctxt - else - (); - case result of - (_,ith)::_ => - (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); - [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) - end - | Metis_Resolution.Satisfiable _ => - (trace_msg ctxt (fn () => - "Metis: No first-order proof with the supplied lemmas"); - raise METIS_UNPROVABLE ())) - handle METIS_UNPROVABLE () => - (case fallback_type_encs of - [] => [] - | _ => fall_back ()) + false_th :: _ => [false_th RS @{thm FalseE}] + | [] => + (case Metis_Resolution.loop (Metis_Resolution.new (resolution_params ordering) + {axioms = axioms |> map fst, conjecture = []}) of + Metis_Resolution.Contradiction mth => + let + val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) + val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt + (*add constraints arising from converting goal to clause form*) + val proof = Metis_Proof.proof mth + val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms + val used = map_filter (used_axioms axioms) proof + val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used + val (used_th_cls_pairs, unused_th_cls_pairs) = + List.partition (have_common_thm used o snd o snd) th_cls_pairs + val unused_ths = maps (snd o snd) unused_th_cls_pairs + val unused_names = map fst unused_th_cls_pairs + in + unused := unused_ths; + if not (null unused_names) then + verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names) + else + (); + if not (null cls) andalso not (have_common_thm used cls) then + verbose_warning ctxt "The assumptions are inconsistent" + else + (); + (case result of + (_, ith) :: _ => + (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + [discharge_skolem_premises ctxt dischargers ith]) + | _ => (trace_msg ctxt (K "Metis: No result"); [])) + end + | Metis_Resolution.Satisfiable _ => + (trace_msg ctxt (K "Metis: No first-order proof with the supplied lemmas"); + raise METIS_UNPROVABLE ())) + handle METIS_UNPROVABLE () => if null fallback_type_encs then [] else fall_back () | METIS_RECONSTRUCT (loc, msg) => - (case fallback_type_encs of - [] => - (verbose_warning ctxt - ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) - | _ => fall_back ()) + if null fallback_type_encs then + (verbose_warning ctxt ("Failed to replay Metis proof\n" ^ loc ^ ": " ^ msg); []) + else + fall_back ()) end fun neg_clausify ctxt combinators = @@ -259,17 +250,22 @@ else all_tac) st0 -fun metis_tac type_encs0 lam_trans ctxt ths i st0 = +fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 = let + val unused = Unsynchronized.ref [] val type_encs = if null type_encs0 then partial_type_encs else type_encs0 val _ = trace_msg ctxt (fn () => "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) val type_encs = type_encs |> maps unalias_type_enc - fun tac clause = resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1 + val combs = (lam_trans = combsN) + fun tac clause = resolve_tac (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1 + val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0 in - Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0 + (!unused, seq) end +fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i + (* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts "X" because this breaks a few proofs (in the rare and subtle case where a proof relied on