--- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -114,7 +114,7 @@
val type_consts_of_terms : theory -> term list -> string list
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_system
- -> bool option -> bool -> term list -> term
+ -> bool option -> bool -> bool -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
* (string * 'a) list vector * int list * int Symtab.table
@@ -796,7 +796,8 @@
#>> uncurry (mk_aconn c)
and do_formula bs t =
case t of
- @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
+ @{const Trueprop} $ t1 => do_formula bs t1
+ | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
| Const (@{const_name All}, _) $ Abs (s, T, t') =>
do_quant bs AForall s T t'
| Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
@@ -879,22 +880,25 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
-(* making fact and conjecture formulas *)
-fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =
+fun preprocess_prop ctxt presimp kind t =
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
|> transform_elim_prop
|> Object_Logic.atomize_term thy
val need_trueprop = (fastype_of t = @{typ bool})
- val t = t |> need_trueprop ? HOLogic.mk_Trueprop
- |> Raw_Simplifier.rewrite_term thy
- (Meson.unfold_set_const_simps ctxt) []
- |> extensionalize_term ctxt
- |> presimp ? presimplify_term ctxt
- |> perhaps (try (HOLogic.dest_Trueprop))
- |> introduce_combinators_in_term ctxt kind
- |> kind <> Axiom ? freeze_term
+ in
+ t |> need_trueprop ? HOLogic.mk_Trueprop
+ |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
+ |> extensionalize_term ctxt
+ |> presimp ? presimplify_term ctxt
+ |> introduce_combinators_in_term ctxt kind
+ |> kind <> Axiom ? freeze_term
+ end
+
+(* making fact and conjecture formulas *)
+fun make_formula thy format type_sys eq_as_iff name loc kind t =
+ let
val (combformula, atomic_types) =
combformula_from_prop thy format type_sys eq_as_iff t []
in
@@ -902,16 +906,23 @@
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp
+fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
((name, loc), t) =
- case (keep_trivial,
- make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
- (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
- if s = tptp_true then NONE else SOME formula
- | (_, formula) => SOME formula
+ let val thy = Proof_Context.theory_of ctxt in
+ case (keep_trivial,
+ t |> preproc ? preprocess_prop ctxt presimp Axiom
+ |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
+ (false,
+ formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
+ if s = tptp_true then NONE else SOME formula
+ | (_, formula) => SOME formula
+ end
-fun make_conjecture ctxt format prem_kind type_sys ts =
- let val last = length ts - 1 in
+fun make_conjecture ctxt format prem_kind type_sys preproc ts =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val last = length ts - 1
+ in
map2 (fn j => fn t =>
let
val (kind, maybe_negate) =
@@ -922,8 +933,9 @@
if prem_kind = Conjecture then update_combformula mk_anot
else I)
in
- t |> make_formula ctxt format type_sys true true
- (string_of_int j) General kind
+ t |> preproc ? preprocess_prop ctxt true kind
+ |> make_formula thy format type_sys true (string_of_int j)
+ General kind
|> maybe_negate
end)
(0 upto last) ts
@@ -1273,7 +1285,7 @@
| _ => I)
end)
fun make_facts eq_as_iff =
- map_filter (make_fact ctxt format type_sys false eq_as_iff false)
+ map_filter (make_fact ctxt format type_sys true false eq_as_iff false)
val fairly_sound = is_type_sys_fairly_sound type_sys
in
helper_table
@@ -1292,7 +1304,7 @@
[]
fun translate_atp_fact ctxt format type_sys keep_trivial =
- `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)
+ `(make_fact ctxt format type_sys keep_trivial true true true o apsnd prop_of)
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
@@ -1331,8 +1343,7 @@
fun type_consts_of_terms thy ts =
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)
-
-fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
+fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
rich_facts =
let
val thy = Proof_Context.theory_of ctxt
@@ -1351,7 +1362,8 @@
val supers = tvar_classes_of_terms all_ts
val tycons = type_consts_of_terms thy all_ts
val conjs =
- hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys
+ hyp_ts @ [concl_t]
+ |> make_conjecture ctxt format prem_kind type_sys preproc
val (supers', arity_clauses) =
if level_of_type_sys type_sys = No_Types then ([], [])
else make_arity_clauses thy tycons supers
@@ -1745,10 +1757,12 @@
val free_typesN = "Type variables"
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
- explicit_apply readable_names hyp_ts concl_t facts =
+ explicit_apply readable_names preproc hyp_ts concl_t
+ facts =
let
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
+ translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
+ facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -44,8 +44,8 @@
val metis_name_table =
[((tptp_equal, 2), metis_equal),
((tptp_old_equal, 2), metis_equal),
- ((predicator_name, 1), metis_predicator),
- ((app_op_name, 2), metis_app_op)]
+ ((const_prefix ^ predicator_name, 1), metis_predicator),
+ ((const_prefix ^ app_op_name, 2), metis_app_op)]
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
| predicate_of thy (t, pos) =
@@ -314,9 +314,8 @@
val clauses = conj_clauses @ fact_clauses
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys
- explicit_apply false (map prop_of clauses)
+ explicit_apply false false (map prop_of clauses)
@{prop False} []
- (* val _ = tracing (PolyML.makestring atp_problem) FIXME ### *)
val axioms =
atp_problem
|> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 31 16:38:36 2011 +0200
@@ -667,7 +667,8 @@
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
type_sys explicit_apply
- (Config.get ctxt atp_readable_names) hyp_ts concl_t facts
+ (Config.get ctxt atp_readable_names) true hyp_ts concl_t
+ facts
fun weights () = atp_problem_weights atp_problem
val core =
File.shell_path command ^ " " ^