ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
--- a/src/HOL/TPTP/atp_export.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sun Jul 17 14:12:45 2011 +0200
@@ -160,8 +160,8 @@
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
- (map (introduce_combinators ctxt o snd)) false true
- [] @{prop False}
+ (rpair [] o map (introduce_combinators ctxt))
+ false true [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Sun Jul 17 14:12:45 2011 +0200
@@ -251,34 +251,6 @@
(** Hard-core proof reconstruction: structured Isar proofs **)
-(* Simple simplifications to ensure that sort annotations don't leave a trail of
- spurious "True"s. *)
-fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
- Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
- | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
- Const (@{const_name All}, T) $ Abs (s, T', s_not t')
- | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
- | s_not (@{const HOL.conj} $ t1 $ t2) =
- @{const HOL.disj} $ s_not t1 $ s_not t2
- | s_not (@{const HOL.disj} $ t1 $ t2) =
- @{const HOL.conj} $ s_not t1 $ s_not t2
- | s_not (@{const False}) = @{const True}
- | s_not (@{const True}) = @{const False}
- | s_not (@{const Not} $ t) = t
- | s_not t = @{const Not} $ t
-fun s_conj (@{const True}, t2) = t2
- | s_conj (t1, @{const True}) = t1
- | s_conj p = HOLogic.mk_conj p
-fun s_disj (@{const False}, t2) = t2
- | s_disj (t1, @{const False}) = t1
- | s_disj p = HOLogic.mk_disj p
-fun s_imp (@{const True}, t2) = t2
- | s_imp (t1, @{const False}) = s_not t1
- | s_imp p = HOLogic.mk_imp p
-fun s_iff (@{const True}, t2) = t2
- | s_iff (t1, @{const True}) = t1
- | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-
fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
--- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:12:45 2011 +0200
@@ -3,7 +3,7 @@
Author: Makarius
Author: Jasmin Blanchette, TU Muenchen
-Translation of HOL to FOL for Sledgehammer.
+Translation of HOL to FOL for Metis and Sledgehammer.
*)
signature ATP_TRANSLATE =
@@ -92,8 +92,8 @@
val introduce_combinators : Proof.context -> term -> term
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> ((formula_kind * term) list -> term list) -> bool -> bool
- -> term list -> term -> ((string * locality) * term) list
+ -> bool -> (term list -> term list * term list) -> 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
val atp_problem_weights : string problem -> (string * real) list
@@ -120,15 +120,13 @@
val bound_var_prefix = "B_"
val schematic_var_prefix = "V_"
val fixed_var_prefix = "v_"
-
val tvar_prefix = "T_"
val tfree_prefix = "t_"
-
val const_prefix = "c_"
val type_const_prefix = "tc_"
val class_prefix = "cl_"
-val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
@@ -143,6 +141,7 @@
val arity_clause_prefix = "arity_"
val tfree_clause_prefix = "tfree_"
+val lambda_fact_prefix = "ATP.lambda_"
val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
@@ -158,9 +157,9 @@
val prefixed_type_tag_name = const_prefix ^ type_tag_name
(* Freshness almost guaranteed! *)
-val sledgehammer_weak_prefix = "Sledgehammer:"
+val atp_weak_prefix = "ATP:"
-val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
+val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
@@ -879,7 +878,7 @@
#> Meson.presimplify ctxt
#> prop_of)
-fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
+fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
fun conceal_bounds Ts t =
subst_bounds (map (Free o apfst concealed_bound_name)
(0 upto length Ts - 1 ~~ Ts), t)
@@ -901,29 +900,34 @@
t
fun simple_translate_lambdas do_lambdas ctxt t =
- let
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name All}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ =>
- if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
- else t |> Envir.eta_contract |> do_lambdas ctxt Ts
- val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
- in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ let val thy = Proof_Context.theory_of ctxt in
+ if Meson.is_fol_term thy t then
+ t
+ else
+ let
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ =>
+ if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
+ else t |> Envir.eta_contract |> do_lambdas ctxt Ts
+ val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
+ in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ end
fun do_conceal_lambdas Ts (t1 $ t2) =
do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
@@ -946,11 +950,16 @@
handle THM _ => do_conceal_lambdas Ts t
val introduce_combinators = simple_translate_lambdas do_introduce_combinators
-fun process_abstractions_in_terms ctxt trans_lambdas ps =
+fun preprocess_abstractions_in_terms ctxt trans_lambdas facts =
let
- val thy = Proof_Context.theory_of ctxt
- val (fo_ps, ho_ps) = ps |> List.partition (Meson.is_fol_term thy o snd)
- in map snd fo_ps @ trans_lambdas ho_ps end
+ val (facts, lambda_ts) =
+ facts |> map (snd o snd) |> trans_lambdas
+ |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
+ val lambda_facts =
+ map2 (fn t => fn j =>
+ ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
+ lambda_ts (1 upto length lambda_ts)
+ in (facts, lambda_facts) end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
@@ -959,11 +968,11 @@
fun aux (t $ u) = aux t $ aux u
| aux (Abs (s, T, t)) = Abs (s, T, aux t)
| aux (Var ((s, i), T)) =
- Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+ Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-fun preprocess_prop ctxt presimp_consts t =
+fun presimp_prop ctxt presimp_consts t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
@@ -1002,9 +1011,8 @@
val thy = Proof_Context.theory_of ctxt
val last = length ps - 1
in
- map2 (fn j => fn (kind, t) =>
- t |> make_formula thy type_enc (format <> CNF) (string_of_int j)
- Local kind
+ map2 (fn j => fn ((name, loc), (kind, t)) =>
+ t |> make_formula thy type_enc (format <> CNF) name loc kind
|> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
(0 upto last) ps
end
@@ -1426,29 +1434,32 @@
let
val thy = Proof_Context.theory_of ctxt
val presimp_consts = Meson.presimplified_consts ctxt
- fun preprocess kind =
- preprocess_prop ctxt presimp_consts
- #> pair kind #> single
- #> process_abstractions_in_terms ctxt trans_lambdas
- #> the_single
val fact_ts = facts |> map snd
(* Remove existing facts from the conjecture, as this can dramatically
boost an ATP's performance (for some reason). *)
val hyp_ts =
hyp_ts
|> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
- val fact_ts = facts |> map snd |> preproc ? map (preprocess Axiom)
+ val fact_ps = facts |> map (apsnd (pair Axiom))
val conj_ps =
map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
- |> preproc
- ? map (fn (kind, t) => (kind, t |> preprocess kind |> freeze_term))
- val (facts, fact_names) =
- map2 (fn (name, _) => fn t =>
- (make_fact ctxt format type_enc true (name, t), name))
- facts fact_ts
- |> map_filter (try (apfst the))
+ |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
+ val ((conj_ps, fact_ps), lambda_ps) =
+ conj_ps @ fact_ps
+ |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
+ |> (if preproc then preprocess_abstractions_in_terms ctxt trans_lambdas
+ else rpair [])
+ |>> chop (length conj_ps)
+ |>> preproc ? apfst (map (apsnd (apsnd freeze_term)))
+ val conjs = make_conjecture ctxt format type_enc conj_ps
+ val (fact_names, facts) =
+ fact_ps
+ |> map_filter (fn (name, (_, t)) =>
+ make_fact ctxt format type_enc true (name, t)
+ |> Option.map (pair name))
|> ListPair.unzip
- val conjs = make_conjecture ctxt format type_enc conj_ps
+ val lambdas =
+ lambda_ps |> map_filter (make_fact ctxt format type_enc false 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
@@ -1458,7 +1469,8 @@
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers
in
- (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
+ (fact_names |> map single,
+ (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
end
fun fo_literal_from_type_literal (TyLitVar (class, name)) =
--- a/src/HOL/Tools/ATP/atp_util.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Jul 17 14:12:45 2011 +0200
@@ -23,6 +23,11 @@
-> typ
val is_type_surely_finite : Proof.context -> bool -> typ -> bool
val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
+ val s_not : term -> term
+ val s_conj : term * term -> term
+ val s_disj : term * term -> term
+ val s_imp : term * term -> term
+ val s_iff : term * term -> term
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
val transform_elim_prop : term -> term
@@ -203,6 +208,34 @@
fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
+(* Simple simplifications to ensure that sort annotations don't leave a trail of
+ spurious "True"s. *)
+fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+ Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
+ | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+ Const (@{const_name All}, T) $ Abs (s, T', s_not t')
+ | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
+ | s_not (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.disj} $ s_not t1 $ s_not t2
+ | s_not (@{const HOL.disj} $ t1 $ t2) =
+ @{const HOL.conj} $ s_not t1 $ s_not t2
+ | s_not (@{const False}) = @{const True}
+ | s_not (@{const True}) = @{const False}
+ | s_not (@{const Not} $ t) = t
+ | s_not t = @{const Not} $ t
+fun s_conj (@{const True}, t2) = t2
+ | s_conj (t1, @{const True}) = t1
+ | s_conj p = HOLogic.mk_conj p
+fun s_disj (@{const False}, t2) = t2
+ | s_disj (t1, @{const False}) = t1
+ | s_disj p = HOLogic.mk_disj p
+fun s_imp (@{const True}, t2) = t2
+ | s_imp (t1, @{const False}) = s_not t1
+ | s_imp p = HOLogic.mk_imp p
+fun s_iff (@{const True}, t2) = t2
+ | s_iff (t1, @{const True}) = t1
+ | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+
fun monomorphic_term subst =
map_types (map_type_tvar (fn v =>
case Type.lookup subst v of
--- a/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:12:45 2011 +0200
@@ -197,8 +197,8 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- (map (introduce_combinators ctxt o snd)) false false
- [] @{prop False} props
+ (rpair [] o map (introduce_combinators ctxt))
+ false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:12:45 2011 +0200
@@ -60,8 +60,8 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
- val concealed_lambdasN : string
- val lambda_liftingN : string
+ val concealedN : string
+ val liftingN : string
val combinatorsN : string
val lambdasN : string
val smartN : string
@@ -334,8 +334,8 @@
(* configuration attributes *)
-val concealed_lambdasN = "concealed_lambdas"
-val lambda_liftingN = "lambda_lifting"
+val concealedN = "concealed"
+val liftingN = "lifting"
val combinatorsN = "combinators"
val lambdasN = "lambdas"
val smartN = "smart"
@@ -525,15 +525,6 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt ps =
- let
- val ts = map snd ps (*###*)
- in
- case SMT_Translate.lift_lambdas ctxt false ts |> snd of
- (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
- | (defs, ts) => ts @ defs
- end
-
fun translate_atp_lambdas ctxt type_enc =
Config.get ctxt atp_lambda_translation
|> (fn trans =>
@@ -546,14 +537,14 @@
else
trans)
|> (fn trans =>
- if trans = concealed_lambdasN then
- map (conceal_lambdas ctxt o snd)
- else if trans = lambda_liftingN then
- lift_lambdas ctxt
+ if trans = concealedN then
+ rpair [] o map (conceal_lambdas ctxt)
+ else if trans = liftingN then
+ SMT_Translate.lift_lambdas ctxt false #> snd #> swap
else if trans = combinatorsN then
- map (introduce_combinators ctxt o snd)
+ rpair [] o map (introduce_combinators ctxt)
else if trans = lambdasN then
- map (Envir.eta_contract o snd)
+ rpair [] o map (Envir.eta_contract)
else
error ("Unknown lambda translation method: " ^ quote trans ^ "."))