fixed lambda-liftg: must ensure the formulas are in close form
authorblanchet
Sun Jul 17 14:21:19 2011 +0200 (2011-07-17)
changeset 4386458a7b3fdc193
parent 43863 a43d61270142
child 43869 58be172c6ca4
fixed lambda-liftg: must ensure the formulas are in close form
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:12:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:21:19 2011 +0200
     1.3 @@ -940,17 +940,18 @@
     1.4  
     1.5  fun do_introduce_combinators ctxt Ts t =
     1.6    let val thy = Proof_Context.theory_of ctxt in
     1.7 -    t |> conceal_bounds Ts
     1.8 -      |> cterm_of thy
     1.9 -      |> Meson_Clausify.introduce_combinators_in_cterm
    1.10 -      |> prop_of |> Logic.dest_equals |> snd
    1.11 -      |> reveal_bounds Ts
    1.12 +    t |> not (Meson.is_fol_term thy t)
    1.13 +         ? (conceal_bounds Ts
    1.14 +            #> cterm_of thy
    1.15 +            #> Meson_Clausify.introduce_combinators_in_cterm
    1.16 +            #> prop_of #> Logic.dest_equals #> snd
    1.17 +            #> reveal_bounds Ts)
    1.18    end
    1.19    (* A type variable of sort "{}" will make abstraction fail. *)
    1.20 -  handle THM _ => do_conceal_lambdas Ts t
    1.21 +  handle THM _ => t |> do_conceal_lambdas Ts
    1.22  val introduce_combinators = simple_translate_lambdas do_introduce_combinators
    1.23  
    1.24 -fun preprocess_abstractions_in_terms ctxt trans_lambdas facts =
    1.25 +fun preprocess_abstractions_in_terms trans_lambdas facts =
    1.26    let
    1.27      val (facts, lambda_ts) =
    1.28        facts |> map (snd o snd) |> trans_lambdas 
    1.29 @@ -1440,26 +1441,28 @@
    1.30      val hyp_ts =
    1.31        hyp_ts
    1.32        |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
    1.33 -    val fact_ps = facts |> map (apsnd (pair Axiom))
    1.34 -    val conj_ps =
    1.35 +    val facts = facts |> map (apsnd (pair Axiom))
    1.36 +    val conjs =
    1.37        map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
    1.38        |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
    1.39 -    val ((conj_ps, fact_ps), lambda_ps) =
    1.40 -      conj_ps @ fact_ps
    1.41 -      |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
    1.42 -      |> (if preproc then preprocess_abstractions_in_terms ctxt trans_lambdas
    1.43 -          else rpair [])
    1.44 -      |>> chop (length conj_ps)
    1.45 -      |>> preproc ? apfst (map (apsnd (apsnd freeze_term)))
    1.46 -    val conjs = make_conjecture ctxt format type_enc conj_ps
    1.47 +    val ((conjs, facts), lambdas) =
    1.48 +      if preproc then
    1.49 +        conjs @ facts
    1.50 +        |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
    1.51 +        |> preprocess_abstractions_in_terms trans_lambdas
    1.52 +        |>> chop (length conjs)
    1.53 +        |>> apfst (map (apsnd (apsnd freeze_term)))
    1.54 +      else
    1.55 +        ((conjs, facts), [])
    1.56 +    val conjs = conjs |> make_conjecture ctxt format type_enc
    1.57      val (fact_names, facts) =
    1.58 -      fact_ps
    1.59 +      facts
    1.60        |> map_filter (fn (name, (_, t)) =>
    1.61                          make_fact ctxt format type_enc true (name, t)
    1.62                          |> Option.map (pair name))
    1.63        |> ListPair.unzip
    1.64      val lambdas =
    1.65 -      lambda_ps |> map_filter (make_fact ctxt format type_enc false o apsnd snd)
    1.66 +      lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
    1.67      val all_ts = concl_t :: hyp_ts @ fact_ts
    1.68      val subs = tfree_classes_of_terms all_ts
    1.69      val supers = tvar_classes_of_terms all_ts
    1.70 @@ -1581,8 +1584,7 @@
    1.71     the remote provers might care. *)
    1.72  fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
    1.73          type_enc (j, {name, locality, kind, iformula, atomic_types}) =
    1.74 -  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
    1.75 -   kind,
    1.76 +  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
    1.77     iformula
    1.78     |> close_iformula_universally
    1.79     |> formula_from_iformula ctxt format nonmono_Ts type_enc
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:12:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:21:19 2011 +0200
     2.3 @@ -28,6 +28,7 @@
     2.4    val s_disj : term * term -> term
     2.5    val s_imp : term * term -> term
     2.6    val s_iff : term * term -> term
     2.7 +  val close_form : term -> term
     2.8    val monomorphic_term : Type.tyenv -> term -> term
     2.9    val eta_expand : typ list -> term -> int -> term
    2.10    val transform_elim_prop : term -> term
    2.11 @@ -236,6 +237,11 @@
    2.12    | s_iff (t1, @{const True}) = t1
    2.13    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    2.14  
    2.15 +fun close_form t =
    2.16 +  fold (fn ((x, i), T) => fn t' =>
    2.17 +           HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    2.18 +       (Term.add_vars t []) t
    2.19 +
    2.20  fun monomorphic_term subst =
    2.21    map_types (map_type_tvar (fn v =>
    2.22        case Type.lookup subst v of
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:12:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:21:19 2011 +0200
     3.3 @@ -532,15 +532,16 @@
     3.4             if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
     3.5           else if trans = lambdasN andalso
     3.6                   not (is_type_enc_higher_order type_enc) then
     3.7 -           error ("Lambda translation method incompatible with \
     3.8 -                  \first-order encoding.")
     3.9 +           error ("Lambda translation method incompatible with first-order \
    3.10 +                  \encoding.")
    3.11           else
    3.12             trans)
    3.13    |> (fn trans =>
    3.14           if trans = concealedN then
    3.15             rpair [] o map (conceal_lambdas ctxt)
    3.16           else if trans = liftingN then
    3.17 -           SMT_Translate.lift_lambdas ctxt false #> snd #> swap
    3.18 +           map (close_form o Envir.eta_contract)
    3.19 +           #> SMT_Translate.lift_lambdas ctxt false #> snd #> swap
    3.20           else if trans = combinatorsN then
    3.21             rpair [] o map (introduce_combinators ctxt)
    3.22           else if trans = lambdasN then
     4.1 --- a/src/HOL/Tools/refute.ML	Sun Jul 17 14:12:45 2011 +0200
     4.2 +++ b/src/HOL/Tools/refute.ML	Sun Jul 17 14:21:19 2011 +0200
     4.3 @@ -62,7 +62,6 @@
     4.4  (* Additional functions used by Nitpick (to be factored out)                 *)
     4.5  (* ------------------------------------------------------------------------- *)
     4.6  
     4.7 -  val close_form : term -> term
     4.8    val get_classdef : theory -> string -> (string * term) option
     4.9    val norm_rhs : term -> term
    4.10    val get_def : theory -> string * typ -> (string * term) option