--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Apr 24 09:47:40 2012 +0200
@@ -189,7 +189,7 @@
val ctxt = Proof_Context.init_global thy
val state = Proof.init ctxt
val (res, _) = Nitpick.pick_nits_in_term state
- (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
+ (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
val _ = Output.urgent_message ("Nitpick: " ^ res)
in
(rpair []) (case res of
--- a/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200
@@ -45,9 +45,12 @@
? Path.append (Path.explode "$PWD"))
val ((_, _, problem), thy) =
TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
+ val partitioned_problem =
+ List.partition (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition)
+ problem
in
(exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
- map get_tptp_formula problem, thy)
+ pairself (map get_tptp_formula) partitioned_problem, Theory.checkpoint thy)
end
(** Isabelle (combination of provers) **)
@@ -59,8 +62,9 @@
fun nitpick_tptp_file timeout file_name =
let
- val (falsify, ts, thy) = read_tptp_file @{theory} file_name
+ val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
val ctxt = Proof_Context.init_global thy
+ val defs = defs |> map (ATP_Util.extensionalize_term ctxt)
val state = Proof.init ctxt
val params =
[("card", "1\<emdash>100"),
@@ -82,8 +86,8 @@
val step = 0
val subst = []
in
- Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst ts
- (if falsify then @{prop False} else @{prop True}); ()
+ Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst
+ defs nondefs (if falsify then @{prop False} else @{prop True}); ()
end
@@ -99,13 +103,13 @@
fun refute_tptp_file timeout file_name =
let
- val (falsify, ts, thy) = read_tptp_file @{theory} file_name
+ val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
val ctxt = Proof_Context.init_global thy
val params =
[("maxtime", string_of_int timeout),
("maxvars", "100000")]
in
- Refute.refute_term ctxt params ts @{prop False}
+ Refute.refute_term ctxt params (defs @ nondefs) @{prop False}
|> print_szs_from_outcome falsify
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Apr 24 09:47:40 2012 +0200
@@ -1207,19 +1207,6 @@
else
t
-fun is_fun_equality (@{const_name HOL.eq},
- Type (_, [Type (@{type_name fun}, _), _])) = true
- | is_fun_equality _ = false
-
-fun extensionalize_term ctxt t =
- if exists_Const is_fun_equality t then
- let val thy = Proof_Context.theory_of ctxt in
- t |> cterm_of thy |> Meson.extensionalize_conv ctxt
- |> prop_of |> Logic.dest_equals |> snd
- end
- else
- t
-
fun preprocess_abstractions_in_terms trans_lams facts =
let
val (facts, lambda_ts) =
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Apr 24 09:47:40 2012 +0200
@@ -35,6 +35,7 @@
val close_form : term -> term
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
+ val extensionalize_term : Proof.context -> term -> term
val transform_elim_prop : term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val strip_subgoal :
@@ -286,6 +287,19 @@
(List.take (binder_types (fastype_of1 (Ts, t)), n))
(list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
+fun is_fun_equality (@{const_name HOL.eq},
+ Type (_, [Type (@{type_name fun}, _), _])) = true
+ | is_fun_equality _ = false
+
+fun extensionalize_term ctxt t =
+ if exists_Const is_fun_equality t then
+ let val thy = Proof_Context.theory_of ctxt in
+ t |> cterm_of thy |> Meson.extensionalize_conv ctxt
+ |> prop_of |> Logic.dest_equals |> snd
+ end
+ else
+ t
+
(* 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
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 24 09:47:40 2012 +0200
@@ -72,7 +72,7 @@
val unregister_term_postprocessor : typ -> theory -> theory
val pick_nits_in_term :
Proof.state -> params -> mode -> int -> int -> int -> (term * term) list
- -> term list -> term -> string * Proof.state
+ -> term list -> term list -> term -> string * Proof.state
val pick_nits_in_subgoal :
Proof.state -> params -> mode -> int -> int -> string * Proof.state
end;
@@ -217,7 +217,7 @@
fun plazy f = Pretty.blk (0, pstrs (f ()))
fun pick_them_nits_in_term deadline state (params : params) mode i n step
- subst assm_ts orig_t =
+ subst def_assm_ts nondef_assm_ts orig_t =
let
val timer = Timer.startRealTimer ()
val thy = Proof.theory_of state
@@ -259,7 +259,9 @@
fun check_deadline () =
if passed_deadline deadline then raise TimeLimit.TimeOut else ()
- val assm_ts = if assms orelse mode <> Normal then assm_ts else []
+ val (def_assm_ts, nondef_assm_ts) =
+ if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
+ else ([], [])
val _ =
if step = 0 then
print_nt (fn () => "Nitpicking formula...")
@@ -269,26 +271,27 @@
(if i <> 1 orelse n <> 1 then
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
else
- "goal")) [Logic.list_implies (assm_ts, orig_t)]))
+ "goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
o Date.fromTimeLocal o Time.now)
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
- val conj_ts = neg_t :: assm_ts @ evals @ these needs
+ val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs
val tfree_table =
if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
else []
val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table
val neg_t = neg_t |> merge_tfrees
- val assm_ts = assm_ts |> map merge_tfrees
+ val def_assm_ts = def_assm_ts |> map merge_tfrees
+ val nondef_assm_ts = nondef_assm_ts |> map merge_tfrees
val evals = evals |> map merge_tfrees
val needs = needs |> Option.map (map merge_tfrees)
- val conj_ts = neg_t :: assm_ts @ evals @ these needs
+ val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs
val original_max_potential = max_potential
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
val case_names = case_const_names ctxt stds
- val defs = all_defs_of thy subst
+ val defs = def_assm_ts @ all_defs_of thy subst
val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
val nondef_table = const_nondef_table nondefs
@@ -321,7 +324,7 @@
error "Nitpick cannot handle goals with schematic type variables."
val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
no_poly_user_axioms, binarize) =
- preprocess_formulas hol_ctxt assm_ts neg_t
+ preprocess_formulas hol_ctxt nondef_assm_ts neg_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -672,7 +675,8 @@
got_all_user_axioms andalso none_true wfs andalso
sound_finitizes andalso total_consts <> SOME true andalso
codatatypes_ok
- fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
+ fun assms_prop () =
+ Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts)
in
(print_t (fn () =>
"% SZS status " ^
@@ -1047,7 +1051,7 @@
val timeout_bonus = seconds 1.0
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
- step subst assm_ts orig_t =
+ step subst def_assm_ts nondef_assm_ts orig_t =
let
val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
val print_t = if mode = TPTP then Output.urgent_message else K ()
@@ -1065,7 +1069,7 @@
time_limit (if debug orelse is_none timeout then NONE
else SOME (Time.+ (the timeout, timeout_bonus)))
(pick_them_nits_in_term deadline state params mode i n step subst
- assm_ts) orig_t
+ def_assm_ts nondef_assm_ts) orig_t
handle TOO_LARGE (_, details) =>
(print_t "% SZS status Unknown";
print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
@@ -1108,7 +1112,7 @@
val t = Logic.goal_params t i |> fst
val assms = map term_of (Assumption.all_assms_of ctxt)
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
- in pick_nits_in_term state params mode i n step subst assms t end
+ in pick_nits_in_term state params mode i n step subst [] assms t end
end
end;