--- a/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:56:06 2011 +0200
@@ -24,24 +24,24 @@
lemma "inc \<noteq> (\<lambda>y. 0)"
sledgehammer [expect = some] (inc_def plus_1_not_0)
-by (new_metis_exhaust inc_def plus_1_not_0)
+by (metis_exhaust inc_def plus_1_not_0)
lemma "inc = (\<lambda>y. y + 1)"
sledgehammer [expect = some] (inc_def)
-by (new_metis_exhaust inc_def)
+by (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 (new_metis_exhaust add_swap_def)
+by (metis_exhaust add_swap_def)
definition "A = {xs\<Colon>'a list. True}"
lemma "xs \<in> A"
sledgehammer [expect = some]
-by (new_metis_exhaust A_def Collect_def mem_def)
+by (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 (new_metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (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 (new_metis_exhaust id_apply)
+by (metis_exhaust id_apply)
end
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:56:06 2011 +0200
@@ -69,47 +69,47 @@
"mangled_tags_heavy!",
"simple!"]
-fun new_metis_exhaust_tac ctxt ths =
+fun 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.new_metis_tac [type_sys] ctxt ths 1
+ THEN Metis_Tactics.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 new_metis_exhaust = {*
+method_setup metis_exhaust = {*
Attrib.thms >>
- (fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss))
+ (fn ths => fn ctxt => SIMPLE_METHOD (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 new_metis_exhaust
+by metis_exhaust
lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (new_metis_exhaust last.simps)
+by (metis_exhaust last.simps)
lemma "map Suc [0] = [Suc 0]"
-by (new_metis_exhaust map.simps)
+by (metis_exhaust map.simps)
lemma "map Suc [1 + 1] = [Suc 2]"
-by (new_metis_exhaust map.simps nat_1_add_1)
+by (metis_exhaust map.simps nat_1_add_1)
lemma "map Suc [2] = [Suc (1 + 1)]"
-by (new_metis_exhaust map.simps nat_1_add_1)
+by (metis_exhaust map.simps nat_1_add_1)
definition "null xs = (xs = [])"
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
-by (new_metis_exhaust null_def)
+by (metis_exhaust null_def)
lemma "(0::nat) + 0 = 0"
-by (new_metis_exhaust arithmetic_simps(38))
+by (metis_exhaust arithmetic_simps(38))
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:56:06 2011 +0200
@@ -18,7 +18,7 @@
val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
- fun metis ctxt = Metis_Tactics.new_metis_tac [] ctxt (thms @ facts)
+ fun metis ctxt = Metis_Tactics.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:36 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:56:06 2011 +0200
@@ -542,9 +542,9 @@
else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metisFT" then
- Metis_Tactics.new_metisFT_tac
+ Metis_Tactics.metisFT_tac
else
- Metis_Tactics.new_metis_tac []) ctxt thms
+ Metis_Tactics.metis_tac []) ctxt thms
fun apply_reconstructor thms =
Mirabelle.can_apply timeout (do_reconstructor thms) st
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:56:06 2011 +0200
@@ -427,7 +427,10 @@
fun term_from_atp ctxt textual sym_tab =
let
val thy = Proof_Context.theory_of ctxt
- (* see also "mk_var" in "Metis_Reconstruct" *)
+ (* For Metis, we use 1 rather than 0 because variable references in clauses
+ may otherwise conflict with variable constraints in the goal. At least,
+ type inference often fails otherwise. See also "axiom_inference" in
+ "Metis_Reconstruct". *)
val var_index = if textual then 0 else 1
fun do_term extra_ts opt_T u =
case u of
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:56:06 2011 +0200
@@ -9,8 +9,6 @@
signature METIS_RECONSTRUCT =
sig
- type mode = Metis_Translate.mode
-
exception METIS of string * string
val trace : bool Config.T
@@ -23,7 +21,7 @@
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term * term -> bool
val replay_one_inference :
- Proof.context -> mode -> (string * term) list -> int Symtab.table
+ Proof.context -> (string * term) list -> int Symtab.table
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -65,154 +63,6 @@
| types_of (SomeTerm _ :: tts) = types_of tts
| types_of (SomeType T :: tts) = T :: types_of tts
-fun apply_list rator nargs rands =
- let val trands = terms_of rands
- in if length trands = nargs then SomeTerm (list_comb(rator, trands))
- else raise Fail
- ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
- " expected " ^ string_of_int nargs ^
- " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
- end;
-
-fun infer_types ctxt =
- Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-
-(* We use 1 rather than 0 because variable references in clauses may otherwise
- conflict with variable constraints in the goal...at least, type inference
- often fails otherwise. See also "axiom_inference" below. *)
-fun make_var (w, T) = Var ((w, 1), T)
-
-(*Remove the "apply" operator from an HO term*)
-fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
- | strip_happ args x = (x, args)
-
-fun hol_type_from_metis_term _ (Metis_Term.Var v) =
- (case strip_prefix_and_unascii tvar_prefix v of
- SOME w => make_tvar w
- | NONE => make_tvar v)
- | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
- (case strip_prefix_and_unascii type_const_prefix x of
- SOME tc => Type (invert_const tc,
- map (hol_type_from_metis_term ctxt) tys)
- | NONE =>
- case strip_prefix_and_unascii tfree_prefix x of
- SOME tf => make_tfree ctxt tf
- | NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
-
-(*Maps metis terms to isabelle terms*)
-fun hol_term_from_metis_PT ctxt fol_tm =
- let val thy = Proof_Context.theory_of ctxt
- val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
- Metis_Term.toString fol_tm)
- fun tm_to_tt (Metis_Term.Var v) =
- (case strip_prefix_and_unascii tvar_prefix v of
- SOME w => SomeType (make_tvar w)
- | NONE =>
- case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => SomeTerm (make_var (w, HOLogic.typeT))
- | NONE => SomeTerm (make_var (v, HOLogic.typeT)))
- (*Var from Metis with a name like _nnn; possibly a type variable*)
- | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
- | tm_to_tt (t as Metis_Term.Fn (".", _)) =
- let val (rator,rands) = strip_happ [] t in
- case rator of
- Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
- | _ => case tm_to_tt rator of
- SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
- | _ => raise Fail "tm_to_tt: HO application"
- end
- | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
- and applic_to_tt ("=",ts) =
- SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
- | applic_to_tt (a,ts) =
- case strip_prefix_and_unascii const_prefix a of
- SOME b =>
- let
- val c = b |> invert_const |> unproxify_const
- val ntypes = num_type_args thy c
- val nterms = length ts - ntypes
- val tts = map tm_to_tt ts
- val tys = types_of (List.take(tts,ntypes))
- val t =
- if String.isPrefix new_skolem_const_prefix c then
- Var ((new_skolem_var_name_from_const c, 1),
- Type_Infer.paramify_vars (tl tys ---> hd tys))
- else
- Const (c, dummyT)
- in if length tys = ntypes then
- apply_list t nterms (List.drop(tts,ntypes))
- else
- raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^
- " but gets " ^ string_of_int (length tys) ^
- " type arguments\n" ^
- cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
- " the terms are \n" ^
- cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
- end
- | NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix_and_unascii type_const_prefix a of
- SOME b =>
- SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
- | NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case strip_prefix_and_unascii tfree_prefix a of
- SOME b => SomeType (make_tfree ctxt b)
- | NONE => (*a fixed variable? They are Skolem functions.*)
- case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b =>
- let val opr = Free (b, HOLogic.typeT)
- in apply_list opr (length ts) (map tm_to_tt ts) end
- | NONE => raise Fail ("unexpected metis function: " ^ a)
- in
- case tm_to_tt fol_tm of
- SomeTerm t => t
- | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
- end
-
-(*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_metis_FT ctxt fol_tm =
- let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
- Metis_Term.toString fol_tm)
- fun do_const c =
- let val c = c |> invert_const |> unproxify_const in
- if String.isPrefix new_skolem_const_prefix c then
- Var ((new_skolem_var_name_from_const c, 1), dummyT)
- else
- Const (c, dummyT)
- end
- fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
- (case strip_prefix_and_unascii schematic_var_prefix v of
- SOME w => make_var (w, dummyT)
- | NONE => make_var (v, dummyT))
- | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
- Const (@{const_name HOL.eq}, HOLogic.typeT)
- | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
- (case strip_prefix_and_unascii const_prefix x of
- SOME c => do_const c
- | NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_unascii fixed_var_prefix x of
- SOME v => Free (v, hol_type_from_metis_term ctxt ty)
- | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
- | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) =
- cvt tm1 $ cvt tm2
- | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
- cvt tm1 $ cvt tm2
- | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
- | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
- list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
- | cvt (t as Metis_Term.Fn (x, [])) =
- (case strip_prefix_and_unascii const_prefix x of
- SOME c => do_const c
- | NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix_and_unascii fixed_var_prefix x of
- SOME v => Free (v, dummyT)
- | NONE => (trace_msg ctxt (fn () =>
- "hol_term_from_metis_FT bad const: " ^ x);
- hol_term_from_metis_PT ctxt t))
- | cvt t = (trace_msg ctxt (fn () =>
- "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
- hol_term_from_metis_PT ctxt t)
- in fol_tm |> cvt end
-
fun atp_name_from_metis s =
case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
SOME ((s, _), (_, swap)) => (s, swap)
@@ -223,15 +73,8 @@
end
| atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
-fun hol_term_from_metis_MX ctxt sym_tab =
- atp_term_from_metis
- #> term_from_atp ctxt false sym_tab NONE
-
-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 (Type_Sys _) sym_tab =
- hol_term_from_metis_MX ctxt sym_tab
+fun hol_term_from_metis ctxt sym_tab =
+ atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
fun atp_literal_from_metis (pos, atom) =
atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
@@ -241,7 +84,7 @@
fun reveal_old_skolems_and_infer_types ctxt old_skolems =
map (reveal_old_skolem_terms old_skolems)
- #> infer_types ctxt
+ #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
fun hol_clause_from_metis ctxt sym_tab old_skolems =
Metis_Thm.clause
@@ -250,8 +93,8 @@
#> prop_from_atp ctxt false sym_tab
#> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
-fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
- let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
+fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
+ let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -284,9 +127,9 @@
(* INFERENCE RULE: AXIOM *)
-(* This causes variables to have an index of 1 by default. See also "make_var"
- above. *)
-fun axiom_inference th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
+(* This causes variables to have an index of 1 by default. See also
+ "term_from_atp" in "ATP_Reconstruct". *)
+val axiom_inference = Thm.incr_indexes 1 oo lookth
(* INFERENCE RULE: ASSUME *)
@@ -298,10 +141,10 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
in cterm_instantiate substs th end;
-fun assume_inference ctxt mode old_skolems sym_tab atom =
+fun assume_inference ctxt old_skolems sym_tab atom =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
+ (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
(Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -309,7 +152,7 @@
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inference ctxt mode old_skolems sym_tab th_pairs fsubst th =
+fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
let val thy = Proof_Context.theory_of ctxt
val i_th = lookth th_pairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -317,7 +160,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolems_and_infer_types" below. *)
- val t = hol_term_from_metis ctxt mode sym_tab y
+ val t = hol_term_from_metis ctxt sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -441,7 +284,7 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inference ctxt mode old_skolems sym_tab th_pairs atom th1 th2 =
+fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
let
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
@@ -457,7 +300,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_atom =
- singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
+ singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
(Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () =>
" atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -486,10 +329,10 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inference ctxt mode old_skolems sym_tab t =
+fun refl_inference ctxt old_skolems sym_tab t =
let
val thy = Proof_Context.theory_of ctxt
- val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t
+ val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -499,19 +342,11 @@
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
-val metis_eq = Metis_Term.Fn ("=", []);
-
-(* Equality has no type arguments *)
-fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0
- | get_ty_arg_size thy (Const (s, _)) =
- (num_type_args thy s handle TYPE _ => 0)
- | get_ty_arg_size _ _ = 0
-
-fun equality_inference ctxt mode old_skolems sym_tab (pos, atom) fp fr =
+fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
let val thy = Proof_Context.theory_of ctxt
val m_tm = Metis_Term.Fn atom
val [i_atom, i_tm] =
- hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr]
+ hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
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
@@ -522,53 +357,24 @@
(case t of
SOME t => " fol-term: " ^ Metis_Term.toString t
| NONE => ""))
- fun path_finder_FO tm [] = (tm, Bound 0)
- | path_finder_FO tm (p::ps) =
- let val (tm1,args) = strip_comb tm
- val adjustment = get_ty_arg_size thy tm1
- val p' = if adjustment > p then p else p - adjustment
- val tm_p = nth args p'
- handle Subscript =>
- raise METIS ("equality_inference",
- string_of_int p ^ " adj " ^
- string_of_int adjustment ^ " term " ^
- Syntax.string_of_term ctxt tm)
- val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
- " " ^ Syntax.string_of_term ctxt tm_p)
- val (r,t) = path_finder_FO tm_p ps
- in
- (r, list_comb (tm1, replace_item_list t p' args))
- end
- 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 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
- | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
- (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 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)) =
+ fun path_finder tm [] _ = (tm, Bound 0)
+ | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
let
val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
#> the #> unmangled_const_name))
in
if s = metis_predicator orelse s = predicator_name orelse
s = metis_type_tag orelse s = type_tag_name then
- path_finder_MX tm ps (nth ts p)
+ path_finder tm ps (nth ts p)
else if s = metis_app_op orelse s = app_op_name then
let
val (tm1, tm2) = dest_comb tm
val p' = p - (length ts - 2)
in
if p' = 0 then
- path_finder_MX tm1 ps (nth ts p) ||> (fn y => y $ tm2)
+ path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
else
- path_finder_MX tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
+ path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
end
else
let
@@ -581,31 +387,11 @@
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)
+ val (r, t) = path_finder 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 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*)
- if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
- else path_finder_HO tm (p::ps) (*1 selects second operand*)
- | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
- path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
- | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
- (Metis_Term.Fn ("=", [t1,t2])) =
- (*equality: not curried, as other predicates are*)
- if p=0 then path_finder_FT tm (0::1::ps)
- (Metis_Term.Fn (metis_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2]))
- (*select first operand*)
- else path_finder_FT tm (p::ps)
- (Metis_Term.Fn (metis_app_op, [metis_eq, t2]))
- (*1 selects second operand*)
- | 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 (Type_Sys _) tm ps t = path_finder_MX tm ps t
- val (tm_subst, body) = path_finder mode i_atom fp m_tm
+ | path_finder tm ps t = path_finder_fail tm ps (SOME t)
+ val (tm_subst, body) = path_finder 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)
val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
@@ -619,21 +405,21 @@
val factor = Seq.hd o distinct_subgoals_tac
-fun one_step ctxt mode old_skolems sym_tab th_pairs p =
+fun one_step ctxt old_skolems sym_tab th_pairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
| (_, Metis_Proof.Assume f_atom) =>
- assume_inference ctxt mode old_skolems sym_tab f_atom
+ assume_inference ctxt old_skolems sym_tab f_atom
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- inst_inference ctxt mode old_skolems sym_tab th_pairs f_subst f_th1
+ inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
|> factor
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
- resolve_inference ctxt mode old_skolems sym_tab th_pairs f_atom f_th1 f_th2
+ resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
|> factor
| (_, Metis_Proof.Refl f_tm) =>
- refl_inference ctxt mode old_skolems sym_tab f_tm
+ refl_inference ctxt old_skolems sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inference ctxt mode old_skolems sym_tab f_lit f_p f_r
+ equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -684,7 +470,7 @@
end
end
-fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs =
+fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
if not (null th_pairs) andalso
prop_of (snd (hd th_pairs)) aconv @{prop False} then
(* Isabelle sometimes identifies literals (premises) that are distinct in
@@ -699,7 +485,7 @@
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf)
+ val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:56:06 2011 +0200
@@ -16,11 +16,8 @@
val trace : bool Config.T
val verbose : bool Config.T
val new_skolemizer : bool Config.T
- val old_metis_tac : Proof.context -> thm list -> int -> tactic
- val old_metisF_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 metis_tac : string list -> Proof.context -> thm list -> int -> tactic
+ val metisFT_tac : Proof.context -> thm list -> int -> tactic
val setup : theory -> theory
end
@@ -38,15 +35,12 @@
val default_unsound_type_sys = "poly_args"
val default_sound_type_sys = "poly_preds_heavy_query"
-fun method_call_for_mode HO = (@{binding old_metis}, "")
- | method_call_for_mode FO = (@{binding metisF}, "")
- | method_call_for_mode FT = (@{binding old_metisFT}, "")
- | method_call_for_mode (Type_Sys type_sys) =
- if type_sys = default_sound_type_sys then
- (@{binding metisFT}, "")
- else
- (@{binding metis},
- if type_sys = default_unsound_type_sys then "" else type_sys)
+fun method_call_for_type_sys type_sys =
+ if type_sys = default_sound_type_sys then
+ (@{binding metisFT}, "")
+ else
+ (@{binding metis},
+ if type_sys = default_unsound_type_sys then "" else type_sys)
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -92,13 +86,8 @@
val resolution_params = {active = active_params, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
+fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
- val _ =
- if mode = FO then
- legacy_feature "Old 'metisF' command -- use 'metis' instead"
- else
- ()
val new_skolemizer =
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
val th_cls_pairs =
@@ -112,8 +101,8 @@
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 (mode, sym_tab, {axioms, old_skolems, ...}) =
- prepare_metis_problem ctxt mode cls ths
+ val (sym_tab, axioms, old_skolems) =
+ prepare_metis_problem ctxt type_sys 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
@@ -121,7 +110,7 @@
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 () => "mode = " ^ string_of_mode mode)
+ val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
in
case filter (fn t => prop_of t aconv @{prop False}) cls of
@@ -136,8 +125,8 @@
(*add constraints arising from converting goal to clause form*)
val proof = Metis_Proof.proof mth
val result =
- fold (replay_one_inference ctxt' mode old_skolems sym_tab)
- proof axioms
+ axioms
+ |> fold (replay_one_inference ctxt' 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
@@ -166,7 +155,7 @@
end
| Metis_Resolution.Satisfiable _ =>
(trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
- if null fallback_modes then
+ if null fallback_type_syss then
()
else
raise METIS ("FOL_SOLVE",
@@ -174,17 +163,17 @@
[])
end
handle METIS (loc, msg) =>
- case fallback_modes of
+ case fallback_type_syss of
[] => error ("Failed to replay Metis proof in Isabelle." ^
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
else ""))
- | mode :: _ =>
- let val (binding, arg) = method_call_for_mode mode in
+ | type_sys :: _ =>
+ let val (binding, arg) = method_call_for_type_sys type_sys in
(verbose_warning ctxt
("Falling back on " ^
quote (Binding.qualified_name_of binding ^
(arg |> arg <> "" ? enclose " (" ")")) ^ "...");
- FOL_SOLVE fallback_modes ctxt cls ths0)
+ FOL_SOLVE fallback_type_syss ctxt cls ths0)
end
val neg_clausify =
@@ -204,12 +193,12 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-fun generic_metis_tac modes ctxt ths i st0 =
+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 modes ctxt clause ths) 1
+ 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 {}";
@@ -218,19 +207,12 @@
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
end
-val old_metis_modes = [HO, FT]
-val old_metisF_modes = [FO, FT]
-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_default_type_syss = [default_unsound_type_sys, default_sound_type_sys]
+val metisFT_type_syss = [default_sound_type_sys]
-val old_metis_tac = generic_metis_tac old_metis_modes
-val old_metisF_tac = generic_metis_tac old_metisF_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
+fun metis_tac [] = generic_metis_tac metis_default_type_syss
+ | metis_tac type_syss = generic_metis_tac type_syss
+val metisFT_tac = generic_metis_tac metisFT_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.
@@ -240,33 +222,30 @@
val has_tvar =
exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
-fun method modes (type_sys, ths) ctxt facts =
+fun method type_syss (type_sys, ths) ctxt facts =
let
val (schem_facts, nonschem_facts) = List.partition has_tvar facts
- val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes
+ val type_syss = type_sys |> Option.map single |> the_default type_syss
in
HEADGOAL (Method.insert_tac nonschem_facts THEN'
- CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths))
+ CHANGED_PROP
+ o generic_metis_tac type_syss ctxt (schem_facts @ ths))
end
-fun setup_method (modes as mode :: _) =
- (if modes = new_metis_default_modes then
+fun setup_method (type_syss as type_sys :: _) =
+ (if type_syss = metis_default_type_syss 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))
+ -- Attrib.thms >> (METHOD oo method type_syss)
+ |> Method.setup (fst (method_call_for_type_sys type_sys))
val setup =
- [(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)")]
+ [(metis_default_type_syss, "Metis for FOL and HOL problems"),
+ (metisFT_type_syss,
+ "Metis for FOL/HOL problems with fully-typed translation")]
|> fold (uncurry setup_method)
end;
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:56:06 2011 +0200
@@ -11,17 +11,10 @@
sig
type type_literal = ATP_Translate.type_literal
- datatype mode = FO | HO | FT | Type_Sys of string
-
datatype isa_thm =
Isa_Reflexive_or_Trivial |
Isa_Raw of thm
- type metis_problem =
- {axioms : (Metis_Thm.thm * isa_thm) list,
- tfrees : type_literal list,
- old_skolems : (string * term) list}
-
val metis_equal : string
val metis_predicator : string
val metis_app_op : string
@@ -29,10 +22,9 @@
val metis_generated_var_prefix : string
val metis_name_table : ((string * int) * (string * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
- val string_of_mode : mode -> string
val prepare_metis_problem :
- Proof.context -> mode -> thm list -> thm list
- -> mode * int Symtab.table * metis_problem
+ Proof.context -> string -> thm list -> thm list
+ -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -54,20 +46,6 @@
((prefixed_app_op_name, 2), (metis_app_op, false)),
((prefixed_type_tag_name, 2), (metis_type_tag, true))]
-fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
- | predicate_of thy (t, pos) =
- (combterm_from_term thy [] (Envir.eta_contract t), pos)
-
-fun literals_of_term1 args thy (@{const Trueprop} $ P) =
- literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy P) thy Q
- | literals_of_term1 (lits, ts) thy P =
- let val ((pred, ts'), pol) = predicate_of thy (P, true) in
- ((pol, pred) :: lits, union (op =) ts ts')
- end
-val literals_of_term = literals_of_term1 ([], [])
-
fun old_skolem_const_name i j num_T_args =
old_skolem_const_prefix ^ Long_Name.separator ^
(space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
@@ -114,127 +92,6 @@
(* ------------------------------------------------------------------------- *)
-(* HOL to FOL (Isabelle to Metis) *)
-(* ------------------------------------------------------------------------- *)
-
-(* 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 (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"
- | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
- | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
- | fn_isa_to_met_sublevel "c_conj" = "c_fconj"
- | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"
- | fn_isa_to_met_sublevel "c_implies" = "c_fimplies"
- | fn_isa_to_met_sublevel x = x
-
-fun fn_isa_to_met_toplevel "equal" = metis_equal
- | fn_isa_to_met_toplevel x = x
-
-fun metis_lit b c args = (b, (c, args));
-
-fun metis_term_from_typ (Type (s, Ts)) =
- Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts)
- | metis_term_from_typ (TFree (s, _)) =
- Metis_Term.Fn (make_fixed_type_var s, [])
- | metis_term_from_typ (TVar (x, _)) =
- Metis_Term.Var (make_schematic_type_var x)
-
-(*These two functions insert type literals before the real literals. That is the
- opposite order from TPTP linkup, but maybe OK.*)
-
-fun hol_term_to_fol_FO tm =
- case strip_combterm_comb tm of
- (CombConst ((c, _), _, Ts), tms) =>
- let val tyargs = map metis_term_from_typ Ts
- val args = map hol_term_to_fol_FO tms
- in Metis_Term.Fn (c, tyargs @ args) end
- | (CombVar ((v, _), _), []) => Metis_Term.Var v
- | _ => raise Fail "non-first-order combterm"
-
-fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) =
- Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts)
- | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
- | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
- Metis_Term.Fn (metis_app_op, map hol_term_to_fol_HO [tm1, tm2])
-
-(*The fully-typed translation, to avoid type errors*)
-fun tag_with_type tm T =
- Metis_Term.Fn (metis_type_tag, [tm, metis_term_from_typ T])
-
-fun hol_term_to_fol_FT (CombVar ((s, _), ty)) =
- tag_with_type (Metis_Term.Var s) ty
- | hol_term_to_fol_FT (CombConst ((a, _), ty, _)) =
- tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty
- | hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) =
- tag_with_type
- (Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2]))
- (combtyp_of tm)
-
-fun hol_literal_to_fol FO (pos, tm) =
- let
- val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm
- val tylits = if p = "equal" then [] else map metis_term_from_typ Ts
- val lits = map hol_term_to_fol_FO tms
- in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
- | hol_literal_to_fol HO (pos, tm) =
- (case strip_combterm_comb tm of
- (CombConst(("equal", _), _, _), tms) =>
- metis_lit pos metis_equal (map hol_term_to_fol_HO tms)
- | _ => metis_lit pos metis_predicator [hol_term_to_fol_HO tm])
- | hol_literal_to_fol FT (pos, tm) =
- (case strip_combterm_comb tm of
- (CombConst(("equal", _), _, _), tms) =>
- metis_lit pos metis_equal (map hol_term_to_fol_FT tms)
- | _ => metis_lit pos metis_predicator [hol_term_to_fol_FT tm])
-
-fun literals_of_hol_term thy mode t =
- let val (lits, types_sorts) = literals_of_term thy t in
- (map (hol_literal_to_fol mode) lits, types_sorts)
- end
-
-(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
- metis_lit pos s [Metis_Term.Var s']
- | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
- metis_lit pos s [Metis_Term.Fn (s',[])]
-
-fun has_default_sort _ (TVar _) = false
- | has_default_sort ctxt (TFree (x, s)) =
- (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
-
-fun metis_of_tfree tf =
- Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
-
-fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th =
- let
- val thy = Proof_Context.theory_of ctxt
- val (old_skolems, (mlits, types_sorts)) =
- th |> prop_of |> Logic.strip_imp_concl
- |> conceal_old_skolem_terms j old_skolems
- ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
- in
- if is_conjecture then
- (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
- raw_type_literals_for_types types_sorts, old_skolems)
- else
- let
- val tylits = types_sorts |> filter_out (has_default_sort ctxt)
- |> raw_type_literals_for_types
- val mtylits = map (metis_of_type_literals false) tylits
- in
- (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
- old_skolems)
- end
- end;
-
-(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
(* ------------------------------------------------------------------------- *)
@@ -242,56 +99,6 @@
Isa_Reflexive_or_Trivial |
Isa_Raw of thm
-type metis_problem =
- {axioms : (Metis_Thm.thm * isa_thm) list,
- tfrees : type_literal list,
- old_skolems : (string * term) list}
-
-fun is_quasi_fol_clause thy =
- Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
-
-(*Extract TFree constraints from context to include as conjecture clauses*)
-fun init_tfrees ctxt =
- let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
- Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
- |> raw_type_literals_for_types
- end;
-
-fun const_in_metis c (pred, tm_list) =
- let
- fun in_mterm (Metis_Term.Var _) = false
- | in_mterm (Metis_Term.Fn (nm, tm_list)) =
- c = nm orelse exists in_mterm tm_list
- in c = pred orelse exists in_mterm tm_list end
-
-(* ARITY CLAUSE *)
-fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
- metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
- | m_arity_cls (TVarLit ((c, _), (s, _))) =
- metis_lit false c [Metis_Term.Var s]
-(* TrueI is returned as the Isabelle counterpart because there isn't any. *)
-fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) =
- (TrueI,
- Metis_Thm.axiom (Metis_LiteralSet.fromList
- (map m_arity_cls (concl_lits :: prem_lits))));
-
-(* CLASSREL CLAUSE *)
-fun m_class_rel_cls (subclass, _) (superclass, _) =
- [metis_lit false subclass [Metis_Term.Var "T"],
- metis_lit true superclass [Metis_Term.Var "T"]]
-fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) =
- (TrueI, m_class_rel_cls subclass superclass
- |> Metis_LiteralSet.fromList |> Metis_Thm.axiom)
-
-fun type_ext thy tms =
- let
- val subs = tfree_classes_of_terms tms
- val supers = tvar_classes_of_terms tms
- val tycons = type_constrs_of_terms thy tms
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers'
- in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
-
val proxy_defs = map (fst o snd o snd) proxy_table
val prepare_helper =
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
@@ -346,92 +153,39 @@
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt (mode as Type_Sys type_sys) conj_clauses
- fact_clauses =
- let
- val type_sys = type_sys_from_string type_sys
- val explicit_apply = NONE
- val clauses =
- conj_clauses @ fact_clauses
- |> (if polymorphism_of_type_sys type_sys = Polymorphic then
- I
- else
- map (pair 0)
- #> rpair ctxt
- #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
- #> fst #> maps (map (zero_var_indexes o snd)))
- val (old_skolems, props) =
- fold_rev (fn clause => fn (old_skolems, props) =>
- clause |> prop_of |> Logic.strip_imp_concl
- |> conceal_old_skolem_terms (length clauses)
- old_skolems
- ||> (fn prop => prop :: props))
- clauses ([], [])
+fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
+ let
+ val type_sys = type_sys_from_string type_sys
+ val explicit_apply = NONE
+ val clauses =
+ conj_clauses @ fact_clauses
+ |> (if polymorphism_of_type_sys type_sys = Polymorphic then
+ I
+ else
+ map (pair 0)
+ #> rpair ctxt
+ #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
+ #> fst #> maps (map (zero_var_indexes o snd)))
+ val (old_skolems, props) =
+ fold_rev (fn clause => fn (old_skolems, props) =>
+ clause |> prop_of |> Logic.strip_imp_concl
+ |> conceal_old_skolem_terms (length clauses)
+ old_skolems
+ ||> (fn prop => prop :: props))
+ clauses ([], [])
(*
val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
*)
- val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
- false false props @{prop False} []
+ val (atp_problem, _, _, _, _, _, sym_tab) =
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
+ false false props @{prop False} []
(*
val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
*)
- (* "rev" is for compatibility *)
- val axioms =
- atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
- |> rev
- in
- (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
- end
- | 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. *)
- val mode =
- if mode = HO andalso
- forall (forall (is_quasi_fol_clause thy))
- [conj_clauses, fact_clauses] then
- FO
- else
- mode
- fun add_thm is_conjecture (isa_ith, metis_ith)
- {axioms, tfrees, old_skolems} : metis_problem =
- let
- val (mth, tfree_lits, old_skolems) =
- hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
- metis_ith
- in
- {axioms = (mth, Isa_Raw isa_ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
- end;
- fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} =
- {axioms = (mth, Isa_Raw ith) :: axioms, tfrees = tfrees,
- old_skolems = old_skolems}
- fun add_tfrees {axioms, tfrees, old_skolems} =
- {axioms = map (rpair (Isa_Raw TrueI) o metis_of_tfree)
- (distinct (op =) tfrees) @ axioms,
- tfrees = tfrees, old_skolems = old_skolems}
- val problem =
- {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
- |> fold (add_thm true o `Meson.make_meta_clause) conj_clauses
- |> add_tfrees
- |> fold (add_thm false o `Meson.make_meta_clause) fact_clauses
- val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem)
- fun is_used c =
- exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
- val problem =
- if mode = FO then
- problem
- else
- let
- val helper_ths =
- helper_table
- |> filter (is_used o prefix const_prefix o fst o fst)
- |> maps (fn ((_, needs_full_types), thms) =>
- if needs_full_types andalso mode <> FT then []
- else map (`prepare_helper) thms)
- in problem |> fold (add_thm false) helper_ths end
- val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
- in (mode, Symtab.empty, fold add_type_thm type_ths problem) end
+ (* "rev" is for compatibility *)
+ val axioms =
+ atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
+ |> rev
+ in (sym_tab, axioms, old_skolems) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:56:06 2011 +0200
@@ -417,8 +417,8 @@
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
fun tac_for_reconstructor Metis =
- Metis_Tactics.new_metis_tac [Metis_Tactics.default_unsound_type_sys]
- | tac_for_reconstructor MetisFT = Metis_Tactics.new_metisFT_tac
+ Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys]
+ | tac_for_reconstructor MetisFT = Metis_Tactics.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:36 2011 +0200
+++ b/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:56:06 2011 +0200
@@ -52,7 +52,7 @@
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis"
- (ALLGOALS (Metis_Tactics.new_metis_tac [] ctxt []))
+ (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
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:36 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:56:06 2011 +0200
@@ -70,7 +70,7 @@
in
case run_atp false timeout i i ctxt th atp of
SOME facts =>
- Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
+ Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
| NONE => Seq.empty
end