# HG changeset patch # User blanchet # Date 1310905279 -7200 # Node ID 58a7b3fdc193cab136b1f01c5858ace8873c2084 # Parent a43d6127014225bb5c2511da29ee88d1ef885e01 fixed lambda-liftg: must ensure the formulas are in close form diff -r a43d61270142 -r 58a7b3fdc193 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:12:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:21:19 2011 +0200 @@ -940,17 +940,18 @@ fun do_introduce_combinators ctxt Ts t = let val thy = Proof_Context.theory_of ctxt in - t |> conceal_bounds Ts - |> cterm_of thy - |> Meson_Clausify.introduce_combinators_in_cterm - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts + t |> not (Meson.is_fol_term thy t) + ? (conceal_bounds Ts + #> cterm_of thy + #> Meson_Clausify.introduce_combinators_in_cterm + #> prop_of #> Logic.dest_equals #> snd + #> reveal_bounds Ts) end (* A type variable of sort "{}" will make abstraction fail. *) - handle THM _ => do_conceal_lambdas Ts t + handle THM _ => t |> do_conceal_lambdas Ts val introduce_combinators = simple_translate_lambdas do_introduce_combinators -fun preprocess_abstractions_in_terms ctxt trans_lambdas facts = +fun preprocess_abstractions_in_terms trans_lambdas facts = let val (facts, lambda_ts) = facts |> map (snd o snd) |> trans_lambdas @@ -1440,26 +1441,28 @@ val hyp_ts = hyp_ts |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t) - val fact_ps = facts |> map (apsnd (pair Axiom)) - val conj_ps = + val facts = facts |> map (apsnd (pair Axiom)) + val conjs = map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)] |> 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 ((conjs, facts), lambdas) = + if preproc then + conjs @ facts + |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts))) + |> preprocess_abstractions_in_terms trans_lambdas + |>> chop (length conjs) + |>> apfst (map (apsnd (apsnd freeze_term))) + else + ((conjs, facts), []) + val conjs = conjs |> make_conjecture ctxt format type_enc val (fact_names, facts) = - fact_ps + facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t) |> Option.map (pair name)) |> ListPair.unzip val lambdas = - lambda_ps |> map_filter (make_fact ctxt format type_enc false o apsnd snd) + lambdas |> 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 @@ -1581,8 +1584,7 @@ the remote provers might care. *) fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts type_enc (j, {name, locality, kind, iformula, atomic_types}) = - (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, - kind, + (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, iformula |> close_iformula_universally |> formula_from_iformula ctxt format nonmono_Ts type_enc diff -r a43d61270142 -r 58a7b3fdc193 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sun Jul 17 14:12:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Sun Jul 17 14:21:19 2011 +0200 @@ -28,6 +28,7 @@ val s_disj : term * term -> term val s_imp : term * term -> term val s_iff : term * term -> term + val close_form : term -> term val monomorphic_term : Type.tyenv -> term -> term val eta_expand : typ list -> term -> int -> term val transform_elim_prop : term -> term @@ -236,6 +237,11 @@ | s_iff (t1, @{const True}) = t1 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 +fun close_form t = + fold (fn ((x, i), T) => fn t' => + HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) + (Term.add_vars t []) t + fun monomorphic_term subst = map_types (map_type_tvar (fn v => case Type.lookup subst v of diff -r a43d61270142 -r 58a7b3fdc193 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:12:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:21:19 2011 +0200 @@ -532,15 +532,16 @@ if is_type_enc_higher_order type_enc then lambdasN else combinatorsN else if trans = lambdasN andalso not (is_type_enc_higher_order type_enc) then - error ("Lambda translation method incompatible with \ - \first-order encoding.") + error ("Lambda translation method incompatible with first-order \ + \encoding.") else trans) |> (fn trans => if trans = concealedN then rpair [] o map (conceal_lambdas ctxt) else if trans = liftingN then - SMT_Translate.lift_lambdas ctxt false #> snd #> swap + map (close_form o Envir.eta_contract) + #> SMT_Translate.lift_lambdas ctxt false #> snd #> swap else if trans = combinatorsN then rpair [] o map (introduce_combinators ctxt) else if trans = lambdasN then diff -r a43d61270142 -r 58a7b3fdc193 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sun Jul 17 14:12:45 2011 +0200 +++ b/src/HOL/Tools/refute.ML Sun Jul 17 14:21:19 2011 +0200 @@ -62,7 +62,6 @@ (* Additional functions used by Nitpick (to be factored out) *) (* ------------------------------------------------------------------------- *) - val close_form : term -> term val get_classdef : theory -> string -> (string * term) option val norm_rhs : term -> term val get_def : theory -> string * typ -> (string * term) option