# HG changeset patch # User blanchet # Date 1572005696 -7200 # Node ID 1d2b2cc792f12809e81d9607bdfbea89dd137725 # Parent 1019b860955274b8fbb5ba24123230af549c9f05 removed experimental encoding for Waldmeister diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Fri Oct 25 14:06:02 2019 +0200 +++ b/src/HOL/ATP.thy Fri Oct 25 14:14:56 2019 +0200 @@ -131,19 +131,6 @@ unfolding fFalse_def fTrue_def fequal_def by auto -subsection \Waldmeister helpers\ - -(* Has all needed simplification lemmas for logic. *) -lemma boolean_equality: "(P \ P) = True" - by simp - -lemma boolean_comm: "(P \ Q) = (Q \ P)" - by auto - -lemmas waldmeister_fol = boolean_equality boolean_comm - simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc - - subsection \Basic connection between ATPs and HOL\ ML_file \Tools/lambda_lifting.ML\ @@ -151,8 +138,5 @@ ML_file \Tools/ATP/atp_problem_generate.ML\ ML_file \Tools/ATP/atp_proof_reconstruct.ML\ ML_file \Tools/ATP/atp_systems.ML\ -ML_file \Tools/ATP/atp_waldmeister.ML\ - -hide_fact (open) waldmeister_fol boolean_equality boolean_comm end diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Oct 25 14:06:02 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Oct 25 14:14:56 2019 +0200 @@ -1697,7 +1697,7 @@ mk_atyquant AForall (map (fn TVar (z as (_, S)) => (AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts) | Native (_, Raw_Polymorphic _, _) => - mk_atyquant AForall (map (fn TVar (z as (_, S)) => (AType ((tvar_name z, []), []), [])) Ts) + mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts) | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))) fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 = diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:06:02 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:14:56 2019 +0200 @@ -65,7 +65,6 @@ val spassN : string val vampireN : string val waldmeisterN : string - val waldmeister_newN : string val z3_tptpN : string val zipperpositionN : string val remote_prefix : string @@ -136,7 +135,6 @@ val spassN = "spass" val vampireN = "vampire" val waldmeisterN = "waldmeister" -val waldmeister_newN = "waldmeister_new" val z3_tptpN = "z3_tptp" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:06:02 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:14:56 2019 +0200 @@ -797,7 +797,6 @@ remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" -val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN "mono_args" (* Setup *) @@ -836,7 +835,7 @@ [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, - remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new] + remote_vampire, remote_snark, remote_pirate, remote_waldmeister] val _ = Theory.setup (fold add_atp atps) diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/Tools/ATP/atp_waldmeister.ML --- a/src/HOL/Tools/ATP/atp_waldmeister.ML Fri Oct 25 14:06:02 2019 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,596 +0,0 @@ -(* Title: HOL/Tools/ATP/atp_waldmeister.ML - Author: Albert Steckermeier, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -General-purpose functions used by the Sledgehammer modules. -*) - -exception FailureMessage of string - -signature ATP_WALDMEISTER_SKOLEMIZER = -sig - val skolemize : bool -> Proof.context -> term -> (Proof.context * (term list * term)) -end; - -signature ATP_WALDMEISTER_TYPE_ENCODER = -sig - val encode_type : typ -> string - val decode_type_string : string -> typ - val encode_types : typ list -> string - val decode_types : string -> typ list - val encode_const : string * typ list -> string - val decode_const : string -> string * typ list -end; - -signature ATP_WALDMEISTER = -sig - type 'a atp_problem = 'a ATP_Problem.atp_problem - type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - type 'a atp_proof = 'a ATP_Proof.atp_proof - type stature = ATP_Problem_Generate.stature - type waldmeister_info = (string * (term list * (term option * term))) list - - val waldmeister_skolemize_rule : string - - val generate_waldmeister_problem : Proof.context -> term list -> term -> - ((string * stature) * term) list -> - string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * - waldmeister_info - val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof -> - (term, string) atp_step list - val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> - (term, string) atp_step list -end; - -structure ATP_Waldmeister_Skolemizer : ATP_WALDMEISTER_SKOLEMIZER = -struct - -open HOLogic - -fun contains_quantor (Const (\<^const_name>\Ex\, _) $ _) = true - | contains_quantor (Const (\<^const_name>\All\, _) $ _) = true - | contains_quantor (t1 $ t2) = contains_quantor t1 orelse contains_quantor t2 - | contains_quantor _ = false - -fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name, ty) = - let - val fun_type = (map type_of arg_trms) ---> ty - val (fun_name, _) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type) - val (_, ctxt1_new) = Variable.add_fixes [fun_name] ctxt1 - val (_, ctxt2_new) = Variable.add_fixes [fun_name] ctxt2 - in - (Term.list_comb (Free (fun_name,fun_type), arg_trms), ctxt1_new, ctxt2_new) - end - -fun skolem_free ctxt1 ctxt2 vars (bound_name, ty, trm) = - let - val (fun_trm, ctxt1_new, ctxt2_new) = - mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty) - in - (Term.subst_bounds ([fun_trm], trm), ctxt1_new, ctxt2_new) - end - -fun skolem_var ctxt (bound_name, ty, trm) = - let - val (var_name, _) = singleton (Variable.variant_frees ctxt []) (bound_name, ty) - val (_, ctxt') = Variable.add_fixes [var_name] ctxt - val var = Var ((var_name, 0), ty) - in - (Term.subst_bounds ([var], trm), ctxt', var) - end - -fun skolem_bound is_free ctxt1 ctxt2 spets vars x = - if is_free then - let - val (trm', ctxt1', ctxt2') = skolem_free ctxt1 ctxt2 vars x - in - (ctxt1', ctxt2',spets, trm', vars) - end - else - let - val (trm', ctxt2', var) = skolem_var ctxt2 x - in - (ctxt1, ctxt2', spets, trm', var :: vars) - end - -fun skolemize' pos ctxt1 ctxt2 spets vars (Const (\<^const_name>\Not\, _) $ trm') = - let - val (ctxt1', ctxt2', spets', trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm' - in - (ctxt1', ctxt2', map mk_not spets', mk_not trm'') - end - | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (\<^const_name>\HOL.eq\, t) $ a $ b)) = - if t = \<^typ>\bool \ bool \ bool\ andalso contains_quantor trm then - skolemize' pos ctxt1 ctxt2 (trm :: spets) vars (mk_conj (mk_imp (a, b), mk_imp (b, a))) - else - (ctxt1, ctxt2, spets, trm) - | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name, _) $ Abs x)) = - if name = \<^const_name>\Ex\ orelse name = \<^const_name>\All\ then - let - val is_free = (name = \<^const_name>\Ex\ andalso pos) - orelse (name = \<^const_name>\All\ andalso not pos) - val (ctxt1', ctxt2', spets', trm', vars') = - skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x - in - skolemize' pos ctxt1' ctxt2' spets' vars' trm' - end - else - (ctxt1, ctxt2, spets, trm) - | skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name, _)) $ a $ b) = - if name = \<^const_name>\conj\ orelse name = \<^const_name>\disj\ orelse - name = \<^const_name>\implies\ then - let - val pos_a = if name = \<^const_name>\implies\ then not pos else pos - val (ctxt1', ctxt2', spets', a') = skolemize' pos_a ctxt1 ctxt2 [] vars a - val (ctxt1'', ctxt2'', spets'', b') = skolemize' pos ctxt1' ctxt2' [] vars b - in - (ctxt1'', ctxt2'', - map (fn trm => c $ a' $ trm) spets'' @ map (fn trm => c $ trm $ b) spets' @ spets, - c $ a' $ b') - end - else - (ctxt1,ctxt2,spets,c $ a $ b) - | skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm) - - fun vars_of trm = - rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) trm [])); - - fun skolemize positve ctxt trm = - let - val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] (vars_of trm) trm - in - (ctxt1, (trm :: List.rev spets, skolemized_trm)) - end - -end; - -structure ATP_Waldmeister_Type_Encoder : ATP_WALDMEISTER_TYPE_ENCODER = -struct - -val delimiter = ";" -val open_paranthesis = "[" -val close_parathesis = "]" -val type_prefix = "Type" -val tfree_prefix = "TFree" -val tvar_prefix = "TVar" - -val identifier_character = not o member (op =) [delimiter, open_paranthesis, close_parathesis] - -fun encode_type (Type (name, types)) = - type_prefix ^ open_paranthesis ^ name ^ delimiter ^ - (map encode_type types |> space_implode delimiter) ^ close_parathesis -| encode_type (TFree (name, sorts)) = - tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ space_implode delimiter sorts ^ - close_parathesis -| encode_type (TVar ((name, i), sorts)) = - tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ - close_parathesis ^ delimiter ^ space_implode delimiter sorts ^ close_parathesis - -fun encode_types types = space_implode delimiter (map encode_type types) - -fun parse_identifier x = - (Scan.many identifier_character >> implode) x - -fun parse_star delim scanner x = - (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x - -fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --| - $$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x -and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --| - $$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x -and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis - |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ - close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| - $$ close_parathesis >> TVar) x -and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x - -fun parse_types x = parse_star delimiter parse_any_type x - -fun decode_type_string s = Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ - quote s)) parse_type)) (Symbol.explode s) |> fst - -fun decode_types s = Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ - quote s))) parse_types) (Symbol.explode s) |> fst - -fun encode_const (name,tys) = name ^ delimiter ^ encode_types tys - -fun parse_const s = (parse_identifier --| $$ delimiter -- parse_types) s - -fun decode_const s = Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^ - quote s))) parse_const) (Symbol.explode s) |> fst - -end; - -structure ATP_Waldmeister (*** : ATP_WALDMEISTER *) = -struct - -open ATP_Util -open ATP_Problem -open ATP_Problem_Generate -open ATP_Proof -open ATP_Proof_Reconstruct -open ATP_Waldmeister_Skolemizer -open ATP_Waldmeister_Type_Encoder -open HOLogic - -type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term -type atp_connective = ATP_Problem.atp_connective -type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula -type atp_format = ATP_Problem.atp_format -type atp_formula_role = ATP_Problem.atp_formula_role -type 'a atp_problem = 'a ATP_Problem.atp_problem -type waldmeister_info = (string * (term list * (term option * term))) list - -val const_prefix = #"c" -val var_prefix = #"V" -val free_prefix = #"v" -val conjecture_condition_name = "condition" -val waldmeister_equals = "eq" -val waldmeister_true = "true" -val waldmeister_false = "false" -val waldmeister_skolemize_rule = "waldmeister_skolemize" -val lam_lift_waldmeister_prefix = "lambda_wm" -val waldmeister_apply = "wm_apply" - -val factsN = "Relevant facts" -val helpersN = "Helper facts" -val conjN = "Conjecture" -val conj_identifier = conjecture_prefix ^ "0" - -val WM_ERROR_MSG = "Waldmeister problem generator failed: " - -(* - Some utilitary functions for translation. -*) - -fun gen_ascii_tuple str = (str, ascii_of str) - -fun mk_eq_true (trm as (Const (\<^const_name>\HOL.eq\, _) $ _ $ _)) = (NONE,trm) - | mk_eq_true trm = (SOME trm,HOLogic.mk_eq (trm, \<^term>\True\)) - -val is_lambda_name = String.isPrefix lam_lifted_poly_prefix - -fun lookup table k = - List.find (fn (key, _) => key = k) table - -fun dest_list' (f $ t) = - let - val (function, trms) = dest_list' f - in - (function, t :: trms) - end - | dest_list' t = (t,[]); - -fun dest_list trm = dest_list' trm ||> List.rev - -fun list_update x [] = [x] - | list_update (a,b) ((c,d) :: xs) = - if a = c andalso b < d then - (a,b) :: xs - else - (c,d) :: list_update (a,b) xs - -(* - Hiding partial applications in terms -*) - -fun map_minimal_app' info (trm :: trms) = - map_minimal_app' (minimal_app' info trm) trms - | map_minimal_app' info _ = info - -and minimal_app' info (trm as _ $ _) = - let - val (function, trms) = dest_list trm - val info' = map_minimal_app' info trms - in - case function of - (Const _) => list_update (function, length trms) info' | - (Free _) => list_update (function, length trms) info' | - _ => info - end - | minimal_app' info (trm as Const _) = - list_update (trm, 0) info - | minimal_app' info (trm as Free _) = - list_update (trm, 0) info - | minimal_app' info _ = info; - -fun map_minimal_app trms = map_minimal_app' [] trms - -fun mk_waldmeister_app function [] = function - | mk_waldmeister_app function (a :: args) = - let - val funT = type_of function - val argT = type_of a - val resT = dest_funT funT |> snd - val newT = funT --> argT --> resT - in - mk_waldmeister_app (Const (waldmeister_apply ^ "," ^ - encode_types [resT, argT], newT) $ function $ a) args - end - -fun hide_partial_applications info (trm as (_ $ _)) = - let - val (function, trms) = dest_list trm - val trms' = map (hide_partial_applications info) trms - in - case function of - Var _ => mk_waldmeister_app function trms' | - _ => - let - val min_args = lookup info function |> the |> snd - val args0 = List.take (trms',min_args) - val args1 = List.drop (trms',min_args) - val function' = list_comb (function,args0) - in - mk_waldmeister_app function' args1 - end - end - | hide_partial_applications _ t = t; - -fun remove_waldmeister_app ((c as Const (name, _)) $ x $ y) = - if String.isPrefix waldmeister_apply name then - remove_waldmeister_app x $ remove_waldmeister_app y - else - c $ remove_waldmeister_app x $ remove_waldmeister_app y - | remove_waldmeister_app (x $ y) = remove_waldmeister_app x $ remove_waldmeister_app y - | remove_waldmeister_app x = x - -(* - Translation from Isabelle terms to ATP terms. -*) - -fun trm_to_atp'' thy (Const (x, ty)) args = - let - val ty_args = if is_lambda_name x orelse String.isPrefix waldmeister_apply x then - [] else Sign.const_typargs thy (x, ty) - in - [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x, ty_args)), []), args)] - end - | trm_to_atp'' _ (Free (x, _)) args = - [ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)] - | trm_to_atp'' _ (Var ((x, _), _)) args = - [ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)] - | trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args) - | trm_to_atp'' _ _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Unexpected term") - -fun trm_to_atp' thy trm = trm_to_atp'' thy trm [] |> hd - -fun eq_trm_to_atp thy (Const (\<^const_name>\HOL.eq\, _) $ lhs $ rhs) = - ATerm ((("equal", "equal"), []), [trm_to_atp' thy lhs, trm_to_atp' thy rhs]) - | eq_trm_to_atp _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Non-eq term") - -(* Translation from ATP terms to Isabelle terms. *) - -fun construct_term thy (name, args) = - let - val prefix = String.sub (name, 0) - val encoded_name = String.extract(name, 1, NONE) - fun dummy_fun_type () = replicate (length args) dummyT ---> dummyT - in - if prefix = const_prefix then - let - val (const_name, ty_args) = if String.isPrefix waldmeister_apply encoded_name then - (waldmeister_apply, []) else decode_const encoded_name - val const_trans_name = - if is_lambda_name const_name then - lam_lift_waldmeister_prefix ^ (* ?? *) - String.extract(const_name, size lam_lifted_poly_prefix, NONE) - else - const_name - in - Const (const_trans_name, - if is_lambda_name const_name orelse String.isPrefix waldmeister_apply const_name then - dummyT - else - Sign.const_instance thy (const_name, ty_args)) - end - else if prefix = free_prefix then - Free (encoded_name, dummy_fun_type ()) - else if Char.isUpper prefix then - Var ((name, 0), dummy_fun_type ()) - (* Use name instead of encoded_name because Waldmeister renames free variables. *) - else if name = waldmeister_equals then - (case args of - [_, _] => eq_const dummyT - | _ => raise FailureMessage - (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ - Int.toString (length args))) - else if name = waldmeister_true then - \<^term>\True\ - else if name = waldmeister_false then - \<^term>\False\ - else - raise FailureMessage - (WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name) - end - -and atp_to_trm' thy (ATerm ((name,_), args)) = - (case args of - [] => construct_term thy (name, args) - | _ => Term.list_comb (construct_term thy (name, args), map (atp_to_trm' thy) args)) - | atp_to_trm' _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm' expects ATerm") - -fun atp_to_trm thy (ATerm (("equal", _), [lhs, rhs])) = - mk_eq (atp_to_trm' thy lhs, atp_to_trm' thy rhs) - | atp_to_trm _ (ATerm (("$true", _), _)) = \<^term>\True\ - | atp_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm expects ATerm") - -fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy - | formula_to_trm thy (AConn (ANot, [aterm])) = - mk_not (formula_to_trm thy aterm) - | formula_to_trm _ _ = - raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn") - -(* Abstract translation *) - -fun mk_formula prefix_name name atype aterm = - Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, []) - -fun problem_lines_of_fact thy prefix (s, (_, (_, t))) = - mk_formula (prefix ^ "0_") s Axiom (eq_trm_to_atp thy t) - -fun make_nice problem = nice_atp_problem true CNF problem - -fun mk_conjecture aterm = - let - val formula = mk_anot (AAtom aterm) - in - Formula ((conj_identifier, ""), Hypothesis, formula, NONE, []) - end - -fun generate_waldmeister_problem ctxt hyps_t0 concl_t0 facts0 = - let - val thy = Proof_Context.theory_of ctxt - - val preproc = Object_Logic.atomize_term ctxt - - val conditions = map preproc hyps_t0 - val consequence = preproc concl_t0 - val facts = map (apsnd preproc #> apfst fst) facts0 : (string * term) list - - fun map_ctxt' _ ctxt [] ys = (ctxt, ys) - | map_ctxt' f ctxt (x :: xs) ys = - let - val (ctxt', x') = f ctxt x - in - map_ctxt' f ctxt' xs (x' :: ys) - end - - fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs [] - - fun skolemize_fact ctxt (name, trm) = - let - val (ctxt', (steps, trm')) = skolemize true ctxt trm - in - (ctxt', (name, (steps, trm'))) - end - - fun name_list' _ [] _ = [] - | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1) - - fun name_list prefix xs = name_list' prefix xs 0 - - (* Skolemization, hiding lambdas and translating formulas to equations *) - val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts - val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions - - val post_skolem = do_cheaply_conceal_lambdas [] - - val sko_eq_facts0 = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts - val sko_eq_conditions0 = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions - |> name_list conjecture_condition_name - val (_, eq_conseq as (_, (non_eq_consequence0, eq_consequence0))) = - skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) - - val sko_eq_info = - (((conj_identifier, eq_conseq) :: sko_eq_conditions0) - @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0) - - (* Translation of partial function applications *) - val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info) - - fun hide_partial_apps_in_last (x, (y, (z, term))) = - (x, (y, (z, hide_partial_applications fun_app_info term))) - - val sko_eq_facts = map hide_partial_apps_in_last sko_eq_facts0 - val sko_eq_conditions = map hide_partial_apps_in_last sko_eq_conditions0 - val eq_consequence = hide_partial_applications fun_app_info eq_consequence0 - - (* Problem creation *) - val fact_lines = map (problem_lines_of_fact thy fact_prefix) sko_eq_facts - val condition_lines = - map (fn (name, (_, (_, trm))) => - mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions - val axiom_lines = fact_lines @ condition_lines - - val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence) - - val helper_lemmas_needed = exists (snd #> snd #> fst #> is_some) sko_eq_facts - orelse exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse - is_some non_eq_consequence0 - - val helper_lines = - if helper_lemmas_needed then - [(helpersN, - @{thms waldmeister_fol} - |> map (fn th => (("", (Global, General)), preproc (Thm.prop_of th))) - |> map (fn ((s, _) ,t) => mk_formula helper_prefix s Axiom (eq_trm_to_atp thy t)))] - else - [] - - val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] - - val (nice_problem, pool) = make_nice problem - in - (nice_problem, Option.map snd pool |> the_default Symtab.empty, [], Symtab.empty, sko_eq_info) - end - -fun termify_line ctxt (name, role, u, rule, deps) = - let - val thy = Proof_Context.theory_of ctxt - val t = u |> formula_to_trm thy |> remove_waldmeister_app - |> singleton (infer_formulas_types ctxt) - |> HOLogic.mk_Trueprop - in - (name, role, t, rule, deps) - end - -fun termify_waldmeister_proof ctxt pool = - nasty_atp_proof pool - #> map (termify_line ctxt) - #> repair_waldmeister_endgame - -fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of - SOME x => x | - NONE => NONE - -fun fix_name name = - if String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then - String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> - (fn x => fact_prefix ^ "0_" ^ x) - else - name - -fun skolemization_steps info - (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) = - case get_skolem_info info (map fix_name isabelle_names) of - NONE => [proof_step] | - SOME (_, ([], _)) => [proof_step] | - SOME (_, (step :: steps,_)) => - let - val raw_trm = dest_Trueprop trm - val is_narrowing = raw_trm = \<^term>\True = False\ orelse raw_trm = \<^term>\False = True\ - val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name andalso not is_narrowing - in - if is_narrowing then - [proof_step] - else - let - fun mk_steps _ [] = [] - | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]), - Plain, mk_Trueprop ((is_conjecture ? mk_not) x), waldmeister_skolemize_rule, - [(waldmeister_name ^ "_" ^ Int.toString (i-1), - if i = 1 then isabelle_names else [])]) - :: mk_steps (i+1) xs - - val first_step = ((waldmeister_name ^ "_0", isabelle_names), Unknown, - mk_Trueprop ((is_conjecture ? mk_not) step), rule, []) - - val sub_steps = mk_steps 1 steps - - val skolem_steps = first_step :: sub_steps - val num_of_steps = length skolem_steps - in - (skolem_steps @ - [((waldmeister_name, []), Unknown, trm, waldmeister_skolemize_rule, - [(waldmeister_name ^ "_" ^ Int.toString (num_of_steps - 1), - if num_of_steps = 1 then isabelle_names else [])])]) - end - end - -fun introduce_waldmeister_skolems info proof_steps = proof_steps - |> maps (skolemization_steps info) -end; diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 25 14:06:02 2019 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 25 14:14:56 2019 +0200 @@ -28,9 +28,9 @@ open ATP_Util open ATP_Problem +open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct -open ATP_Waldmeister open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof @@ -62,8 +62,8 @@ val skolemize_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, - spass_skolemize_rule, vampire_skolemisation_rule, - veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] + spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, + zipperposition_cnf_rule] fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix diff -r 1019b8609552 -r 1d2b2cc792f1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 25 14:06:02 2019 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 25 14:14:56 2019 +0200 @@ -29,7 +29,6 @@ open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct -open ATP_Waldmeister open ATP_Satallax open ATP_Systems open Sledgehammer_Util @@ -143,7 +142,6 @@ val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name - val waldmeister_new = (local_name = waldmeister_newN) val spassy = (local_name = pirateN orelse local_name = spassN) val completish = Config.get ctxt atp_completish @@ -262,7 +260,7 @@ val readable_names = not (Config.get ctxt atp_full_names) val lam_trans = lam_trans |> the_default best_lam_trans val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases - val value as (atp_problem, _, _, _, _) = + val value as (atp_problem, _, _, _) = if cache_key = SOME key then cache_value else @@ -271,13 +269,8 @@ |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) - |> (if waldmeister_new then - generate_waldmeister_problem ctxt hyp_ts concl_t - #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e)) - else - generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode - lam_trans uncurried_aliases readable_names true hyp_ts concl_t - #> (fn (a, b, c, d) => (a, b, c, d, NONE))) + |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode + lam_trans uncurried_aliases readable_names true hyp_ts concl_t fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem @@ -340,7 +333,7 @@ end | maybe_run_slice _ result = result in - ((NONE, ([], Symtab.empty, [], Symtab.empty,NONE)), + ((NONE, ([], Symtab.empty, [], Symtab.empty)), ("", Time.zeroTime, [], [], SOME InternalError), NONE) |> fold maybe_run_slice actual_slices end @@ -352,7 +345,7 @@ if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output - val ((_, (_, pool, lifted, sym_tab,wm_info)), (output, run_time, used_from, atp_proof, outcome), + val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) = with_cleanup clean_up run () |> tap export @@ -385,10 +378,8 @@ if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE val atp_proof = atp_proof - |> (if waldmeister_new then termify_waldmeister_proof ctxt pool - else termify_atp_proof ctxt name format type_enc pool lifted sym_tab) + |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> spassy ? introduce_spassy_skolems - |> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I) |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,