# HG changeset patch # User blanchet # Date 1310904765 -7200 # Node ID a43d6127014225bb5c2511da29ee88d1ef885e01 # Parent a14fdb8c0497f79c54b27a2116cb9985f0ccce77 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) diff -r a14fdb8c0497 -r a43d61270142 src/HOL/TPTP/atp_export.ML --- 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))) diff -r a14fdb8c0497 -r a43d61270142 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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 diff -r a14fdb8c0497 -r a43d61270142 src/HOL/Tools/ATP/atp_translate.ML --- 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)) = diff -r a14fdb8c0497 -r a43d61270142 src/HOL/Tools/ATP/atp_util.ML --- 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 diff -r a14fdb8c0497 -r a43d61270142 src/HOL/Tools/Metis/metis_translate.ML --- 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)) diff -r a14fdb8c0497 -r a43d61270142 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 ^ "."))