1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:38 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 21 17:17:39 2011 +0200
1.3 @@ -1474,9 +1474,9 @@
1.4 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1.5 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1.6 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1.7 -fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
1.8 - | is_var_nonmonotonic_in_formula pos phi _ name =
1.9 +fun should_predicate_on_var_in_formula pos phi (SOME true) name =
1.10 formula_fold pos (is_var_positively_naked_in_term name) phi false
1.11 + | should_predicate_on_var_in_formula _ _ _ _ = true
1.12
1.13 fun mk_const_aterm format type_sys x T_args args =
1.14 ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
1.15 @@ -1548,34 +1548,33 @@
1.16 end
1.17 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1.18 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1.19 - in do_formula o SOME end
1.20 + in do_formula end
1.21
1.22 fun bound_tvars type_sys Ts =
1.23 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1.24 (type_literals_for_types type_sys add_sorts_on_tvar Ts))
1.25
1.26 -fun formula_for_fact ctxt format nonmono_Ts type_sys
1.27 - ({combformula, atomic_types, ...} : translated_formula) =
1.28 - combformula
1.29 - |> close_combformula_universally
1.30 - |> formula_from_combformula ctxt format nonmono_Ts type_sys
1.31 - is_var_nonmonotonic_in_formula true
1.32 - |> bound_tvars type_sys atomic_types
1.33 - |> close_formula_universally
1.34 -
1.35 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1.36 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1.37 the remote provers might care. *)
1.38 -fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
1.39 - (j, formula as {name, locality, kind, ...}) =
1.40 - Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
1.41 - encode name,
1.42 - kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
1.43 - case locality of
1.44 - Intro => intro_info
1.45 - | Elim => elim_info
1.46 - | Simp => simp_info
1.47 - | _ => NONE)
1.48 +fun formula_line_for_fact ctxt format prefix encode exporter nonmono_Ts type_sys
1.49 + (j, {name, locality, kind, combformula, atomic_types}) =
1.50 + (prefix ^ (if exporter then "" else string_of_int j ^ "_") ^ encode name,
1.51 + kind,
1.52 + combformula
1.53 + |> close_combformula_universally
1.54 + |> formula_from_combformula ctxt format nonmono_Ts type_sys
1.55 + should_predicate_on_var_in_formula
1.56 + (if exporter then NONE else SOME true)
1.57 + |> bound_tvars type_sys atomic_types
1.58 + |> close_formula_universally,
1.59 + NONE,
1.60 + case locality of
1.61 + Intro => intro_info
1.62 + | Elim => elim_info
1.63 + | Simp => simp_info
1.64 + | _ => NONE)
1.65 + |> Formula
1.66
1.67 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
1.68 : class_rel_clause) =
1.69 @@ -1604,7 +1603,7 @@
1.70 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1.71 Formula (conjecture_prefix ^ name, kind,
1.72 formula_from_combformula ctxt format nonmono_Ts type_sys
1.73 - is_var_nonmonotonic_in_formula false
1.74 + should_predicate_on_var_in_formula (SOME false)
1.75 (close_combformula_universally combformula)
1.76 |> bound_tvars type_sys atomic_types
1.77 |> close_formula_universally, NONE, NONE)
1.78 @@ -1725,7 +1724,7 @@
1.79 |> type_pred_combterm ctxt format type_sys res_T
1.80 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1.81 |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
1.82 - (K (K (K (K true)))) true
1.83 + (K (K (K (K true)))) (SOME true)
1.84 |> n > 1 ? bound_tvars type_sys (atyps_of T)
1.85 |> close_formula_universally
1.86 |> maybe_negate,
1.87 @@ -1859,7 +1858,7 @@
1.88 val explicit_apply = NONE (* for experimental purposes *)
1.89
1.90 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
1.91 - freshen_facts readable_names preproc hyp_ts concl_t facts =
1.92 + exporter readable_names preproc hyp_ts concl_t facts =
1.93 let
1.94 val (format, type_sys) = choose_format [format] type_sys
1.95 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1.96 @@ -1887,7 +1886,7 @@
1.97 poly_nonmono_Ts type_sys
1.98 val helper_lines =
1.99 0 upto length helpers - 1 ~~ helpers
1.100 - |> map (formula_line_for_fact ctxt format helper_prefix I false
1.101 + |> map (formula_line_for_fact ctxt format helper_prefix I exporter
1.102 poly_nonmono_Ts type_sys)
1.103 |> (if needs_type_tag_idempotence type_sys then
1.104 cons (type_tag_idempotence_fact ())
1.105 @@ -1898,8 +1897,8 @@
1.106 val problem =
1.107 [(explicit_declsN, sym_decl_lines),
1.108 (factsN,
1.109 - map (formula_line_for_fact ctxt format fact_prefix ascii_of
1.110 - freshen_facts nonmono_Ts type_sys)
1.111 + map (formula_line_for_fact ctxt format fact_prefix ascii_of exporter
1.112 + nonmono_Ts type_sys)
1.113 (0 upto length facts - 1 ~~ facts)),
1.114 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1.115 (aritiesN, map formula_line_for_arity_clause arity_clauses),