renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
--- a/src/HOL/IsaMakefile Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 02 14:43:20 2011 +0200
@@ -234,7 +234,7 @@
Tools/Meson/meson_clausify.ML \
Tools/Meson/meson_tactic.ML \
Tools/Metis/metis_reconstruct.ML \
- Tools/Metis/metis_tactics.ML \
+ Tools/Metis/metis_tactic.ML \
Tools/Metis/metis_translate.ML \
Tools/abel_cancel.ML \
Tools/arith_data.ML \
--- a/src/HOL/Metis.thy Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Metis.thy Fri Sep 02 14:43:20 2011 +0200
@@ -11,7 +11,7 @@
uses "~~/src/Tools/Metis/metis.ML"
("Tools/Metis/metis_translate.ML")
("Tools/Metis/metis_reconstruct.ML")
- ("Tools/Metis/metis_tactics.ML")
+ ("Tools/Metis/metis_tactic.ML")
("Tools/try_methods.ML")
begin
@@ -36,9 +36,9 @@
use "Tools/Metis/metis_translate.ML"
use "Tools/Metis/metis_reconstruct.ML"
-use "Tools/Metis/metis_tactics.ML"
+use "Tools/Metis/metis_tactic.ML"
-setup {* Metis_Tactics.setup *}
+setup {* Metis_Tactic.setup *}
hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Sep 02 14:43:20 2011 +0200
@@ -70,7 +70,7 @@
| tac (type_enc :: type_encs) st =
st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
|> ((if null type_encs then all_tac else rtac @{thm fork} 1)
- THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1
+ THEN Metis_Tactic.metis_tac [type_enc] ctxt ths 1
THEN COND (has_fewer_prems 2) all_tac no_tac
THEN tac type_encs)
in tac end
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 02 14:43:20 2011 +0200
@@ -18,7 +18,7 @@
val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
- fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts)
+ fun metis ctxt = Metis_Tactic.metis_tac [] ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
|> prefix (metis_tag id)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 02 14:43:20 2011 +0200
@@ -577,15 +577,15 @@
sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
- ORELSE' Metis_Tactics.metis_tac [] ctxt thms
+ ORELSE' Metis_Tactic.metis_tac [] ctxt thms
else if !reconstructor = "smt" then
SMT_Solver.smt_tac ctxt thms
else if full orelse !reconstructor = "metis (full_types)" then
- Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms
+ Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms
else if !reconstructor = "metis (no_types)" then
- Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms
+ Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms
else if !reconstructor = "metis" then
- Metis_Tactics.metis_tac [] ctxt thms
+ Metis_Tactic.metis_tac [] ctxt thms
else
K all_tac
end
--- a/src/HOL/TPTP/CASC_Setup.thy Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/TPTP/CASC_Setup.thy Fri Sep 02 14:43:20 2011 +0200
@@ -131,7 +131,7 @@
Sledgehammer_Filter.no_relevance_override))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis"
- (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
+ (ALLGOALS (Metis_Tactic.metis_tac [] ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
ORELSE
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 02 14:43:20 2011 +0200
@@ -0,0 +1,268 @@
+(* Title: HOL/Tools/Metis/metis_tactic.ML
+ Author: Kong W. Susanto, Cambridge University Computer Laboratory
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright Cambridge University 2007
+
+HOL setup for the Metis prover.
+*)
+
+signature METIS_TACTIC =
+sig
+ val metisN : string
+ val full_typesN : string
+ val partial_typesN : string
+ val no_typesN : string
+ val really_full_type_enc : string
+ val full_type_enc : string
+ val partial_type_enc : string
+ val no_type_enc : string
+ val full_type_syss : string list
+ val partial_type_syss : string list
+ val trace : bool Config.T
+ val verbose : bool Config.T
+ val new_skolemizer : bool Config.T
+ val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
+ val setup : theory -> theory
+end
+
+structure Metis_Tactic : METIS_TACTIC =
+struct
+
+open ATP_Translate
+open Metis_Translate
+open Metis_Reconstruct
+
+val metisN = "metis"
+
+val full_typesN = "full_types"
+val partial_typesN = "partial_types"
+val no_typesN = "no_types"
+
+val really_full_type_enc = "mono_tags_uniform"
+val full_type_enc = "poly_guards_uniform_query"
+val partial_type_enc = "poly_args"
+val no_type_enc = "erased"
+
+val full_type_syss = [full_type_enc, really_full_type_enc]
+val partial_type_syss = partial_type_enc :: full_type_syss
+
+val type_enc_aliases =
+ [(full_typesN, full_type_syss),
+ (partial_typesN, partial_type_syss),
+ (no_typesN, [no_type_enc])]
+
+fun method_call_for_type_enc type_syss =
+ metisN ^ " (" ^
+ (case AList.find (op =) type_enc_aliases type_syss of
+ [alias] => alias
+ | _ => hd type_syss) ^ ")"
+
+val new_skolemizer =
+ Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
+
+(* Designed to work also with monomorphic instances of polymorphic theorems. *)
+fun have_common_thm ths1 ths2 =
+ exists (member (Term.aconv_untyped o pairself prop_of) ths1)
+ (map Meson.make_meta_clause ths2)
+
+(*Determining which axiom clauses are actually used*)
+fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
+ | used_axioms _ _ = NONE
+
+(* Lightweight predicate type information comes in two flavors, "t = t'" and
+ "t => t'", where "t" and "t'" are the same term modulo type tags.
+ In Isabelle, type tags are stripped away, so we are left with "t = t" or
+ "t => t". Type tag idempotence is also handled this way. *)
+fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
+ let val thy = Proof_Context.theory_of ctxt in
+ case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
+ Const (@{const_name HOL.eq}, _) $ _ $ t =>
+ let
+ val ct = cterm_of thy t
+ val cT = ctyp_of_term ct
+ in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
+ | Const (@{const_name disj}, _) $ t1 $ t2 =>
+ (if can HOLogic.dest_not t1 then t2 else t1)
+ |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
+ | _ => raise Fail "unexpected tags sym clause"
+ end
+ |> Meson.make_meta_clause
+
+val clause_params =
+ {ordering = Metis_KnuthBendixOrder.default,
+ orderLiterals = Metis_Clause.UnsignedLiteralOrder,
+ orderTerms = true}
+val active_params =
+ {clause = clause_params,
+ prefactor = #prefactor Metis_Active.default,
+ postfactor = #postfactor Metis_Active.default}
+val waiting_params =
+ {symbolsWeight = 1.0,
+ variablesWeight = 0.0,
+ literalsWeight = 0.0,
+ models = []}
+val resolution_params = {active = active_params, waiting = waiting_params}
+
+(* Main function to start Metis proof and reconstruction *)
+fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
+ let val thy = Proof_Context.theory_of ctxt
+ val new_skolemizer =
+ Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
+ val th_cls_pairs =
+ map2 (fn j => fn th =>
+ (Thm.get_name_hint th,
+ Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
+ (0 upto length ths0 - 1) ths0
+ val ths = maps (snd o snd) th_cls_pairs
+ val dischargers = map (fst o snd) th_cls_pairs
+ val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
+ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
+ val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
+ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
+ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
+ val type_enc = type_enc_from_string Sound type_enc
+ val (sym_tab, axioms, old_skolems) =
+ prepare_metis_problem ctxt type_enc cls ths
+ fun get_isa_thm mth Isa_Reflexive_or_Trivial =
+ reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems 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 () => "CLAUSES GIVEN TO METIS")
+ val thms = axioms |> map fst
+ val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
+ val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
+ 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
+ {axioms = thms, 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 old_skolems sym_tab) proof
+ val used = map_filter (used_axioms axioms) proof
+ 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 lemmas supplied");
+ if null fallback_type_syss then
+ ()
+ else
+ raise METIS ("FOL_SOLVE",
+ "No first-order proof with the lemmas supplied");
+ [])
+ end
+ handle METIS (loc, msg) =>
+ case fallback_type_syss of
+ [] => error ("Failed to replay Metis proof in Isabelle." ^
+ (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
+ else ""))
+ | _ =>
+ (verbose_warning ctxt
+ ("Falling back on " ^
+ quote (method_call_for_type_enc fallback_type_syss) ^ "...");
+ FOL_SOLVE fallback_type_syss ctxt cls ths0)
+
+fun neg_clausify ctxt =
+ single
+ #> Meson.make_clauses_unsorted ctxt
+ #> map Meson_Clausify.introduce_combinators_in_theorem
+ #> Meson.finish_cnf
+
+fun preskolem_tac ctxt st0 =
+ (if exists (Meson.has_too_many_clauses ctxt)
+ (Logic.prems_of_goal (prop_of st0) 1) then
+ Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
+ THEN cnf.cnfx_rewrite_tac ctxt 1
+ else
+ all_tac) st0
+
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
+fun generic_metis_tac type_syss ctxt ths i st0 =
+ let
+ val _ = trace_msg ctxt (fn () =>
+ "Metis called with theorems\n" ^
+ cat_lines (map (Display.string_of_thm ctxt) ths))
+ fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
+ in
+ if exists_type type_has_top_sort (prop_of st0) then
+ verbose_warning ctxt "Proof state contains the universal sort {}"
+ else
+ ();
+ Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
+ end
+
+fun metis_tac [] = generic_metis_tac partial_type_syss
+ | metis_tac type_syss = generic_metis_tac type_syss
+
+(* 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 extensionality not being
+ applied) and brings few benefits. *)
+val has_tvar =
+ exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
+
+fun method default_type_syss (override_type_syss, ths) ctxt facts =
+ let
+ val _ =
+ if default_type_syss = full_type_syss then
+ legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
+ else
+ ()
+ val (schem_facts, nonschem_facts) = List.partition has_tvar facts
+ val type_syss = override_type_syss |> the_default default_type_syss
+ in
+ HEADGOAL (Method.insert_tac nonschem_facts THEN'
+ CHANGED_PROP
+ o generic_metis_tac type_syss ctxt (schem_facts @ ths))
+ end
+
+fun setup_method (binding, type_syss) =
+ ((Args.parens (Scan.repeat Parse.short_ident)
+ >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
+ |> Scan.option |> Scan.lift)
+ -- Attrib.thms >> (METHOD oo method type_syss)
+ |> Method.setup binding
+
+val setup =
+ [((@{binding metis}, partial_type_syss),
+ "Metis for FOL and HOL problems"),
+ ((@{binding metisFT}, full_type_syss),
+ "Metis for FOL/HOL problems with fully-typed translation")]
+ |> fold (uncurry setup_method)
+
+end;
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Sep 02 14:43:20 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,268 +0,0 @@
-(* Title: HOL/Tools/Metis/metis_tactics.ML
- Author: Kong W. Susanto, Cambridge University Computer Laboratory
- Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
- Copyright Cambridge University 2007
-
-HOL setup for the Metis prover.
-*)
-
-signature METIS_TACTICS =
-sig
- val metisN : string
- val full_typesN : string
- val partial_typesN : string
- val no_typesN : string
- val really_full_type_enc : string
- val full_type_enc : string
- val partial_type_enc : string
- val no_type_enc : string
- val full_type_syss : string list
- val partial_type_syss : string list
- val trace : bool Config.T
- val verbose : bool Config.T
- val new_skolemizer : bool Config.T
- val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
- val setup : theory -> theory
-end
-
-structure Metis_Tactics : METIS_TACTICS =
-struct
-
-open ATP_Translate
-open Metis_Translate
-open Metis_Reconstruct
-
-val metisN = "metis"
-
-val full_typesN = "full_types"
-val partial_typesN = "partial_types"
-val no_typesN = "no_types"
-
-val really_full_type_enc = "mono_tags_uniform"
-val full_type_enc = "poly_guards_uniform_query"
-val partial_type_enc = "poly_args"
-val no_type_enc = "erased"
-
-val full_type_syss = [full_type_enc, really_full_type_enc]
-val partial_type_syss = partial_type_enc :: full_type_syss
-
-val type_enc_aliases =
- [(full_typesN, full_type_syss),
- (partial_typesN, partial_type_syss),
- (no_typesN, [no_type_enc])]
-
-fun method_call_for_type_enc type_syss =
- metisN ^ " (" ^
- (case AList.find (op =) type_enc_aliases type_syss of
- [alias] => alias
- | _ => hd type_syss) ^ ")"
-
-val new_skolemizer =
- Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
-
-(* Designed to work also with monomorphic instances of polymorphic theorems. *)
-fun have_common_thm ths1 ths2 =
- exists (member (Term.aconv_untyped o pairself prop_of) ths1)
- (map Meson.make_meta_clause ths2)
-
-(*Determining which axiom clauses are actually used*)
-fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
- | used_axioms _ _ = NONE
-
-(* Lightweight predicate type information comes in two flavors, "t = t'" and
- "t => t'", where "t" and "t'" are the same term modulo type tags.
- In Isabelle, type tags are stripped away, so we are left with "t = t" or
- "t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
- let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
- Const (@{const_name HOL.eq}, _) $ _ $ t =>
- let
- val ct = cterm_of thy t
- val cT = ctyp_of_term ct
- in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
- | Const (@{const_name disj}, _) $ t1 $ t2 =>
- (if can HOLogic.dest_not t1 then t2 else t1)
- |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
- | _ => raise Fail "unexpected tags sym clause"
- end
- |> Meson.make_meta_clause
-
-val clause_params =
- {ordering = Metis_KnuthBendixOrder.default,
- orderLiterals = Metis_Clause.UnsignedLiteralOrder,
- orderTerms = true}
-val active_params =
- {clause = clause_params,
- prefactor = #prefactor Metis_Active.default,
- postfactor = #postfactor Metis_Active.default}
-val waiting_params =
- {symbolsWeight = 1.0,
- variablesWeight = 0.0,
- literalsWeight = 0.0,
- models = []}
-val resolution_params = {active = active_params, waiting = waiting_params}
-
-(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
- let val thy = Proof_Context.theory_of ctxt
- val new_skolemizer =
- Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
- val th_cls_pairs =
- map2 (fn j => fn th =>
- (Thm.get_name_hint th,
- Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
- (0 upto length ths0 - 1) ths0
- val ths = maps (snd o snd) th_cls_pairs
- val dischargers = map (fst o snd) th_cls_pairs
- val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
- val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
- val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
- val type_enc = type_enc_from_string Sound type_enc
- val (sym_tab, axioms, old_skolems) =
- prepare_metis_problem ctxt type_enc cls ths
- fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems 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 () => "CLAUSES GIVEN TO METIS")
- val thms = axioms |> map fst
- val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
- val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
- 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
- {axioms = thms, 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 old_skolems sym_tab) proof
- val used = map_filter (used_axioms axioms) proof
- 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 lemmas supplied");
- if null fallback_type_syss then
- ()
- else
- raise METIS ("FOL_SOLVE",
- "No first-order proof with the lemmas supplied");
- [])
- end
- handle METIS (loc, msg) =>
- case fallback_type_syss of
- [] => error ("Failed to replay Metis proof in Isabelle." ^
- (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
- else ""))
- | _ =>
- (verbose_warning ctxt
- ("Falling back on " ^
- quote (method_call_for_type_enc fallback_type_syss) ^ "...");
- FOL_SOLVE fallback_type_syss ctxt cls ths0)
-
-fun neg_clausify ctxt =
- single
- #> Meson.make_clauses_unsorted ctxt
- #> map Meson_Clausify.introduce_combinators_in_theorem
- #> Meson.finish_cnf
-
-fun preskolem_tac ctxt st0 =
- (if exists (Meson.has_too_many_clauses ctxt)
- (Logic.prems_of_goal (prop_of st0) 1) then
- Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
- THEN cnf.cnfx_rewrite_tac ctxt 1
- else
- all_tac) st0
-
-val type_has_top_sort =
- exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
-fun generic_metis_tac type_syss ctxt ths i st0 =
- let
- val _ = trace_msg ctxt (fn () =>
- "Metis called with theorems\n" ^
- cat_lines (map (Display.string_of_thm ctxt) ths))
- fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
- in
- if exists_type type_has_top_sort (prop_of st0) then
- verbose_warning ctxt "Proof state contains the universal sort {}"
- else
- ();
- Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
- end
-
-fun metis_tac [] = generic_metis_tac partial_type_syss
- | metis_tac type_syss = generic_metis_tac type_syss
-
-(* 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 extensionality not being
- applied) and brings few benefits. *)
-val has_tvar =
- exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
-
-fun method default_type_syss (override_type_syss, ths) ctxt facts =
- let
- val _ =
- if default_type_syss = full_type_syss then
- legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
- else
- ()
- val (schem_facts, nonschem_facts) = List.partition has_tvar facts
- val type_syss = override_type_syss |> the_default default_type_syss
- in
- HEADGOAL (Method.insert_tac nonschem_facts THEN'
- CHANGED_PROP
- o generic_metis_tac type_syss ctxt (schem_facts @ ths))
- end
-
-fun setup_method (binding, type_syss) =
- ((Args.parens (Scan.repeat Parse.short_ident)
- >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
- |> Scan.option |> Scan.lift)
- -- Attrib.thms >> (METHOD oo method type_syss)
- |> Method.setup binding
-
-val setup =
- [((@{binding metis}, partial_type_syss),
- "Metis for FOL and HOL problems"),
- ((@{binding metisFT}, full_type_syss),
- "Metis for FOL/HOL problems with fully-typed translation")]
- |> fold (uncurry setup_method)
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 02 14:43:20 2011 +0200
@@ -299,7 +299,7 @@
(* Sledgehammer the given subgoal *)
-val default_minimize_prover = Metis_Tactics.metisN
+val default_minimize_prover = Metis_Tactic.metisN
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 02 14:43:20 2011 +0200
@@ -128,9 +128,9 @@
"Async_Manager". *)
val das_tool = "Sledgehammer"
-val metisN = Metis_Tactics.metisN
-val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
-val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
+val metisN = Metis_Tactic.metisN
+val metis_full_typesN = metisN ^ "_" ^ Metis_Tactic.full_typesN
+val metis_no_typesN = metisN ^ "_" ^ Metis_Tactic.no_typesN
val metis_prover_infos =
[(metisN, Metis),
@@ -413,15 +413,15 @@
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
fun tac_for_reconstructor Metis =
- Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
+ Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc]
| tac_for_reconstructor Metis_Full_Types =
- Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
+ Metis_Tactic.metis_tac Metis_Tactic.full_type_syss
| tac_for_reconstructor Metis_No_Types =
- Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
+ Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
| tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
fun timed_reconstructor reconstructor debug timeout ths =
- (Config.put Metis_Tactics.verbose debug
+ (Config.put Metis_Tactic.verbose debug
#> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))
|> timed_apply timeout
--- a/src/HOL/Tools/try_methods.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML Fri Sep 02 14:43:20 2011 +0200
@@ -113,7 +113,7 @@
fun do_try_methods mode timeout_opt quad st =
let
- val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false #>
+ val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
Config.put Lin_Arith.verbose false)
in
if mode = Normal then
--- a/src/HOL/ex/sledgehammer_tactics.ML Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Fri Sep 02 14:43:20 2011 +0200
@@ -71,7 +71,7 @@
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
case run_atp override_params relevance_override i i ctxt th of
SOME facts =>
- Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
+ Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
| NONE => Seq.empty
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =