# HG changeset patch # User desharna # Date 1666072650 -7200 # Node ID 045729b42c5da7583045d86fec71d5edd8d58e59 # Parent 44b0b22f4e2e6c489e151d47b010b0ec9618e4a0# Parent e5162a8baa2458d3e70d0b994491746bfb19fba6 merged diff -r 44b0b22f4e2e -r 045729b42c5d src/HOL/Examples/Ackermann.thy --- a/src/HOL/Examples/Ackermann.thy Mon Oct 17 18:21:54 2022 +0200 +++ b/src/HOL/Examples/Ackermann.thy Tue Oct 18 07:57:30 2022 +0200 @@ -4,7 +4,7 @@ section \A Tail-Recursive, Stack-Based Ackermann's Function\ -theory Ackermann imports Main +theory Ackermann imports "HOL-Library.Multiset_Order" "HOL-Library.Product_Lexorder" begin @@ -17,7 +17,9 @@ | "ack (Suc m) 0 = ack m 1" | "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)" -text\Here is the stack-based version, which uses lists.\ +subsection \Example of proving termination by reasoning about the domain\ + +text\The stack-based version uses lists.\ function (domintros) ackloop :: "nat list \ nat" where "ackloop (n # 0 # l) = ackloop (Suc n # l)" @@ -86,4 +88,53 @@ theorem ack: "ack m n = ackloop [n,m]" by (simp add: ackloop_acklist) +subsection \Example of proving termination using a multiset ordering\ + +text \This termination proof uses the argument from +Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. +Communications of the ACM 22 (8) 1979, 465–476.\ + +text\Setting up the termination proof. Note that Dershowitz had @{term z} as a global variable. +The top two stack elements are treated differently from the rest.\ + +fun ack_mset :: "nat list \ (nat\nat) multiset" where + "ack_mset [] = {#}" +| "ack_mset [x] = {#}" +| "ack_mset (z#y#l) = mset ((y,z) # map (\x. (Suc x, 0)) l)" + +lemma case1: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x \# mset l #}" +proof (cases l) + case (Cons m list) + have "{#(m, Suc n)#} < {#(Suc m, 0)#}" + by auto + also have "\ \ {#(Suc m, 0), (0,n)#}" + by auto + finally show ?thesis + by (simp add: Cons) +qed auto + +text\The stack-based version again. We need a fresh copy because + we've already proved the termination of @{term ackloop}.\ + +function Ackloop :: "nat list \ nat" where + "Ackloop (n # 0 # l) = Ackloop (Suc n # l)" +| "Ackloop (0 # Suc m # l) = Ackloop (1 # m # l)" +| "Ackloop (Suc n # Suc m # l) = Ackloop (n # Suc m # m # l)" +| "Ackloop [m] = m" +| "Ackloop [] = 0" + by pat_completeness auto + + +text \In each recursive call, the function @{term ack_mset} decreases according to the multiset +ordering.\ +termination + by (relation "inv_image {(x,y). xAnother shortcut compared with before: equivalence follows directly from this lemma.\ +lemma Ackloop_ack: "Ackloop (n # m # l) = Ackloop (ack m n # l)" + by (induction m n arbitrary: l rule: ack.induct) auto + +theorem "ack m n = Ackloop [n,m]" + by (simp add: Ackloop_ack) + end diff -r 44b0b22f4e2e -r 045729b42c5d src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Oct 17 18:21:54 2022 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Oct 18 07:57:30 2022 +0200 @@ -294,8 +294,6 @@ val default_rank = 1000 val default_term_order_weight = 1 -(* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle - metainformation. *) fun isabelle_info generate_info status rank = if generate_info then [] |> rank <> default_rank @@ -608,11 +606,11 @@ tptp_string_of_role kind ^ "," ^ "\n (" ^ tptp_string_of_formula format phi ^ ")" ^ (case source of - SOME tm => ", " ^ tptp_string_of_term format tm + SOME tm => ", " ^ tptp_string_of_term FOF tm | NONE => if null info then "" else ", []") ^ (case info of [] => "" - | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^ + | tms => ", [" ^ commas (map (tptp_string_of_term FOF) tms) ^ "]") ^ ")." ^ maybe_alt alt ^ "\n" fun tptp_lines format = diff -r 44b0b22f4e2e -r 045729b42c5d src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Oct 17 18:21:54 2022 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Oct 18 07:57:30 2022 +0200 @@ -2256,7 +2256,7 @@ (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP forbids name clashes, and some of the remote provers might care. *) -fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank +fun line_of_fact ctxt generate_isabelle_info prefix encode alt freshen pos mono type_enc rank (j, {name, stature = (_, status), role, iformula, atomic_types}) = Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, alt name), @@ -2266,22 +2266,22 @@ should_guard_var_in_formula (if pos then SOME true else NONE) |> close_formula_universally |> bound_tvars type_enc true atomic_types, - NONE, isabelle_info generate_info (string_of_status status) (rank j)) + NONE, isabelle_info generate_isabelle_info (string_of_status status) (rank j)) -fun lines_of_subclass generate_info type_enc sub super = +fun lines_of_subclass generate_isabelle_info type_enc sub super = Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom, AConn (AImplies, [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a))) |> bound_tvars type_enc false [tvar_a], - NONE, isabelle_info generate_info inductiveN helper_rank) + NONE, isabelle_info generate_isabelle_info inductiveN helper_rank) -fun lines_of_subclass_pair generate_info type_enc (sub, supers) = +fun lines_of_subclass_pair generate_isabelle_info type_enc (sub, supers) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)] else - map (lines_of_subclass generate_info type_enc sub) supers + map (lines_of_subclass generate_isabelle_info type_enc sub) supers -fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) = +fun line_of_tcon_clause generate_isabelle_info type_enc (name, prems, (cl, T)) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then Class_Memb (class_memb_prefix ^ name, map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems, @@ -2291,7 +2291,7 @@ mk_ahorn (maps (class_atoms type_enc) prems) (class_atom type_enc (cl, T)) |> bound_tvars type_enc true (snd (dest_Type T)), - NONE, isabelle_info generate_info inductiveN helper_rank) + NONE, isabelle_info generate_isabelle_info inductiveN helper_rank) fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) = Formula ((conjecture_prefix ^ name, ""), role, @@ -2486,7 +2486,7 @@ ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end -fun line_of_guards_mono_type ctxt generate_info mono type_enc T = +fun line_of_guards_mono_type ctxt generate_isabelle_info mono type_enc T = Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, IConst (`make_bound_var "X", T, []) @@ -2496,21 +2496,21 @@ (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), - NONE, isabelle_info generate_info inductiveN helper_rank) + NONE, isabelle_info generate_isabelle_info inductiveN helper_rank) -fun line_of_tags_mono_type ctxt generate_info mono type_enc T = +fun line_of_tags_mono_type ctxt generate_isabelle_info mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, - NONE, isabelle_info generate_info non_rec_defN helper_rank) + NONE, isabelle_info generate_isabelle_info non_rec_defN helper_rank) end -fun lines_of_mono_types ctxt generate_info mono type_enc = +fun lines_of_mono_types ctxt generate_isabelle_info mono type_enc = (case type_enc of Native _ => K [] - | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc) - | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc)) + | Guards _ => map (line_of_guards_mono_type ctxt generate_isabelle_info mono type_enc) + | Tags _ => map (line_of_tags_mono_type ctxt generate_isabelle_info mono type_enc)) fun decl_line_of_sym ctxt type_enc s (s', T_args, T, pred_sym, ary, _) = let @@ -2534,7 +2534,7 @@ fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I) -fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j +fun line_of_guards_sym_decl ctxt generate_isabelle_info mono type_enc n s j (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt @@ -2563,10 +2563,10 @@ |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, - NONE, isabelle_info generate_info inductiveN helper_rank) + NONE, isabelle_info generate_isabelle_info inductiveN helper_rank) end -fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s +fun lines_of_tags_sym_decl ctxt generate_isabelle_info mono type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val thy = Proof_Context.theory_of ctxt @@ -2583,7 +2583,7 @@ val tag_with = tag_with_type ctxt mono type_enc NONE fun formula c = [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE, - isabelle_info generate_info non_rec_defN helper_rank)] + isabelle_info generate_isabelle_info non_rec_defN helper_rank)] in if pred_sym orelse not (should_encode_type ctxt mono level res_T) then [] @@ -2608,7 +2608,7 @@ end | rationalize_decls _ decls = decls -fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) = +fun lines_of_sym_decls ctxt generate_isabelle_info mono type_enc (s, decls) = (case type_enc of Native _ => [decl_line_of_sym ctxt type_enc s (hd decls)] | Guards (_, level) => @@ -2618,7 +2618,7 @@ val n = length decls val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl) in - map_index (uncurry (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)) decls + map_index (uncurry (line_of_guards_sym_decl ctxt generate_isabelle_info mono type_enc n s)) decls end | Tags (_, level) => if is_type_level_uniform level then @@ -2626,14 +2626,14 @@ else let val n = length decls in map_index I decls - |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s) + |> maps (lines_of_tags_sym_decl ctxt generate_isabelle_info mono type_enc n s) end) -fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab = +fun lines_of_sym_decl_table ctxt generate_isabelle_info mono type_enc mono_Ts sym_decl_tab = let val syms = sym_decl_tab |> Symtab.dest |> sort_by fst - val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts - val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms + val mono_lines = lines_of_mono_types ctxt generate_isabelle_info mono type_enc mono_Ts + val decl_lines = maps (lines_of_sym_decls ctxt generate_isabelle_info mono type_enc) syms in mono_lines @ decl_lines end fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases @@ -2680,8 +2680,8 @@ fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0 - types in_conj = +fun do_uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0 sym_tab + base_s0 types in_conj = let fun do_alias ary = let @@ -2717,31 +2717,32 @@ in ([tm1, tm2], [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE, - isabelle_info generate_info non_rec_defN helper_rank)]) + isabelle_info generate_isabelle_info non_rec_defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab +fun uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = (case unprefix_and_unascii const_prefix s of SOME mangled_s => if String.isSubstring uncurried_alias_sep mangled_s then let val base_s0 = mangled_s |> unmangled_invert_const in - do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab - base_s0 types in_conj min_ary + do_uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0 + sym_tab base_s0 types in_conj min_ary end else ([], []) | NONE => ([], [])) -fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases - sym_tab0 sym_tab = +fun uncurried_alias_lines_of_sym_table ctxt generate_isabelle_info ctrss mono type_enc + uncurried_aliases sym_tab0 sym_tab = ([], []) |> uncurried_aliases ? Symtab.fold_rev (pair_append - o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab) + o uncurried_alias_lines_of_sym ctxt generate_isabelle_info ctrss mono type_enc sym_tab0 + sym_tab) sym_tab val implicit_declsN = "Could-be-implicit typings" @@ -2820,7 +2821,7 @@ val app_op_and_predicator_threshold = 45 -fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans +fun generate_atp_problem ctxt generate_isabelle_info format prem_role type_enc mode lam_trans uncurried_aliases readable_names presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt @@ -2857,8 +2858,8 @@ val (ho_stuff, sym_tab) = sym_table_of_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = - uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases - sym_tab0 sym_tab + uncurried_alias_lines_of_sym_table ctxt generate_isabelle_info ctrss mono type_enc + uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab) |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false) @@ -2873,7 +2874,7 @@ val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms) |> sym_decl_table_of_facts thy type_enc sym_tab - |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts + |> lines_of_sym_decl_table ctxt generate_isabelle_info mono type_enc mono_Ts val datatype_decl_lines = map decl_line_of_datatype datatypes val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines val num_facts = length facts @@ -2881,14 +2882,14 @@ val pos = mode <> Exporter val rank_of = rank_of_fact_num num_facts val fact_lines = facts - |> map_index (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc - rank_of) + |> map_index (line_of_fact ctxt generate_isabelle_info fact_prefix ascii_of I freshen pos mono + type_enc rank_of) - val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs - val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses + val subclass_lines = maps (lines_of_subclass_pair generate_isabelle_info type_enc) subclass_pairs + val tcon_lines = map (line_of_tcon_clause generate_isabelle_info type_enc) tcon_clauses val helper_lines = helpers - |> map_index (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc - (K default_rank)) + |> map_index (line_of_fact ctxt generate_isabelle_info helper_prefix I (K "") false true mono + type_enc (K default_rank)) val free_type_lines = lines_of_free_types type_enc (facts @ conjs) val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs (* Reordering these might confuse the proof reconstruction code. *) diff -r 44b0b22f4e2e -r 045729b42c5d src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Oct 17 18:21:54 2022 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Oct 18 07:57:30 2022 +0200 @@ -19,6 +19,7 @@ proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, + generate_isabelle_info : bool, good_slices : Proof.context -> (base_slice * atp_slice) list, good_max_mono_iters : int, good_max_new_mono_instances : int} @@ -33,8 +34,8 @@ val spass_H2SOS : string val isabelle_scala_function: string list * string list val remote_atp : string -> string -> string list -> (string * string) list -> - (atp_failure * string) list -> atp_formula_role -> (Proof.context -> base_slice * atp_slice) -> - string * (unit -> atp_config) + (atp_failure * string) list -> atp_formula_role -> bool -> + (Proof.context -> base_slice * atp_slice) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val is_atp_installed : theory -> string -> bool @@ -79,6 +80,7 @@ proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, + generate_isabelle_info : bool, good_slices : Proof.context -> (base_slice * atp_slice) list, good_max_mono_iters : int, good_max_new_mono_instances : int} @@ -137,6 +139,7 @@ proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], @@ -159,6 +162,7 @@ (TimedOut, ": Timeout"), (GaveUp, ": Unknown")], prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((1000 (* infinity *), 100, meshN), (TF1, "poly_native", liftingN, false, ""))], @@ -184,6 +188,7 @@ (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, + generate_isabelle_info = false, good_slices = let val (format, type_enc, lam_trans, extra_options) = @@ -221,6 +226,7 @@ [(ProofIncomplete, "% SZS output start CNFRefutation")] @ known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, 32, meshN), (TF0, "mono_native", liftingN, false, "")), @@ -250,6 +256,7 @@ (GaveUp, "No.of.Axioms")] @ known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], @@ -271,6 +278,7 @@ proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((6, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), @@ -295,6 +303,7 @@ [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((12, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], @@ -314,37 +323,34 @@ val spass_H2SOS = "-Heuristic=2 -SOS" val spass_config : atp_config = - let - val format = DFG Monomorphic - in - {exec = (["SPASS_HOME"], ["SPASS"]), - arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => - ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ - "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem - |> extra_options <> "" ? prefix (extra_options ^ " ")], - proof_delims = [("Here is a proof", "Formulae used in the proof")], - known_failures = - [(GaveUp, "SPASS beiseite: Completion found"), - (TimedOut, "SPASS beiseite: Ran out of time"), - (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), - (MalformedInput, "Undefined symbol"), - (MalformedInput, "Free Variable"), - (Unprovable, "No formulae and clauses found in input file"), - (InternalError, "Please report this error")], - prem_role = Conjecture, - good_slices = - (* FUDGE *) - K [((2, 150, meshN), (format, "mono_native", combsN, true, "")), - ((2, 500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)), - ((2, 50, meshN), (format, "mono_native", liftingN, true, spass_H2LR0LT0)), - ((2, 250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)), - ((2, 1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)), - ((2, 150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), - ((2, 300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)), - ((2, 100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))], - good_max_mono_iters = default_max_mono_iters, - good_max_new_mono_instances = default_max_new_mono_instances} - end + {exec = (["SPASS_HOME"], ["SPASS"]), + arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn problem => + ["-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ + "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ File.bash_path problem + |> extra_options <> "" ? prefix (extra_options ^ " ")], + proof_delims = [("Here is a proof", "Formulae used in the proof")], + known_failures = + [(GaveUp, "SPASS beiseite: Completion found"), + (TimedOut, "SPASS beiseite: Ran out of time"), + (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), + (MalformedInput, "Undefined symbol"), + (MalformedInput, "Free Variable"), + (Unprovable, "No formulae and clauses found in input file"), + (InternalError, "Please report this error")], + prem_role = Conjecture, + generate_isabelle_info = true, + good_slices = + (* FUDGE *) + K [((2, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")), + ((2, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)), + ((2, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)), + ((2, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)), + ((2, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)), + ((2, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), + ((2, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)), + ((2, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))], + good_max_mono_iters = default_max_mono_iters, + good_max_new_mono_instances = default_max_new_mono_instances} val spass = (spassN, fn () => spass_config) @@ -378,6 +384,7 @@ (Interrupted, "Aborted by signal SIGINT")] @ known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = false, good_slices = (* FUDGE *) K [((2, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), @@ -410,6 +417,7 @@ [(TimedOut, "SZS status ResourceOut")] @ (* odd way of timing out *) known_szs_status_failures, prem_role = Hypothesis, + generate_isabelle_info = true, good_slices = K [((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), (* sh5_sh1.sh *) ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), (* sh8_shallow_sine.sh *) @@ -472,7 +480,8 @@ val isabelle_scala_function = (["SCALA_HOME"], ["bin/scala"]) -fun remote_config system_name system_versions proof_delims known_failures prem_role good_slice = +fun remote_config system_name system_versions proof_delims known_failures prem_role + generate_isabelle_info good_slice = {exec = isabelle_scala_function, arguments = fn _ => fn _ => fn command => fn timeout => fn problem => [the_remote_system system_name system_versions, @@ -481,17 +490,21 @@ proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_says_failures, prem_role = prem_role, + generate_isabelle_info = generate_isabelle_info, good_slices = fn ctxt => [good_slice ctxt], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} : atp_config fun remotify_config system_name system_versions good_slice - ({proof_delims, known_failures, prem_role, ...} : atp_config) = - remote_config system_name system_versions proof_delims known_failures prem_role good_slice + ({proof_delims, known_failures, prem_role, generate_isabelle_info, ...} : atp_config) = + remote_config system_name system_versions proof_delims known_failures prem_role + generate_isabelle_info good_slice -fun remote_atp name system_name system_versions proof_delims known_failures prem_role good_slice = +fun remote_atp name system_name system_versions proof_delims known_failures prem_role + generate_isabelle_info good_slice = (remote_prefix ^ name, fn () => - remote_config system_name system_versions proof_delims known_failures prem_role good_slice) + remote_config system_name system_versions proof_delims known_failures prem_role + generate_isabelle_info good_slice) fun remotify_atp (name, config) system_name system_versions good_slice = (remote_prefix ^ name, remotify_config system_name system_versions good_slice o config) @@ -501,7 +514,7 @@ (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) - Hypothesis + Hypothesis false (K ((1000 (* infinity *), 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) val remote_agsyhol = @@ -536,6 +549,7 @@ proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, + generate_isabelle_info = false, good_slices = K [((2, 256, "mepo"), (format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], diff -r 44b0b22f4e2e -r 045729b42c5d src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Oct 17 18:21:54 2022 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Oct 18 07:57:30 2022 +0200 @@ -114,8 +114,8 @@ val thy = Proof.theory_of state val ctxt = Proof.context_of state - val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters, - good_max_new_mono_instances, ...} = get_atp thy name () + val {exec, arguments, proof_delims, known_failures, prem_role, generate_isabelle_info, + good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name @@ -188,7 +188,6 @@ val generous_run_timeout = if mode = MaSh then one_day else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let - val generate_info = (case good_format of DFG _ => true | _ => false) val readable_names = not (Config.get ctxt atp_full_names) in facts @@ -196,8 +195,8 @@ filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) - |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode - good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t + |> generate_atp_problem ctxt generate_isabelle_info good_format prem_role type_enc + atp_mode good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () =>