--- a/src/HOL/TPTP/atp_export.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/TPTP/atp_export.ML Tue Nov 15 22:13:39 2011 +0100
@@ -175,7 +175,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
- val (atp_problem, _, _, _, _, _, _) =
+ val (atp_problem, _, _, _, _, _, _, _) =
facts
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc),
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:13:39 2011 +0100
@@ -45,7 +45,7 @@
val const_prefix : string
val type_const_prefix : string
val class_prefix : string
- val polymorphic_free_prefix : string
+ val lambda_lifted_prefix : string
val skolem_const_prefix : string
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
@@ -87,6 +87,8 @@
val is_type_enc_fairly_sound : type_enc -> bool
val type_enc_from_string : soundness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
+ val lift_lambdas :
+ Proof.context -> type_enc -> term list -> term list * term list
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -98,7 +100,8 @@
-> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
- * (string * locality) list vector * int list * int Symtab.table
+ * (string * locality) list vector * int list * (string * term) list
+ * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
end;
@@ -140,7 +143,8 @@
val simple_type_prefix = "s_"
val class_prefix = "cl_"
-val polymorphic_free_prefix = "poly_free"
+val lambda_lifted_prefix = "lambda"
+val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "_poly"
val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
@@ -494,7 +498,7 @@
atomic_types_of T)
| iterm_from_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T,
- if String.isPrefix polymorphic_free_prefix s then [T] else []),
+ if String.isPrefix lambda_lifted_poly_prefix s then [T] else []),
atomic_types_of T)
| iterm_from_term _ format _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
@@ -653,10 +657,10 @@
fun lift_lambdas ctxt type_enc =
map (close_form o Envir.eta_contract) #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
- (if polymorphism_of_type_enc type_enc = Polymorphic then
- SOME polymorphic_free_prefix
- else
- NONE)
+ (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
+ lambda_lifted_poly_prefix
+ else
+ lambda_lifted_prefix))
Lambda_Lifting.is_quantifier
#> fst
@@ -1117,7 +1121,7 @@
do_cheaply_conceal_lambdas Ts t1
$ do_cheaply_conceal_lambdas Ts t2
| do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
- Free (polymorphic_free_prefix ^ serial_string (),
+ Free (lambda_lifted_poly_prefix ^ serial_string (),
T --> fastype_of1 (T :: Ts, t))
| do_cheaply_conceal_lambdas _ t = t
@@ -1630,7 +1634,7 @@
| add (Const x) =
x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
| add (Free (s, T)) =
- if String.isPrefix polymorphic_free_prefix s then
+ if String.isPrefix lambda_lifted_poly_prefix s then
T |> fold_type_constrs set_insert
else
I
@@ -1641,6 +1645,17 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
+val extract_lambda_def =
+ let
+ fun extr [] (@{const Trueprop} $ t) = extr [] t
+ | extr bs (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+ extr ((s, T) :: bs) t
+ | extr bs (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ (t |> head_of |> dest_Free |> fst,
+ fold_rev (fn (s, T) => fn u => Abs (s, T, u)) bs u)
+ | extr _ _ = raise Fail "malformed lifted lambda"
+ in extr [] end
+
fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts =
let
@@ -1657,7 +1672,7 @@
map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
|> map (apsnd freeze_term)
|> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
- val ((conjs, facts), lambdas) =
+ val ((conjs, facts), lambda_facts) =
if preproc then
conjs @ facts
|> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
@@ -1672,8 +1687,10 @@
make_fact ctxt format type_enc true (name, t)
|> Option.map (pair name))
|> ListPair.unzip
- val lambdas =
- lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
+ val lifted = lambda_facts |> map (extract_lambda_def o snd o snd)
+ val lambda_facts =
+ lambda_facts
+ |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
val all_ts = concl_t :: hyp_ts @ fact_ts
val subs = tfree_classes_of_terms all_ts
val supers = tvar_classes_of_terms all_ts
@@ -1683,8 +1700,8 @@
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers
in
- (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
- class_rel_clauses, arity_clauses)
+ (fact_names |> map single, union (op =) subs supers, conjs,
+ facts @ lambda_facts, class_rel_clauses, arity_clauses, lifted)
end
val type_guard = `(make_fixed_const NONE) type_guard_name
@@ -2095,8 +2112,10 @@
| NONE =>
case strip_prefix_and_unascii fixed_var_prefix s of
SOME s' =>
- if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
- else raise Fail "unexpected type arguments to free variable"
+ if String.isPrefix lambda_lifted_poly_prefix s' then
+ (tvar_a, [tvar_a])
+ else
+ raise Fail "unexpected type arguments to free variable"
| NONE => raise Fail "unexpected type arguments"
in
Decl (sym_decl_prefix ^ s, (s, s'),
@@ -2317,7 +2336,8 @@
else
error ("Unknown lambda translation method: " ^
quote lambda_trans ^ ".")
- val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
+ val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
+ lifted) =
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
val sym_tab =
@@ -2390,6 +2410,7 @@
offset_of_heading_in_problem factsN problem 0,
fact_names |> Vector.fromList,
typed_helpers,
+ lifted,
Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
end
--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 22:13:39 2011 +0100
@@ -15,7 +15,8 @@
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
val ss_only : thm list -> simpset
val cnf_axiom :
- Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
+ Proof.context -> bool -> bool -> int -> thm
+ -> (thm * term) option * thm list
end;
structure Meson_Clausify : MESON_CLAUSIFY =
@@ -364,7 +365,7 @@
end
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom ctxt0 new_skolemizer ax_no th =
+fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th =
let
val thy = Proof_Context.theory_of ctxt0
val choice_ths = choice_theorems thy
@@ -385,7 +386,7 @@
(opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
##> (term_of #> HOLogic.dest_Trueprop
#> singleton (Variable.export_terms ctxt ctxt0))),
- cnf_ths |> map (introduce_combinators_in_theorem
+ cnf_ths |> map (combinators ? introduce_combinators_in_theorem
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
|> Variable.export ctxt ctxt0
|> finish_cnf
--- a/src/HOL/Tools/Meson/meson_tactic.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Tue Nov 15 22:13:39 2011 +0100
@@ -18,7 +18,7 @@
fun meson_general_tac ctxt ths =
let val ctxt' = put_claset HOL_cs ctxt
- in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end
+ in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false true 0) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100
@@ -14,11 +14,12 @@
exception METIS of string * string
val hol_clause_from_metis :
- Proof.context -> type_enc -> int Symtab.table -> (string * term) list
- -> Metis_Thm.thm -> term
+ Proof.context -> type_enc -> int Symtab.table
+ -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val replay_one_inference :
- Proof.context -> type_enc -> (string * term) list -> int Symtab.table
+ Proof.context -> type_enc
+ -> (string * term) list * (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 :
@@ -55,24 +56,24 @@
| atp_clause_from_metis type_enc lits =
lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
-fun reveal_old_skolems_and_infer_types ctxt old_skolems =
- map (reveal_old_skolem_terms old_skolems)
+fun polish_hol_terms ctxt (lifted, old_skolems) =
+ map (reveal_lambda_lifted lifted
+ #> reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems =
+fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
Metis_Thm.clause
#> Metis_LiteralSet.toList
#> atp_clause_from_metis type_enc
#> prop_from_atp ctxt false sym_tab
- #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
+ #> singleton (polish_hol_terms ctxt concealed)
-fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms =
+fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
let val ts = map (hol_term_from_metis ctxt type_enc 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
- val ts' =
- ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
+ val ts' = ts |> polish_hol_terms ctxt concealed
val _ = app (fn t => trace_msg ctxt
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -114,10 +115,10 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
in cterm_instantiate substs th end;
-fun assume_inference ctxt type_enc old_skolems sym_tab atom =
+fun assume_inference ctxt type_enc concealed sym_tab atom =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
+ (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
(Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -125,14 +126,14 @@
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th =
+fun inst_inference ctxt type_enc concealed 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) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reveal_old_skolems_and_infer_types" below. *)
+ (* We call "polish_hol_terms" below. *)
val t = hol_term_from_metis ctxt type_enc sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
@@ -156,7 +157,7 @@
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
val (vars, tms) =
ListPair.unzip (map_filter subst_translation substs)
- ||> reveal_old_skolems_and_infer_types ctxt old_skolems
+ ||> polish_hol_terms ctxt concealed
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg ctxt (fn () =>
@@ -258,7 +259,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 type_enc old_skolems sym_tab th_pairs atom th1 th2 =
+fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
let
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
@@ -274,7 +275,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_atom =
- singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
+ singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
(Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () =>
" atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -303,11 +304,11 @@
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 type_enc old_skolems sym_tab t =
+fun refl_inference ctxt type_enc concealed sym_tab t =
let
val thy = Proof_Context.theory_of ctxt
val i_t =
- singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t
+ singleton (hol_terms_from_metis ctxt type_enc concealed 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
@@ -317,11 +318,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}
-fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr =
+fun equality_inference ctxt type_enc concealed 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 type_enc old_skolems sym_tab [m_tm, fr]
+ hol_terms_from_metis ctxt type_enc concealed 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
@@ -382,22 +383,22 @@
val factor = Seq.hd o distinct_subgoals_tac
-fun one_step ctxt type_enc old_skolems sym_tab th_pairs p =
+fun one_step ctxt type_enc concealed 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 type_enc old_skolems sym_tab f_atom
+ assume_inference ctxt type_enc concealed sym_tab f_atom
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1
+ inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1
|> factor
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
- resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1
+ resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1
f_th2
|> factor
| (_, Metis_Proof.Refl f_tm) =>
- refl_inference ctxt type_enc old_skolems sym_tab f_tm
+ refl_inference ctxt type_enc concealed sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r
+ equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -449,7 +450,7 @@
end
end
-fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf)
+fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
th_pairs =
if not (null th_pairs) andalso
prop_of (snd (hd th_pairs)) aconv @{prop False} then
@@ -465,7 +466,7 @@
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf)
+ val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100
@@ -75,9 +75,9 @@
"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 =
+fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
+ case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = cterm_of thy t
@@ -106,14 +106,15 @@
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 =
+fun FOL_SOLVE (type_enc :: fallback_type_syss) lambda_trans 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))
+ Meson_Clausify.cnf_axiom ctxt new_skolemizer
+ (lambda_trans = combinatorsN) 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
@@ -121,10 +122,10 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_from_string Sound type_enc
- val (sym_tab, axioms, old_skolems) =
- prepare_metis_problem ctxt type_enc cls ths
+ val (sym_tab, axioms, concealed) =
+ prepare_metis_problem ctxt type_enc lambda_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
+ reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
@@ -148,7 +149,7 @@
val proof = Metis_Proof.proof mth
val result =
axioms
- |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
+ |> fold (replay_one_inference ctxt' type_enc concealed 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
@@ -193,12 +194,12 @@
(verbose_warning ctxt
("Falling back on " ^
quote (method_call_for_type_enc fallback_type_syss) ^ "...");
- FOL_SOLVE fallback_type_syss ctxt cls ths0)
+ FOL_SOLVE fallback_type_syss lambda_trans ctxt cls ths0)
-fun neg_clausify ctxt =
+fun neg_clausify ctxt combinators =
single
#> Meson.make_clauses_unsorted ctxt
- #> map Meson_Clausify.introduce_combinators_in_theorem
+ #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
#> Meson.finish_cnf
fun preskolem_tac ctxt st0 =
@@ -214,16 +215,19 @@
fun generic_metis_tac type_syss ctxt ths i st0 =
let
+ val lambda_trans = Config.get ctxt lambda_translation
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
+ fun tac clause =
+ resolve_tac (FOL_SOLVE type_syss lambda_trans 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
+ Meson.MESON (preskolem_tac ctxt)
+ (maps (neg_clausify ctxt (lambda_trans = combinatorsN))) tac ctxt i st0
end
fun metis_tac [] = generic_metis_tac partial_type_syss
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100
@@ -23,13 +23,16 @@
val metis_generated_var_prefix : string
val trace : bool Config.T
val verbose : bool Config.T
+ val lambda_translation : string Config.T
val trace_msg : Proof.context -> (unit -> string) -> unit
val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
+ val reveal_lambda_lifted : (string * term) list -> term -> term
val prepare_metis_problem :
- Proof.context -> type_enc -> thm list -> thm list
- -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
+ Proof.context -> type_enc -> string -> thm list -> thm list
+ -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
+ * ((string * term) list * (string * term) list)
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -48,6 +51,9 @@
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
+val lambda_translation =
+ Attrib.setup_config_string @{binding metis_lambda_translation}
+ (K combinatorsN)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
fun verbose_warning ctxt msg =
@@ -107,6 +113,16 @@
t
| t => t)
+fun reveal_lambda_lifted lambdas =
+ map_aterms (fn t as Free (s, _) =>
+ if String.isPrefix lambda_lifted_prefix s then
+ case AList.lookup (op =) lambdas s of
+ SOME t => t |> map_types (map_type_tvar (K dummyT))
+ | NONE => t
+ else
+ t
+ | t => t)
+
(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
@@ -175,7 +191,7 @@
| 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 type_enc conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses =
let
val (conj_clauses, fact_clauses) =
if polymorphism_of_type_enc type_enc = Polymorphic then
@@ -205,17 +221,18 @@
tracing ("PROPS:\n" ^
cat_lines (map (Syntax.string_of_term ctxt o snd) props))
*)
- val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN
- false false [] @{prop False} props
- (*
+ val (lambda_trans, preproc) =
+ if lambda_trans = combinatorsN then (no_lambdasN, false)
+ else (lambda_trans, true)
+ val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
+ false preproc [] @{prop False} props
val _ = tracing ("ATP PROBLEM: " ^
- cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
- *)
- (* "rev" is for compatibility. *)
+ cat_lines (lines_for_atp_problem CNF atp_problem))
+ (* "rev" is for compatibility with existing proof scripts. *)
val axioms =
atp_problem
|> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
- in (sym_tab, axioms, old_skolems) end
+ in (sym_tab, axioms, (lifted, old_skolems)) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 15:38:50 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:13:39 2011 +0100
@@ -672,7 +672,7 @@
else
()
val (atp_problem, pool, conjecture_offset, facts_offset,
- fact_names, typed_helpers, sym_tab) =
+ fact_names, typed_helpers, _, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
type_enc false (Config.get ctxt atp_lambda_translation)
(not (Config.get ctxt atp_full_names)) true hyp_ts concl_t