--- a/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:35 2011 +0200
@@ -24,24 +24,24 @@
lemma "inc \<noteq> (\<lambda>y. 0)"
sledgehammer [expect = some] (inc_def plus_1_not_0)
-by (metis_eXhaust inc_def plus_1_not_0)
+by (new_metis_exhaust inc_def plus_1_not_0)
lemma "inc = (\<lambda>y. y + 1)"
sledgehammer [expect = some] (inc_def)
-by (metis_eXhaust inc_def)
+by (new_metis_exhaust inc_def)
definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"add_swap = (\<lambda>x y. y + x)"
lemma "add_swap m n = n + m"
sledgehammer [expect = some] (add_swap_def)
-by (metis_eXhaust add_swap_def)
+by (new_metis_exhaust add_swap_def)
definition "A = {xs\<Colon>'a list. True}"
lemma "xs \<in> A"
sledgehammer [expect = some]
-by (metis_eXhaust A_def Collect_def mem_def)
+by (new_metis_exhaust A_def Collect_def mem_def)
definition "B (y::int) \<equiv> y \<le> 0"
definition "C (y::int) \<equiv> y \<le> 1"
@@ -51,7 +51,7 @@
lemma "B \<subseteq> C"
sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
-by (metis_eXhaust B_def C_def int_le_0_imp_le_1 predicate1I)
+by (new_metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
text {* Proxies for logical constants *}
@@ -78,7 +78,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "\<not> id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -90,7 +90,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "x = id True \<or> x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -102,7 +102,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id x = id True \<or> id x = id False"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -114,7 +114,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
sledgehammer [type_sys = erased, expect = none] ()
@@ -139,7 +139,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -151,7 +151,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -163,7 +163,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -175,7 +175,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -187,7 +187,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -199,7 +199,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -211,7 +211,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -223,7 +223,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -235,7 +235,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -247,7 +247,7 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -259,6 +259,6 @@
sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metis_eXhaust id_apply)
+by (new_metis_exhaust id_apply)
end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:35 2011 +0200
@@ -40,47 +40,47 @@
constr (poly, level, heaviness))
[Preds, Tags])
-fun metis_eXhaust_tac ctxt ths =
+fun new_metis_exhaust_tac ctxt ths =
let
fun tac [] st = all_tac st
| tac (type_sys :: type_syss) st =
st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
|> ((if null type_syss then all_tac else rtac @{thm fork} 1)
- THEN Metis_Tactics.metisX_tac ctxt (SOME type_sys) ths 1
+ THEN Metis_Tactics.new_metis_tac [type_sys] ctxt ths 1
THEN COND (has_fewer_prems 2) all_tac no_tac
THEN tac type_syss)
in tac end
*}
-method_setup metis_eXhaust = {*
+method_setup new_metis_exhaust = {*
Attrib.thms >>
- (fn ths => fn ctxt => SIMPLE_METHOD (metis_eXhaust_tac ctxt ths type_syss))
+ (fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss))
*} "exhaustively run the new Metis with all type encodings"
text {* Miscellaneous tests *}
lemma "x = y \<Longrightarrow> y = x"
-by metis_eXhaust
+by new_metis_exhaust
lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (metis_eXhaust last.simps)
+by (new_metis_exhaust last.simps)
lemma "map Suc [0] = [Suc 0]"
-by (metis_eXhaust map.simps)
+by (new_metis_exhaust map.simps)
lemma "map Suc [1 + 1] = [Suc 2]"
-by (metis_eXhaust map.simps nat_1_add_1)
+by (new_metis_exhaust map.simps nat_1_add_1)
lemma "map Suc [2] = [Suc (1 + 1)]"
-by (metis_eXhaust map.simps nat_1_add_1)
+by (new_metis_exhaust map.simps nat_1_add_1)
definition "null xs = (xs = [])"
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
-by (metis_eXhaust null_def)
+by (new_metis_exhaust null_def)
lemma "(0::nat) + 0 = 0"
-by (metis_eXhaust arithmetic_simps(38))
+by (new_metis_exhaust arithmetic_simps(38))
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:35 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_Tactics.new_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 Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:35 2011 +0200
@@ -542,9 +542,9 @@
else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metisFT" then
- Metis_Tactics.metisFT_tac
+ Metis_Tactics.old_metisFT_tac
else
- Metis_Tactics.metis_tac) ctxt thms
+ Metis_Tactics.old_metis_tac) ctxt thms
fun apply_reconstructor thms =
Mirabelle.can_apply timeout (do_reconstructor thms) st
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200
@@ -230,7 +230,8 @@
fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
| hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
| hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
- | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
+ | hol_term_from_metis ctxt (Type_Sys _) sym_tab =
+ hol_term_from_metis_MX ctxt sym_tab
fun atp_literal_from_metis (pos, atom) =
atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
@@ -514,10 +515,10 @@
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
- fun path_finder_fail mode tm ps t =
+ fun path_finder_fail tm ps t =
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
- "equality_inference, path_finder_" ^ string_of_mode mode ^
- ": path = " ^ space_implode " " (map string_of_int ps) ^
+ "equality_inference, path_finder: path = " ^
+ space_implode " " (map string_of_int ps) ^
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
(case t of
SOME t => " fol-term: " ^ Metis_Term.toString t
@@ -542,7 +543,7 @@
fun path_finder_HO tm [] = (tm, Bound 0)
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
| path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
- | path_finder_HO tm ps = path_finder_fail HO tm ps NONE
+ | path_finder_HO tm ps = path_finder_fail tm ps NONE
fun path_finder_FT tm [] _ = (tm, Bound 0)
| path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) =
path_finder_FT tm ps t1
@@ -550,7 +551,7 @@
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
| path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
- | path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t)
+ | path_finder_FT tm ps t = path_finder_fail tm ps (SOME t)
fun path_finder_MX tm [] _ = (tm, Bound 0)
| path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
let
@@ -575,16 +576,16 @@
val (tm1, args) = strip_comb tm
val adjustment = length ts - length args
val p' = if adjustment > p then p else p - adjustment
- val tm_p = nth args p'
- handle Subscript =>
- path_finder_fail MX tm (p :: ps) (SOME t)
+ val tm_p =
+ nth args p'
+ handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
val _ = trace_msg ctxt (fn () =>
"path_finder: " ^ string_of_int p ^ " " ^
Syntax.string_of_term ctxt tm_p)
val (r, t) = path_finder_MX tm_p ps (nth ts p)
in (r, list_comb (tm1, replace_item_list t p' args)) end
end
- | path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME t)
+ | path_finder_MX tm ps t = path_finder_fail tm ps (SOME t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
| path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
@@ -604,7 +605,7 @@
| path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
(*if not equality, ignore head to skip the hBOOL predicate*)
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
- | path_finder MX tm ps t = path_finder_MX tm ps t
+ | path_finder (Type_Sys _) tm ps t = path_finder_MX tm ps t
val (tm_subst, body) = path_finder mode i_atom fp m_tm
val tm_abs = Abs ("x", type_of tm_subst, body)
val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200
@@ -9,18 +9,17 @@
signature METIS_TACTICS =
sig
- type type_sys = ATP_Translate.type_sys
-
val metisN : string
val metisFT_N : string
val trace : bool Config.T
val verbose : bool Config.T
val new_skolemizer : bool Config.T
- val metis_tac : Proof.context -> thm list -> int -> tactic
- val metisF_tac : Proof.context -> thm list -> int -> tactic
- val metisH_tac : Proof.context -> thm list -> int -> tactic
- val metisFT_tac : Proof.context -> thm list -> int -> tactic
- val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic
+ val old_metis_tac : Proof.context -> thm list -> int -> tactic
+ val old_metisF_tac : Proof.context -> thm list -> int -> tactic
+ val old_metisH_tac : Proof.context -> thm list -> int -> tactic
+ val old_metisFT_tac : Proof.context -> thm list -> int -> tactic
+ val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic
+ val new_metisFT_tac : Proof.context -> thm list -> int -> tactic
val setup : theory -> theory
end
@@ -31,15 +30,22 @@
open Metis_Translate
open Metis_Reconstruct
-fun method_binding_for_mode HO = @{binding metis}
- | method_binding_for_mode FO = @{binding metisF}
- | method_binding_for_mode FT = @{binding metisFT}
- | method_binding_for_mode MX = @{binding metisX}
+val full_typesN = "full_types"
+val default_unsound_type_sys = "poly_args"
+val default_sound_type_sys = "poly_preds_query"
-val metisN = Binding.qualified_name_of (method_binding_for_mode HO)
-val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO)
-val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
-val metisX_N = Binding.qualified_name_of (method_binding_for_mode MX)
+fun method_call_for_mode HO = (@{binding metis}, "")
+ | method_call_for_mode FO = (@{binding metisF}, "")
+ | method_call_for_mode FT = (@{binding metisFT}, "")
+ | method_call_for_mode (Type_Sys type_sys) =
+ if type_sys = default_sound_type_sys then
+ (@{binding new_metisFT}, "")
+ else
+ (@{binding new_metis},
+ if type_sys = default_unsound_type_sys then "" else type_sys)
+
+val metisN = Binding.qualified_name_of @{binding metis}
+val metisFT_N = Binding.qualified_name_of @{binding metisFT}
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -85,7 +91,7 @@
val resolution_params = {active = active_params, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE type_sys (mode :: fallback_modes) ctxt cls ths0 =
+fun FOL_SOLVE (mode :: fallback_modes) 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)
@@ -101,7 +107,7 @@
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
val (mode, sym_tab, {axioms, old_skolems, ...}) =
- prepare_metis_problem ctxt mode type_sys cls ths
+ prepare_metis_problem ctxt mode cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
| get_isa_thm _ (Isa_Raw ith) = ith
@@ -167,11 +173,13 @@
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
else ""))
| mode :: _ =>
- (verbose_warning ctxt
- ("Falling back on " ^
- quote (Binding.qualified_name_of
- (method_binding_for_mode mode)) ^ "...");
- FOL_SOLVE type_sys fallback_modes ctxt cls ths0)
+ let val (binding, arg) = method_call_for_mode mode in
+ (verbose_warning ctxt
+ ("Falling back on " ^
+ quote (Binding.qualified_name_of binding ^
+ (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
+ FOL_SOLVE fallback_modes ctxt cls ths0)
+ end
val neg_clausify =
single
@@ -190,12 +198,12 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-fun generic_metis_tac modes type_sys ctxt ths i st0 =
+fun generic_metis_tac modes 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_sys modes ctxt clause ths) 1
+ fun tac clause = resolve_tac (FOL_SOLVE modes 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 {}";
@@ -204,17 +212,21 @@
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
end
-val metis_modes = [HO, FT]
-val metisF_modes = [FO, FT]
-val metisH_modes = [HO]
-val metisFT_modes = [FT]
-val metisX_modes = [MX]
+val old_metis_modes = [HO, FT]
+val old_metisF_modes = [FO, FT]
+val old_metisH_modes = [HO]
+val old_metisFT_modes = [FT]
+val new_metis_default_modes =
+ map Type_Sys [default_unsound_type_sys, default_sound_type_sys]
+val new_metisFT_modes = [Type_Sys default_sound_type_sys]
-val metis_tac = generic_metis_tac metis_modes NONE
-val metisF_tac = generic_metis_tac metisF_modes NONE
-val metisH_tac = generic_metis_tac metisH_modes NONE
-val metisFT_tac = generic_metis_tac metisFT_modes NONE
-fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt
+val old_metis_tac = generic_metis_tac old_metis_modes
+val old_metisF_tac = generic_metis_tac old_metisF_modes
+val old_metisH_tac = generic_metis_tac old_metisH_modes
+val old_metisFT_tac = generic_metis_tac old_metisFT_modes
+fun new_metis_tac [] = generic_metis_tac new_metis_default_modes
+ | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss)
+val new_metisFT_tac = generic_metis_tac new_metisFT_modes
(* 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.
@@ -227,26 +239,30 @@
fun method modes (type_sys, ths) ctxt facts =
let
val (schem_facts, nonschem_facts) = List.partition has_tvar facts
- val type_sys = type_sys |> Option.map type_sys_from_string
+ val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes
in
HEADGOAL (Method.insert_tac nonschem_facts THEN'
- CHANGED_PROP
- o generic_metis_tac modes type_sys ctxt (schem_facts @ ths))
+ CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths))
end
fun setup_method (modes as mode :: _) =
- Method.setup (method_binding_for_mode mode)
- ((if mode = MX then
- Scan.lift (Scan.option (Args.parens Parse.short_ident))
- else
- Scan.succeed NONE)
- -- Attrib.thms >> (METHOD oo method modes))
+ (if modes = new_metis_default_modes then
+ (Args.parens Parse.short_ident
+ >> (fn s => if s = full_typesN then default_sound_type_sys else s))
+ |> Scan.option |> Scan.lift
+ else
+ Scan.succeed NONE)
+ -- Attrib.thms >> (METHOD oo method modes)
+ |> Method.setup (fst (method_call_for_mode mode))
val setup =
- [(metis_modes, "Metis for FOL and HOL problems"),
- (metisF_modes, "Metis for FOL problems"),
- (metisFT_modes, "Metis for FOL/HOL problems with fully-typed translation"),
- (metisX_modes, "Metis for FOL and HOL problems (experimental)")]
+ [(old_metis_modes, "Metis for FOL and HOL problems"),
+ (old_metisF_modes, "Metis for FOL problems (legacy)"),
+ (old_metisFT_modes,
+ "Metis for FOL/HOL problems with fully-typed translation"),
+ (new_metis_default_modes, "Metis for FOL and HOL problems (experimental)"),
+ (new_metisFT_modes,
+ "Metis for FOL/HOL problems with fully-typed translation (experimental)")]
|> fold (uncurry setup_method)
end;
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200
@@ -10,9 +10,8 @@
signature METIS_TRANSLATE =
sig
type type_literal = ATP_Translate.type_literal
- type type_sys = ATP_Translate.type_sys
- datatype mode = FO | HO | FT | MX
+ datatype mode = FO | HO | FT | Type_Sys of string
datatype isa_thm =
Isa_Reflexive_or_Trivial |
@@ -32,7 +31,7 @@
val reveal_old_skolem_terms : (string * term) list -> term -> term
val string_of_mode : mode -> string
val prepare_metis_problem :
- Proof.context -> mode -> type_sys option -> thm list -> thm list
+ Proof.context -> mode -> thm list -> thm list
-> mode * int Symtab.table * metis_problem
end
@@ -118,13 +117,13 @@
(* HOL to FOL (Isabelle to Metis) *)
(* ------------------------------------------------------------------------- *)
-(* first-order, higher-order, fully-typed, mode X (fleXible) *)
-datatype mode = FO | HO | FT | MX
+(* first-order, higher-order, fully-typed, ATP type system *)
+datatype mode = FO | HO | FT | Type_Sys of string
fun string_of_mode FO = "FO"
| string_of_mode HO = "HO"
| string_of_mode FT = "FT"
- | string_of_mode MX = "MX"
+ | string_of_mode (Type_Sys type_sys) = "Type_Sys " ^ type_sys
fun fn_isa_to_met_sublevel "equal" = "c_fequal"
| fn_isa_to_met_sublevel "c_False" = "c_fFalse"
@@ -346,13 +345,11 @@
end
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
-(* FIXME: put in "Metis_Tactics" as string *)
-val default_type_sys = Preds (Polymorphic, Const_Arg_Types, Lightweight)
-
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt (mode as Type_Sys type_sys) conj_clauses
+ fact_clauses =
let
- val type_sys = type_sys |> the_default default_type_sys
+ val type_sys = type_sys_from_string type_sys
val explicit_apply = NONE
val clauses =
conj_clauses @ fact_clauses
@@ -382,9 +379,9 @@
val axioms =
atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
in
- (MX, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
+ (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
end
- | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses =
+ | prepare_metis_problem ctxt mode conj_clauses fact_clauses =
let
val thy = Proof_Context.theory_of ctxt
(* The modes FO and FT are sticky. HO can be downgraded to FO. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:35 2011 +0200
@@ -416,8 +416,8 @@
val full_tac = Method.insert_tac facts i THEN tac ctxt i
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
-fun tac_for_reconstructor Metis = Metis_Tactics.metisH_tac
- | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
+fun tac_for_reconstructor Metis = Metis_Tactics.old_metisH_tac
+ | tac_for_reconstructor MetisFT = Metis_Tactics.old_metisFT_tac
| tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
fun timed_reconstructor reconstructor debug timeout ths =
--- a/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:36:35 2011 +0200
@@ -51,7 +51,8 @@
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
+ SOLVE_TIMEOUT (max_secs div 10) "metis"
+ (ALLGOALS (Metis_Tactics.new_metis_tac ctxt NONE []))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
ORELSE
--- a/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:36:35 2011 +0200
@@ -70,7 +70,7 @@
in
case run_atp false timeout i i ctxt th atp of
SOME facts =>
- Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+ Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
| NONE => Seq.empty
end