# HG changeset patch # User blanchet # Date 1411986609 -7200 # Node ID d15707791817923407edad93b0b73e952d8d13e6 # Parent 999adf103930577e762e40a3865acf2b880c7506# Parent ab4b94892c4cc64f5a74971a06f63208b5a286cd merge diff -r ab4b94892c4c -r d15707791817 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 29 11:18:25 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 29 12:30:09 2014 +0200 @@ -900,9 +900,8 @@ @{thm list.rel_intros(1)[no_vars]} \\ @{thm list.rel_intros(2)[no_vars]} -% FIXME (and add @ before antiquotation below) -%\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \ t\<^sub>m, cases pred]"}\rm:] ~ \\ -%{thm list.rel_cases[no_vars]} +\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \ t\<^sub>m, cases pred]"}\rm:] ~ \\ +@{thm list.rel_cases[no_vars]} \item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\ @{thm list.rel_sel[no_vars]} diff -r ab4b94892c4c -r d15707791817 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 29 12:30:09 2014 +0200 @@ -23,6 +23,7 @@ val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) val isar_proofsK = "isar_proofs" (*: enable Isar proof generation*) +val smt_proofsK = "smt_proofs" (*: enable SMT proof generation*) val minimizeK = "minimize" (*: instruct sledgehammer to run its minimizer*) val check_trivialK = "check_trivial" (*: check if goals are "trivial" (false by default)*) @@ -316,7 +317,7 @@ type stature = ATP_Problem_Generate.stature -fun good_line s = +fun is_good_line s = (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) andalso not (String.isSubstring "(> " s) andalso not (String.isSubstring ", > " s) @@ -325,9 +326,16 @@ (* Fragile hack *) fun proof_method_from_msg args msg = (case AList.lookup (op =) args proof_methodK of - SOME name => name + SOME name => + if name = "smart" then + if exists is_good_line (split_lines msg) then + "none" + else + "fail" + else + name | NONE => - if exists good_line (split_lines msg) then + if exists is_good_line (split_lines msg) then "none" (* trust the preplayed proof *) else if String.isSubstring "metis (" msg then msg |> Substring.full @@ -349,8 +357,8 @@ fun run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST - max_new_mono_instancesLST max_mono_itersLST dir pos st = + hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST + minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = let val thy = Proof.theory_of st val {context = ctxt, facts = chained_ths, goal} = Proof.goal st @@ -375,7 +383,7 @@ force_sos |> the_default I)) val params as {max_facts, minimize, preplay_timeout, ...} = Sledgehammer_Commands.default_params thy - ([("verbose", "true"), + ([(* ("verbose", "true"), *) ("fact_filter", fact_filter), ("type_enc", type_enc), ("strict", strict), @@ -386,6 +394,7 @@ ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] |> isar_proofsLST + |> smt_proofsLST |> minimizeLST (*don't confuse the two minimization flags*) |> max_new_mono_instancesLST |> max_mono_itersLST) @@ -471,6 +480,7 @@ val preplay_timeout = AList.lookup (op =) args preplay_timeoutK |> the_default preplay_timeout_default val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" + val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" val minimizeLST = available_parameter args minimizeK "minimize" val max_new_mono_instancesLST = available_parameter args max_new_mono_instancesK max_new_mono_instancesK @@ -479,8 +489,8 @@ val (msg, result) = run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST - max_new_mono_instancesLST max_mono_itersLST dir pos st + hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST + minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st in (case result of SH_OK (time_isa, time_prover, names) => @@ -559,8 +569,12 @@ in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if !meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms + else if !meth = "none" then + K all_tac + else if !meth = "fail" then + K no_tac else - K all_tac + (warning ("Unknown method " ^ quote (!meth)); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st diff -r ab4b94892c4c -r d15707791817 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Sep 29 12:30:09 2014 +0200 @@ -104,6 +104,7 @@ val mk_aconns : atp_connective -> ('a, 'b, 'c, 'd) atp_formula list -> ('a, 'b, 'c, 'd) atp_formula + val unmangled_type : string -> (string, 'a) ATP_Problem.atp_term val unmangled_const : string -> string * (string, 'b) atp_term list val unmangled_const_name : string -> string list val helper_table : ((string * bool) * (status * thm) list) list diff -r ab4b94892c4c -r d15707791817 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Sep 29 12:30:09 2014 +0200 @@ -348,17 +348,22 @@ >> AType) x and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x -(* We currently ignore TFF and THF types. *) -fun parse_type_signature x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x +(* We currently half ignore types. *) +fun parse_optional_type_signature x = + Scan.option ($$ tptp_has_type |-- parse_type) x and parse_arg x = - ($$ "(" |-- parse_term --| $$ ")" --| parse_type_signature - || scan_general_id --| parse_type_signature + ($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature + || scan_general_id -- parse_optional_type_signature -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") [] -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] - >> ATerm) x + >> (fn (((s, ty_opt), tyargs), args) => + if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then + ATerm ((s, the_list ty_opt), []) + else + ATerm ((s, tyargs), args))) x and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) - --| Scan.option parse_type_signature >> list_app) x + --| parse_optional_type_signature >> list_app) x and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x fun parse_atom x = diff -r ab4b94892c4c -r d15707791817 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Sep 29 12:30:09 2014 +0200 @@ -156,27 +156,6 @@ SOME s => s | NONE => raise ATP_CLASS [cls]) -(* Type variables are given the basic sort "HOL.type". Some will later be constrained by information - from type literals, or by type inference. *) -fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) = - let val Ts = map (typ_of_atp_type ctxt) tys in - (case unprefix_and_unascii type_const_prefix a of - SOME b => Type (invert_const b, Ts) - | NONE => - if not (null tys) then - raise ATP_TYPE [ty] (* only "tconst"s have type arguments *) - else - (case unprefix_and_unascii tfree_prefix a of - SOME b => make_tfree ctxt b - | NONE => - (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". - Sometimes variables from the ATP are indistinguishable from Isabelle variables, which - forces us to use a type parameter in all cases. *) - 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 (AFun (ty1, ty2)) = typ_of_atp_type ctxt ty1 --> typ_of_atp_type ctxt ty2 - fun atp_type_of_atp_term (ATerm ((s, _), us)) = let val tys = map atp_type_of_atp_term us in if s = tptp_fun_type then @@ -187,6 +166,30 @@ AType ((s, []), tys) end +(* Type variables are given the basic sort "HOL.type". Some will later be constrained by information + from type literals, or by type inference. *) +fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) = + let val Ts = map (typ_of_atp_type ctxt) tys in + (case unprefix_and_unascii native_type_prefix a of + SOME b => typ_of_atp_type ctxt (atp_type_of_atp_term (unmangled_type b)) + | NONE => + (case unprefix_and_unascii type_const_prefix a of + SOME b => Type (invert_const b, Ts) + | NONE => + if not (null tys) then + raise ATP_TYPE [ty] (* only "tconst"s have type arguments *) + else + (case unprefix_and_unascii tfree_prefix a of + SOME b => make_tfree ctxt b + | NONE => + (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". + Sometimes variables from the ATP are indistinguishable from Isabelle variables, which + forces us to use a type parameter in all cases. *) + 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 (AFun (ty1, ty2)) = typ_of_atp_type ctxt ty1 --> typ_of_atp_type ctxt ty2 + fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term (* Type class literal applied to a type. Returns triple of polarity, class, type. *) @@ -337,7 +340,7 @@ error "Isar proof reconstruction failed because the ATP proof contains unparsable \ \material." else if String.isPrefix native_type_prefix s then - @{const True} (* ignore TPTP type information *) + @{const True} (* ignore TPTP type information (needed?) *) else if s = tptp_equal then list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), map (do_term [] NONE) us) @@ -620,10 +623,6 @@ #> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop) #> local_prover = waldmeisterN ? repair_waldmeister_endgame -fun take_distinct_vars seen ((t as Var _) :: ts) = - if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts - | take_distinct_vars seen _ = rev seen - fun unskolemize_term skos = let val is_skolem = member (op =) skos diff -r ab4b94892c4c -r d15707791817 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Sep 29 12:30:09 2014 +0200 @@ -461,7 +461,7 @@ {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => - "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^ + "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = [("Here is a proof", "Formulae used in the proof")], diff -r ab4b94892c4c -r d15707791817 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 29 12:30:09 2014 +0200 @@ -1124,8 +1124,8 @@ fun postproc_co_induct lthy nn prop prop_conj = Drule.zero_var_indexes #> `(conj_dests nn) - #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop)) - ##> (fn thm => Thm.permute_prems 0 (~nn) + #>> map (fn thm => Thm.permute_prems 0 ~1 (thm RS prop)) + ##> (fn thm => Thm.permute_prems 0 (~ nn) (if nn = 1 then thm RS prop else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm)); @@ -1524,12 +1524,9 @@ end val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); in - map (fn Asets => - let - fun massage_thm thm = rotate_prems (~1) (thm RS bspec); - in - mk_thm lthy fpTs ctrss Asets |> nn = 1 ? map_prod massage_thm (cons consumes_attr) - end) (transpose setss) + map (mk_thm lthy fpTs ctrss + #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr)) + (transpose setss) end; fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) diff -r ab4b94892c4c -r d15707791817 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Sep 29 11:18:25 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Sep 29 12:30:09 2014 +0200 @@ -236,15 +236,24 @@ let val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt val t' = subst_atomic subst' t - val subs' = map (rationalize_proof subst_ctxt') subs + val subs' = map (rationalize_proof false subst_ctxt') subs in (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt') end - and rationalize_proof (subst_ctxt as (subst, _)) (Proof (fix, assms, steps)) = - Proof (fix, map (apsnd (subst_atomic subst)) assms, - fst (fold_map rationalize_step steps subst_ctxt)) + and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) = + let + val (fix', subst_ctxt' as (subst', _)) = + if outer then + (* last call: eliminate any remaining skolem names (from SMT proofs) *) + (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt)) + else + rename_obtains fix subst_ctxt + in + Proof (fix', map (apsnd (subst_atomic subst')) assms, + fst (fold_map rationalize_step steps subst_ctxt')) + end in - rationalize_proof ([], ctxt) + rationalize_proof true ([], ctxt) end val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT)