# HG changeset patch # User blanchet # Date 1405157483 -7200 # Node ID 677b07d777c3caba72c05301c2851e9d864e6c7a # Parent 2b561e7a0512ec79c3cf7602b921f049c855e242 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax diff -r 2b561e7a0512 -r 677b07d777c3 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Sat Jul 12 11:31:22 2014 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Sat Jul 12 11:31:23 2014 +0200 @@ -62,11 +62,16 @@ end -(** Nitpick (alias Nitrox) **) +(** Nitpick **) fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1 | aptrueprop f t = f t +fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t + | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) = + (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u) + | is_legitimate_tptp_def _ = false + fun nitpick_tptp_file thy timeout file_name = let val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name @@ -74,7 +79,7 @@ val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I)) - |> List.partition (ATP_Util.is_legitimate_tptp_def + |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop) o ATP_Util.unextensionalize_def) val nondefs = pseudo_defs @ nondefs diff -r 2b561e7a0512 -r 677b07d777c3 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Jul 12 11:31:22 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Jul 12 11:31:23 2014 +0200 @@ -1275,30 +1275,17 @@ {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts} end -fun is_format_with_defs (THF _) = true - | is_format_with_defs _ = false - -fun make_fact ctxt format type_enc iff_for_eq ((name, stature as (_, status)), t) = - let - val role = - if is_format_with_defs format andalso status = Non_Rec_Def andalso - is_legitimate_tptp_def t then - Definition - else - Axiom - in - (case make_formula ctxt format type_enc iff_for_eq name stature role t of - formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => - if s = tptp_true then NONE else SOME formula - | formula => SOME formula) - end +fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) = + (case make_formula ctxt format type_enc iff_for_eq name stature Axiom t of + formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => + if s = tptp_true then NONE else SOME formula + | formula => SOME formula) fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (role, t)) => - let - val role' = if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role - val t' = t |> role' = Conjecture ? s_not - in make_formula ctxt format type_enc true name stature role' t' end) + let val t' = t |> role = Conjecture ? s_not in + make_formula ctxt format type_enc true name stature role t' + end) (** Finite and infinite type inference **) diff -r 2b561e7a0512 -r 677b07d777c3 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Jul 12 11:31:22 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Jul 12 11:31:23 2014 +0200 @@ -132,8 +132,7 @@ Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a, (if null clss then @{sort type} else map class_of_atp_class clss)))) end - | typ_of_atp_type ctxt (ty as AFun (a, tys)) = - (typ_of_atp_type ctxt a) --> (typ_of_atp_type ctxt tys) + | typ_of_atp_type ctxt (AFun (a, tys)) = typ_of_atp_type ctxt a --> typ_of_atp_type ctxt tys fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us) @@ -253,7 +252,7 @@ (case unprefix_and_unascii const_prefix s of SOME s' => let - val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const + val ((s', _), mangled_us) = s' |> unmangled_const |>> `invert_const val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term NONE) term_us @@ -475,25 +474,11 @@ fun is_axiom_used_in_proof pred = exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) -fun add_non_rec_defs facts = - fold (fn fact as (_, (_, status)) => status = Non_Rec_Def ? insert (op =) fact) facts - val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" -val leo2_unfold_def_rule = "unfold_def" fun add_fact ctxt facts ((_, ss), _, _, rule, deps) = - (if rule = leo2_extcnf_equal_neg_rule then + (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then insert (op =) (short_thm_name ctxt ext, (Global, General)) - else if rule = leo2_unfold_def_rule then - (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP - proof. Remove the next line once this is fixed. *) - add_non_rec_defs facts - else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then - (fn [] => - (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we - assume the worst and include them all here. *) - [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs facts - | facts => facts) else I) #> (if null deps then union (op =) (resolve_facts facts ss) else I) diff -r 2b561e7a0512 -r 677b07d777c3 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Jul 12 11:31:22 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Jul 12 11:31:23 2014 +0200 @@ -190,8 +190,6 @@ (* Alt-Ergo *) -val alt_ergo_tff1 = TFF Polymorphic - val alt_ergo_config : atp_config = {exec = K (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => @@ -205,7 +203,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))], + [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -593,8 +591,6 @@ (* Zipperposition*) -val zipperposition_tff1 = TFF Polymorphic - val zipperposition_config : atp_config = {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => @@ -605,7 +601,7 @@ prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) - [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))], + [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} diff -r 2b561e7a0512 -r 677b07d777c3 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sat Jul 12 11:31:22 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Sat Jul 12 11:31:23 2014 +0200 @@ -45,7 +45,6 @@ val cong_extensionalize_term : theory -> term -> term val abs_extensionalize_term : Proof.context -> term -> term val unextensionalize_def : term -> term - val is_legitimate_tptp_def : term -> bool val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term @@ -382,12 +381,6 @@ | _ => t) | _ => t -fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t - | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) = - (is_Const t orelse is_Free t) andalso - not (exists_subterm (curry (op =) t) u) - | is_legitimate_tptp_def _ = false - (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to "False". (Cf. "transform_elim_theorem" in