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