--- 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 \<dots> 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 \<dots> 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]}
--- 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
--- 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
--- 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 =
--- 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
--- 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")],
--- 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), _))
--- 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)