--- 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