1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
1.3 @@ -993,41 +993,25 @@
1.4 atomic_types = atomic_types}
1.5 end
1.6
1.7 -fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc
1.8 - presimp_consts ((name, loc), t) =
1.9 +fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
1.10 let val thy = Proof_Context.theory_of ctxt in
1.11 - case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
1.12 - |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1.13 + case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1.14 loc Axiom of
1.15 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1.16 if s = tptp_true then NONE else SOME formula
1.17 | formula => SOME formula
1.18 end
1.19
1.20 -fun make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc
1.21 - presimp_consts ts =
1.22 +fun make_conjecture ctxt format type_enc ps =
1.23 let
1.24 val thy = Proof_Context.theory_of ctxt
1.25 - val last = length ts - 1
1.26 + val last = length ps - 1
1.27 in
1.28 - map2 (fn j => fn t =>
1.29 - let
1.30 - val (kind, maybe_negate) =
1.31 - if j = last then
1.32 - (Conjecture, I)
1.33 - else
1.34 - (prem_kind,
1.35 - if prem_kind = Conjecture then update_iformula mk_anot
1.36 - else I)
1.37 - in
1.38 - t |> preproc ?
1.39 - (preprocess_prop ctxt trans_lambdas presimp_consts kind
1.40 - #> freeze_term)
1.41 - |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1.42 - Local kind
1.43 - |> maybe_negate
1.44 - end)
1.45 - (0 upto last) ts
1.46 + map2 (fn j => fn (kind, t) =>
1.47 + t |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1.48 + Local kind
1.49 + |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
1.50 + (0 upto last) ps
1.51 end
1.52
1.53 (** Finite and infinite type inference **)
1.54 @@ -1386,8 +1370,7 @@
1.55 [t]
1.56 end
1.57 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1.58 - val make_facts =
1.59 - map_filter (make_fact ctxt format type_enc I false false [])
1.60 + val make_facts = map_filter (make_fact ctxt format type_enc false)
1.61 val fairly_sound = is_type_enc_fairly_sound type_enc
1.62 in
1.63 helper_table
1.64 @@ -1449,10 +1432,12 @@
1.65 val thy = Proof_Context.theory_of ctxt
1.66 val fact_ts = facts |> map snd
1.67 val presimp_consts = Meson.presimplified_consts ctxt
1.68 - val make_fact =
1.69 - make_fact ctxt format type_enc trans_lambdas true preproc presimp_consts
1.70 + val preprocess = preprocess_prop ctxt trans_lambdas presimp_consts
1.71 val (facts, fact_names) =
1.72 - facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1.73 + facts |> map (fn (name, t) =>
1.74 + (name, t |> preproc ? preprocess Axiom)
1.75 + |> make_fact ctxt format type_enc true
1.76 + |> rpair name)
1.77 |> map_filter (try (apfst the))
1.78 |> ListPair.unzip
1.79 (* Remove existing facts from the conjecture, as this can dramatically
1.80 @@ -1466,9 +1451,10 @@
1.81 val supers = tvar_classes_of_terms all_ts
1.82 val tycons = type_constrs_of_terms thy all_ts
1.83 val conjs =
1.84 - hyp_ts @ [concl_t]
1.85 - |> make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc
1.86 - presimp_consts
1.87 + map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
1.88 + |> preproc
1.89 + ? map (fn (kind, t) => (kind, t |> preprocess kind |> freeze_term))
1.90 + |> make_conjecture ctxt format type_enc
1.91 val (supers', arity_clauses) =
1.92 if level_of_type_enc type_enc = No_Types then ([], [])
1.93 else make_arity_clauses thy tycons supers
1.94 @@ -1542,8 +1528,7 @@
1.95 and formula_from_iformula ctxt format nonmono_Ts type_enc
1.96 should_predicate_on_var =
1.97 let
1.98 - fun do_term pos =
1.99 - ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.100 + val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level
1.101 val do_bound_type =
1.102 case type_enc of
1.103 Simple_Types (_, level) =>