--- a/NEWS Thu Mar 02 17:05:24 2023 +0100
+++ b/NEWS Thu Mar 02 17:46:29 2023 +0100
@@ -231,6 +231,13 @@
totalp_on_multpDM
totalp_on_multpHO
+* HOL-Algebra: new theories SimpleGroups (simple groups)
+ and SndIsomorphismGrp (second isomorphism theorem for groups),
+ by Jakob von Raumer
+
+* HOL-Analysis and HOL-Complex_Analysis: much new material, due to
+ Manuel Eberl and Wenda Li.
+
* Mirabelle:
- Added session to output directory structure. Minor INCOMPATIBILITY.
@@ -239,9 +246,13 @@
Minor INCOMPATIBILITY.
* Sledgehammer:
- - Added refutational mode to find likely unprovable conectures. It is
- enabled by default in addition to the usual proving mode and can be
- enabled or disabled using the 'refute' option.
+ - Added an inconsistency check mode to find likely unprovable
+ conjectures. It is enabled by default in addition to the usual
+ proving mode and can be controlled using the 'falsify' option.
+ - Added an abduction mode to find likely missing hypotheses to
+ conjectures. It currently works only with the E prover. It is
+ enabled by default and can be controlled using the 'abduce'
+ option.
*** ML ***
--- a/src/Doc/Sledgehammer/document/root.tex Thu Mar 02 17:05:24 2023 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Mar 02 17:46:29 2023 +0100
@@ -100,7 +100,7 @@
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly
-to find proofs but also to find inconsistencies.%
+to find proofs but also to refute the goal.%
\footnote{The distinction between ATPs and SMT solvers is mostly
historical but convenient.}
%
@@ -242,8 +242,7 @@
e: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
cvc4: Try this: \textbf{by} \textit{simp} (0.4 ms) \\
z3: Try this: \textbf{by} \textit{simp} (0.5 ms) \\
-vampire: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
-Done
+vampire: Try this: \textbf{by} \textit{simp} (0.3 ms)
\postw
Sledgehammer ran CVC4, E, Vampire, Z3, and possibly other provers in parallel.
@@ -277,11 +276,17 @@
\prew
\slshape
-vampire found an inconsistency\ldots \\
-vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
-Done
+vampire found a falsification\ldots \\
+vampire: The goal is falsified by these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
\postw
+Sometimes Sledgehammer will helpfully suggest a missing assumption:
+
+\prew
+\slshape
+e: Candidate missing assumption: \\
+length ys = length xs
+\postw
\section{Hints}
\label{hints}
@@ -813,15 +818,30 @@
\opnodefault{prover}{string}
Alias for \textit{provers}.
-\opsmart{check\_consistent}{dont\_check\_consistent}
-Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
-default, it looks for both proofs and inconsistencies.
+\opsmartx{falsify}{dont\_falsify}
+Specifies whether Sledgehammer should look for falsifications or for proofs. By
+default, it looks for both.
-An inconsistency indicates that the goal, taken as an axiom, would be
+A falsification indicates that the goal, taken as an axiom, would be
inconsistent with some specific background facts if it were added as a lemma,
indicating a likely issue with the goal. Sometimes the inconsistency involves
-only the background theory; this might happen, for example, if an axiom is used
-or if a lemma was introduced with \textbf{sorry}.
+only the background theory; this might happen, for example, if a flawed axiom is
+used or if a flawed lemma was introduced with \textbf{sorry}.
+
+\opdefault{abduce}{smart\_int}{smart}
+Specifies the maximum number of candidate missing assumptions that may be
+displayed. These hypotheses are discovered heuristically by a process called
+abduction (which stands in contrast to deduction)---that is, they are guessed
+and found to be sufficient to prove the goal.
+
+Abduction is currently supported only by E. If the option is set to
+\textit{smart} (the default), abduction is enabled only in some of the E time
+slices, and at most one candidate missing assumption is displayed. You can
+disable abduction altogether by setting the option to 0 or enable it in all
+time slices by setting it to a nonzero value.
+
+\optrueonly{dont\_abduce}
+Alias for ``\textit{abduce} = 0''.
\optrue{minimize}{dont\_minimize}
Specifies whether the proof minimization tool should be invoked automatically
@@ -1199,6 +1219,7 @@
\item[\labelitemi] \textbf{\textit{some\_preplayed}:} Sledgehammer found a proof that was successfully preplayed.
\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
+\item[\labelitemi] \textbf{\textit{resources\_out}:} Sledgehammer ran out of resources.
\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some
problem.
\end{enum}
--- a/src/HOL/Analysis/Further_Topology.thy Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Mar 02 17:46:29 2023 +0100
@@ -3333,7 +3333,7 @@
then have "z \<noteq> 0" by auto
have "(w/z)^n = 1"
by (metis False divide_self_if eq power_divide power_one)
- then obtain j where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
+ then obtain j::nat where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
using Suc_leI assms \<open>2 \<le> n\<close> complex_roots_unity [THEN eqset_imp_iff, of n "w/z"]
by force
have "cmod (w/z - 1) < 2 * sin (pi / real n)"
--- a/src/HOL/Analysis/Uniform_Limit.thy Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Mar 02 17:46:29 2023 +0100
@@ -6,7 +6,7 @@
section \<open>Uniform Limit and Uniform Convergence\<close>
theory Uniform_Limit
-imports Connected Summation_Tests
+imports Connected Summation_Tests Infinite_Sum
begin
@@ -560,12 +560,67 @@
shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test[OF assms])
-lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
- by simp
+
+lemma Weierstrass_m_test_general:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: banach"
+ fixes M :: "'a \<Rightarrow> real"
+ assumes norm_le: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> norm (f x y) \<le> M x"
+ assumes summable: "M summable_on X"
+ shows "uniform_limit Y (\<lambda>X y. \<Sum>x\<in>X. f x y) (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y) (finite_subsets_at_top X)"
+proof (rule uniform_limitI)
+ fix \<epsilon> :: real
+ assume "\<epsilon> > 0"
+ define S where "S = (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y)"
+ have S: "((\<lambda>x. f x y) has_sum S y) X" if y: "y \<in> Y" for y
+ unfolding S_def
+ proof (rule has_sum_infsum)
+ have "(\<lambda>x. norm (f x y)) summable_on X"
+ by (rule abs_summable_on_comparison_test'[OF summable norm_le]) (use y in auto)
+ thus "(\<lambda>x. f x y) summable_on X"
+ by (metis abs_summable_summable)
+ qed
+
+ define T where "T = (\<Sum>\<^sub>\<infinity>x\<in>X. M x)"
+ have T: "(M has_sum T) X"
+ unfolding T_def by (simp add: local.summable)
+ have M_summable: "M summable_on X'" if "X' \<subseteq> X" for X'
+ using local.summable summable_on_subset_banach that by blast
+
+ have f_summable: "(\<lambda>x. f x y) summable_on X'" if "X' \<subseteq> X" "y \<in> Y" for X' y
+ using S summable_on_def summable_on_subset_banach that by blast
+ have "eventually (\<lambda>X'. dist (\<Sum>x\<in>X'. M x) T < \<epsilon>) (finite_subsets_at_top X)"
+ using T \<open>\<epsilon> > 0\<close> unfolding T_def has_sum_def tendsto_iff by blast
+ moreover have "eventually (\<lambda>X'. finite X' \<and> X' \<subseteq> X) (finite_subsets_at_top X)"
+ by (simp add: eventually_finite_subsets_at_top_weakI)
+ ultimately show "\<forall>\<^sub>F X' in finite_subsets_at_top X. \<forall>y\<in>Y. dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>"
+ proof eventually_elim
+ case X': (elim X')
+ show "\<forall>y\<in>Y. dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>"
+ proof
+ fix y assume y: "y \<in> Y"
+ have 1: "((\<lambda>x. f x y) has_sum (S y - (\<Sum>x\<in>X'. f x y))) (X - X')"
+ using X' y by (intro has_sum_Diff S has_sum_finite[of X'] f_summable) auto
+ have 2: "(M has_sum (T - (\<Sum>x\<in>X'. M x))) (X - X')"
+ using X' y by (intro has_sum_Diff T has_sum_finite[of X'] M_summable) auto
+ have "dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) = norm (S y - (\<Sum>x\<in>X'. f x y))"
+ by (simp add: dist_norm norm_minus_commute S_def)
+ also have "norm (S y - (\<Sum>x\<in>X'. f x y)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>X-X'. M x)"
+ using 2 y by (intro norm_infsum_le[OF 1 _ norm_le]) (auto simp: infsumI)
+ also have "\<dots> = T - (\<Sum>x\<in>X'. M x)"
+ using 2 by (auto simp: infsumI)
+ also have "\<dots> < \<epsilon>"
+ using X' by (simp add: dist_norm)
+ finally show "dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>" .
+ qed
+ qed
+qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural introduction rules\<close>
+lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
+ by simp
+
named_theorems uniform_limit_intros "introduction rules for uniform_limit"
setup \<open>
Global_Theory.add_thms_dynamic (\<^binding>\<open>uniform_limit_eq_intros\<close>,
--- a/src/HOL/List.thy Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/List.thy Thu Mar 02 17:46:29 2023 +0100
@@ -4999,15 +4999,7 @@
lemma distinct_set_subseqs:
assumes "distinct xs"
shows "distinct (map set (subseqs xs))"
-proof (rule card_distinct)
- have "finite (set xs)" ..
- then have "card (Pow (set xs)) = 2 ^ card (set xs)"
- by (rule card_Pow)
- with assms distinct_card [of xs] have "card (Pow (set xs)) = 2 ^ length xs"
- by simp
- then show "card (set (map set (subseqs xs))) = length (map set (subseqs xs))"
- by (simp add: subseqs_powset length_subseqs)
-qed
+ by (simp add: assms card_Pow card_distinct distinct_card length_subseqs subseqs_powset)
lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
by (induct n) simp_all
@@ -5559,7 +5551,7 @@
next
case snoc
thus ?case
- by (auto simp: nth_append sorted_wrt_append)
+ by (simp add: nth_append sorted_wrt_append)
(metis less_antisym not_less nth_mem)
qed
@@ -5581,7 +5573,7 @@
by simp
lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
- by(induction zs) auto
+ by auto
lemmas sorted2_simps = sorted1 sorted2
@@ -5618,9 +5610,7 @@
lemma sorted_rev_nth_mono:
"sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
- using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
- rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
- by auto
+ by (metis local.nle_le order_class.antisym_conv1 sorted_wrt_iff_nth_less sorted_wrt_rev)
lemma sorted_rev_iff_nth_mono:
"sorted (rev xs) \<longleftrightarrow> (\<forall> i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs!j \<le> xs!i)" (is "?L = ?R")
@@ -5635,7 +5625,7 @@
"length xs - Suc l \<le> length xs - Suc k" "length xs - Suc k < length xs"
using asms by auto
thus "rev xs ! k \<le> rev xs ! l"
- using \<open>?R\<close> \<open>k \<le> l\<close> unfolding rev_nth[OF \<open>k < length xs\<close>] rev_nth[OF \<open>l < length xs\<close>] by blast
+ by (simp add: \<open>?R\<close> rev_nth)
qed
thus ?L by (simp add: sorted_iff_nth_mono)
qed
@@ -5658,13 +5648,9 @@
using sorted_map_remove1 [of "\<lambda>x. x"] by simp
lemma sorted_butlast:
- assumes "xs \<noteq> []" and "sorted xs"
+ assumes "sorted xs"
shows "sorted (butlast xs)"
-proof -
- from \<open>xs \<noteq> []\<close> obtain ys y where "xs = ys @ [y]"
- by (cases xs rule: rev_cases) auto
- with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
-qed
+ by (simp add: assms butlast_conv_take sorted_wrt_take)
lemma sorted_replicate [simp]: "sorted(replicate n x)"
by(induction n) (auto)
@@ -5701,28 +5687,13 @@
"sorted (map f ys)" "distinct (map f ys)"
assumes "set xs = set ys"
shows "xs = ys"
-proof -
- from assms have "map f xs = map f ys"
- by (simp add: sorted_distinct_set_unique)
- with \<open>inj_on f (set xs \<union> set ys)\<close> show "xs = ys"
- by (blast intro: map_inj_on)
-qed
-
-lemma
- assumes "sorted xs"
- shows sorted_take: "sorted (take n xs)"
- and sorted_drop: "sorted (drop n xs)"
-proof -
- from assms have "sorted (take n xs @ drop n xs)" by simp
- then show "sorted (take n xs)" and "sorted (drop n xs)"
- unfolding sorted_append by simp_all
-qed
+ using assms map_inj_on sorted_distinct_set_unique by fastforce
lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
- by (auto dest: sorted_drop simp add: dropWhile_eq_drop)
+ by (auto dest: sorted_wrt_drop simp add: dropWhile_eq_drop)
lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
- by (subst takeWhile_eq_take) (auto dest: sorted_take)
+ by (subst takeWhile_eq_take) (auto dest: sorted_wrt_take)
lemma sorted_filter:
"sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
@@ -5745,7 +5716,7 @@
(is "filter ?P xs = ?tW")
proof (rule takeWhile_eq_filter[symmetric])
let "?dW" = "dropWhile ?P xs"
- fix x assume "x \<in> set ?dW"
+ fix x assume x: "x \<in> set ?dW"
then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
unfolding in_set_conv_nth by auto
hence "length ?tW + i < length (?tW @ ?dW)"
@@ -5759,8 +5730,7 @@
unfolding nth_append_length_plus nth_i
using i preorder_class.le_less_trans[OF le0 i] by simp
also have "... \<le> t"
- using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
- using hd_conv_nth[of "?dW"] by simp
+ by (metis hd_conv_nth hd_dropWhile length_greater_0_conv length_pos_if_in_set local.leI x)
finally show "\<not> t < f x" by simp
qed
@@ -7325,12 +7295,15 @@
lemma Cons_acc_listrel1I [intro!]:
"x \<in> Wellfounded.acc r \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> Wellfounded.acc (listrel1 r)"
-apply (induct arbitrary: xs set: Wellfounded.acc)
-apply (erule thin_rl)
-apply (erule acc_induct)
- apply (rule accI)
-apply (blast)
-done
+proof (induction arbitrary: xs set: Wellfounded.acc)
+ case outer: (1 u)
+ show ?case
+ proof (induct xs rule: acc_induct)
+ case 1
+ show "xs \<in> Wellfounded.acc (listrel1 r)"
+ by (simp add: outer.prems)
+ qed (metis (no_types, lifting) Cons_listrel1E2 acc.simps outer.IH)
+qed
lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
proof (induct set: lists)
@@ -7344,11 +7317,13 @@
qed
lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
-apply (induct set: Wellfounded.acc)
-apply clarify
-apply (rule accI)
-apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
-done
+proof (induction set: Wellfounded.acc)
+ case (1 x)
+ then have "\<And>u v. \<lbrakk>u \<in> set x; (v, u) \<in> r\<rbrakk> \<Longrightarrow> v \<in> Wellfounded.acc r"
+ by (metis in_lists_conv_set in_set_conv_decomp listrel1I)
+ then show ?case
+ by (meson acc.intros in_listsI)
+qed
lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
by (auto simp: wf_acc_iff
@@ -7856,11 +7831,7 @@
"all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
proof -
have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
- proof -
- fix n
- assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
- then show "P n" by (cases "n = i") simp_all
- qed
+ using le_less_Suc_eq by fastforce
show ?thesis by (auto simp add: all_interval_nat_def intro: *)
qed
@@ -7879,11 +7850,7 @@
"all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
proof -
have *: "\<And>k. P i \<Longrightarrow> \<forall>k\<in>{i+1..j}. P k \<Longrightarrow> i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> P k"
- proof -
- fix k
- assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
- then show "P k" by (cases "k = i") simp_all
- qed
+ by (smt (verit, best) atLeastAtMost_iff)
show ?thesis by (auto simp add: all_interval_int_def intro: *)
qed
@@ -8084,11 +8051,7 @@
lemma card_set [code]:
"card (set xs) = length (remdups xs)"
-proof -
- have "card (set (remdups xs)) = length (remdups xs)"
- by (rule distinct_card) simp
- then show ?thesis by simp
-qed
+ by (simp add: length_remdups_card_conv)
lemma the_elem_set [code]:
"the_elem (set [x]) = x"
@@ -8255,15 +8218,8 @@
thus "distinct_adj xs \<longleftrightarrow> distinct_adj ys"
proof (induction rule: list_all2_induct)
case (Cons x xs y ys)
- note * = this
show ?case
- proof (cases xs)
- case [simp]: (Cons x' xs')
- with * obtain y' ys' where [simp]: "ys = y' # ys'"
- by (cases ys) auto
- from * show ?thesis
- using assms by (auto simp: distinct_adj_Cons bi_unique_def)
- qed (use * in auto)
+ by (metis Cons assms bi_unique_def distinct_adj_Cons list.rel_sel)
qed auto
qed
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Mar 02 17:46:29 2023 +0100
@@ -12,6 +12,9 @@
"HOL-Library.Multiset"
begin
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
lemma AE_emeasure_singleton:
assumes x: "emeasure M {x} \<noteq> 0" and ae: "AE x in M. P x" shows "P x"
proof -
--- a/src/HOL/Probability/Product_PMF.thy Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Probability/Product_PMF.thy Thu Mar 02 17:46:29 2023 +0100
@@ -7,6 +7,9 @@
imports Probability_Mass_Function Independent_Family
begin
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
subsection \<open>Preliminaries\<close>
lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\<lambda>x. pmf p x * f x) UNIV"
--- a/src/HOL/Probability/SPMF.thy Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Probability/SPMF.thy Thu Mar 02 17:46:29 2023 +0100
@@ -2338,20 +2338,23 @@
lemma scale_scale_spmf:
"scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
(is "?lhs = ?rhs")
-proof(rule spmf_eqI)
- fix i
- have "max 0 (min (1 / weight_spmf p) r') *
- max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
- max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
- proof(cases "weight_spmf p > 0")
- case False
- thus ?thesis by(simp add: not_less weight_spmf_le_0)
- next
- case True
- thus ?thesis by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
+proof(cases "weight_spmf p > 0")
+ case False
+ thus ?thesis
+ by (simp add: weight_spmf_eq_0 zero_less_measure_iff)
+next
+ case True
+ show ?thesis
+ proof(rule spmf_eqI)
+ fix i
+ have "max 0 (min (1 / weight_spmf p) r') * max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
+ max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
+ using True
+ by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
+ then show "spmf ?lhs i = spmf ?rhs i"
+ apply (subst spmf_scale_spmf)+ (*FOR SOME REASON we now get linarith_split_limit exceeded if simp is used*)
+ by (metis (no_types, opaque_lifting) inverse_eq_divide mult.commute mult.left_commute weight_scale_spmf)
qed
- then show "spmf ?lhs i = spmf ?rhs i"
- by(simp add: spmf_scale_spmf field_simps weight_scale_spmf)
qed
lemma scale_scale_spmf' [simp]:
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Mar 02 17:46:29 2023 +0100
@@ -57,7 +57,7 @@
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
space_implode " " (File.bash_path (Path.explode path) ::
- arguments ctxt false "" atp_timeout prob_file)
+ arguments false false "" atp_timeout prob_file)
val outcome =
Timeout.apply atp_timeout Isabelle_System.bash_output command
|> fst
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Mar 02 17:46:29 2023 +0100
@@ -64,6 +64,7 @@
val tptp_cnf : string
val tptp_fof : string
+ val tptp_tcf : string
val tptp_tff : string
val tptp_thf : string
val tptp_has_type : string
@@ -222,6 +223,7 @@
(* official TPTP syntax *)
val tptp_cnf = "cnf"
val tptp_fof = "fof"
+val tptp_tcf = "tcf" (* sometimes appears in E's output *)
val tptp_tff = "tff"
val tptp_thf = "thf"
val tptp_has_type = ":"
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Mar 02 17:46:29 2023 +0100
@@ -24,6 +24,7 @@
ProofMissing |
ProofIncomplete |
ProofUnparsable |
+ UnsoundProof of bool * string list |
TimedOut |
Inappropriate |
OutOfResources |
@@ -99,6 +100,8 @@
val atp_proof_of_tstplike_proof : bool -> string -> string atp_problem -> string ->
string atp_proof
+ val atp_abduce_candidates_of_output : string -> string atp_problem -> string ->
+ (string, string, (string, string atp_type) atp_term, string) atp_formula list
end;
structure ATP_Proof : ATP_PROOF =
@@ -142,6 +145,7 @@
ProofMissing |
ProofIncomplete |
ProofUnparsable |
+ UnsoundProof of bool * string list |
TimedOut |
Inappropriate |
OutOfResources |
@@ -158,12 +162,21 @@
else
""
+fun from_lemmas [] = ""
+ | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
+
fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable"
- | string_of_atp_failure Unprovable = "Unprovable problem"
+ | string_of_atp_failure Unprovable = "Problem unprovable"
| string_of_atp_failure GaveUp = "Gave up"
| string_of_atp_failure ProofMissing = "Proof missing"
| string_of_atp_failure ProofIncomplete = "Proof incomplete"
| string_of_atp_failure ProofUnparsable = "Proof unparsable"
+ | string_of_atp_failure (UnsoundProof (false, ss)) =
+ "Derived the lemma \"False\"" ^ from_lemmas ss ^
+ ", likely due to the use of an unsound type encoding"
+ | string_of_atp_failure (UnsoundProof (true, ss)) =
+ "Derived the lemma \"False\"" ^ from_lemmas ss ^
+ ", likely due to inconsistent axioms or \"sorry\"d lemmas"
| string_of_atp_failure TimedOut = "Timed out"
| string_of_atp_failure Inappropriate = "Problem outside the prover's scope"
| string_of_atp_failure OutOfResources = "Out of resources"
@@ -570,7 +583,8 @@
end)
fun parse_tstp_fol_line full problem =
- ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(")
+ ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tcf
+ || Scan.this_string tptp_tff) -- $$ "(")
|-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
-- (if full then parse_fol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi)
-- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
@@ -724,4 +738,58 @@
|> parse_proof full local_prover problem
|> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))))
+val e_symbol_prefixes = ["esk", "epred"]
+
+fun exists_name_in_term pred =
+ let
+ fun ex_name (ATerm ((s, _), tms)) = pred s orelse exists ex_name tms
+ | ex_name (AAbs ((_, tm), tms)) = exists ex_name (tm :: tms)
+ in ex_name end
+
+fun exists_name_in_formula pred phi =
+ formula_fold NONE (fn _ => fn tm => fn ex => ex orelse exists_name_in_term pred tm) phi false
+
+fun exists_symbol_in_formula prefixes =
+ exists_name_in_formula (fn s => exists (fn prefix => String.isPrefix prefix s) prefixes)
+
+fun atp_abduce_candidates_of_output local_prover problem output =
+ let
+ (* Truncate too large output to avoid memory issues. *)
+ val max_size = 1000000
+ val output =
+ if String.size output > max_size then
+ String.substring (output, 0, max_size)
+ else
+ output
+
+ fun fold_extract accum [] = accum
+ | fold_extract accum (line :: lines) =
+ if String.isSubstring "# info" line
+ andalso String.isSubstring "negated_conjecture" line then
+ if String.isSubstring ", 0, 0," line then
+ (* This pattern occurs in the "info()" comment of an E clause that directly emerges from
+ the conjecture. We don't want to tell the user that they can prove "P" by assuming
+ "P". *)
+ fold_extract accum lines
+ else
+ let
+ val clean_line =
+ (case space_explode "#" line of
+ [] => ""
+ | before_hash :: _ => before_hash)
+ in
+ (case try (parse_proof true local_prover problem) clean_line of
+ SOME [(_, _, phi, _, _)] =>
+ if local_prover = eN andalso exists_symbol_in_formula e_symbol_prefixes phi then
+ fold_extract accum lines
+ else
+ fold_extract (phi :: accum) lines
+ | _ => fold_extract accum lines)
+ end
+ else
+ fold_extract accum lines
+ in
+ fold_extract [] (split_lines output)
+ end
+
end;
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Mar 02 17:46:29 2023 +0100
@@ -44,6 +44,7 @@
bool -> int Symtab.table ->
(string, string, (string, string atp_type) atp_term, string) atp_formula -> term
+ val is_conjecture_used_in_proof : string atp_proof -> bool
val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
(string * stature) list
val atp_proof_prefers_lifting : string atp_proof -> bool
@@ -58,6 +59,11 @@
val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list
val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
(term, string) atp_step list
+ val termify_atp_abduce_candidate : Proof.context -> string -> ATP_Problem.atp_format ->
+ ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
+ int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula ->
+ term
+ val top_abduce_candidates : int -> term list -> term list
end;
structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -506,6 +512,8 @@
fun is_axiom_used_in_proof pred =
exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
+val is_conjecture_used_in_proof = is_axiom_used_in_proof (is_some o resolve_conjecture)
+
fun add_fact ctxt facts ((num, ss), _, _, rule, deps) =
(if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse
String.isPrefix satallax_tab_rule_prefix rule then
@@ -624,7 +632,7 @@
#> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop)
#> local_prover = waldmeisterN ? repair_waldmeister_endgame
-fun unskolemize_term skos =
+fun unskolemize_spass_term skos =
let
val is_skolem_name = member (op =) skos
@@ -653,10 +661,10 @@
val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1)
- fun unskolem t =
+ fun unskolem_inner t =
(case find_argless_skolem t of
SOME (x as (s, T)) =>
- HOLogic.exists_const T $ Abs (s, T, unskolem (safe_abstract_over (Free x, t)))
+ HOLogic.exists_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Free x, t)))
| NONE =>
(case find_skolem_arg t of
SOME (v as ((s, _), T)) =>
@@ -667,16 +675,19 @@
|> apply2 (fn lits => fold (curry s_disj) lits \<^term>\<open>False\<close>)
in
s_disj (HOLogic.all_const T
- $ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))),
- unskolem have_nots)
+ $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, kill_skolem_arg haves))),
+ unskolem_inner have_nots)
end
| NONE =>
(case find_var t of
SOME (v as ((s, _), T)) =>
- HOLogic.all_const T $ Abs (s, T, unskolem (safe_abstract_over (Var v, t)))
+ HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, t)))
| NONE => t)))
+
+ fun unskolem_outer (@{const Trueprop} $ t) = @{const Trueprop} $ unskolem_outer t
+ | unskolem_outer t = unskolem_inner t
in
- HOLogic.mk_Trueprop o unskolem o HOLogic.dest_Trueprop
+ unskolem_outer
end
fun rename_skolem_args t =
@@ -740,7 +751,7 @@
fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps []
val deps = map (snd #> #1) skoXss_steps
in
- [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
+ [(name0, Unknown, unskolemize_spass_term skos t, spass_pre_skolemize_rule, deps),
(name, Unknown, t, spass_skolemize_rule, [name0])]
end
@@ -782,4 +793,65 @@
map repair_deps atp_proof
end
+fun termify_atp_abduce_candidate ctxt local_prover format type_enc pool lifted sym_tab phi =
+ let
+ val proof = [(("", []), Conjecture, mk_anot phi, "", [])]
+ val new_proof = termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab proof
+ in
+ (case new_proof of
+ [(_, _, phi', _, _)] => phi'
+ | _ => error "Impossible case in termify_atp_abduce_candidate")
+ end
+
+fun sort_top n scored_items =
+ if n <= 0 orelse null scored_items then
+ []
+ else
+ let
+ fun split_min accum [] (_, best_item) = (best_item, List.rev accum)
+ | split_min accum ((score, item) :: scored_items) (best_score, best_item) =
+ if score < best_score then
+ split_min ((best_score, best_item) :: accum) scored_items (score, item)
+ else
+ split_min ((score, item) :: accum) scored_items (best_score, best_item)
+
+ val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items)
+ in
+ min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items)
+ |> distinct (op aconv)
+ end
+
+fun top_abduce_candidates max_candidates candidates =
+ let
+ (* We prefer free variables to other constructs, so that e.g. "x \<le> y" is
+ prioritized over "x \<le> 0". *)
+ fun score t =
+ Term.fold_aterms (fn t => fn score => score + (case t of Free _ => 1 | _ => 2)) t 0
+
+ (* Equations of the form "x = ..." or "... = x" or similar are too specific
+ to be useful. Quantified formulas are also filtered out. As for "True",
+ it may seem an odd choice for abduction, but it sometimes arises in
+ conjunction with type class constraints, which are removed by the
+ termifier. *)
+ fun maybe_score t =
+ (case t of
+ @{prop True} => NONE
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE
+ | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE
+ | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE
+ | @{const Trueprop} $ (@{const less_eq(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE
+ | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const one_class.one(nat)}) => NONE
+ | @{const Trueprop} $ (@{const Not} $
+ (@{const less(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
+ | @{const Trueprop} $ (@{const Not} $
+ (@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE
+ | @{const Trueprop} $ (@{const Not} $
+ (@{const less_eq(nat)} $ @{const one_class.one(nat)} $ _)) => NONE
+ | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE
+ | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE
+ | _ => SOME (score t, t))
+ in
+ sort_top max_candidates (map_filter maybe_score candidates)
+ end
+
end;
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Mar 02 17:46:29 2023 +0100
@@ -62,8 +62,7 @@
val timestamp = timestamp_format o Time.now
(* This hash function is recommended in "Compilers: Principles, Techniques, and
- Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
- particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
+ Tools" by Aho, Sethi, and Ullman. *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
@@ -416,8 +415,8 @@
val map_prod = Ctr_Sugar_Util.map_prod
-(* Compare the length of a list with an integer n while traversing at most n elements of the list.
-*)
+(* Compare the length of a list with an integer n while traversing at most n
+elements of the list. *)
fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
| compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 02 17:46:29 2023 +0100
@@ -24,7 +24,8 @@
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
| SH_Unknown
- | SH_Timeout
+ | SH_TimeOut
+ | SH_ResourcesOut
| SH_None
val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string
@@ -57,12 +58,14 @@
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
| SH_Unknown
-| SH_Timeout
+| SH_TimeOut
+| SH_ResourcesOut
| SH_None
fun short_string_of_sledgehammer_outcome (SH_Some _) = "some"
| short_string_of_sledgehammer_outcome SH_Unknown = "unknown"
- | short_string_of_sledgehammer_outcome SH_Timeout = "timeout"
+ | short_string_of_sledgehammer_outcome SH_TimeOut = "timeout"
+ | short_string_of_sledgehammer_outcome SH_ResourcesOut = "resources_out"
| short_string_of_sledgehammer_outcome SH_None = "none"
fun alternative f (SOME x) (SOME y) = SOME (f (x, y))
@@ -79,18 +82,20 @@
fun max_outcome outcomes =
let
val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
+ val timeout = find_first (fn (SH_TimeOut, _) => true | _ => false) outcomes
+ val resources_out = find_first (fn (SH_ResourcesOut, _) => true | _ => false) outcomes
val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes
- val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes
val none = find_first (fn (SH_None, _) => true | _ => false) outcomes
in
some
|> alternative snd unknown
|> alternative snd timeout
+ |> alternative snd resources_out
|> alternative snd none
|> the_default (SH_Unknown, "")
end
-fun play_one_line_proofs minimize timeout used_facts state i methss =
+fun play_one_line_proofs minimize timeout used_facts state goal i methss =
(if timeout = Time.zeroTime then
[]
else
@@ -98,7 +103,7 @@
val ctxt = Proof.context_of state
val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
val fact_names = map fst used_facts
- val {facts = chained, goal, ...} = Proof.goal state
+ val {facts = chained, ...} = Proof.goal state
val goal_t = Logic.get_goal (Thm.prop_of goal) i
fun try_methss ress [] = ress
@@ -154,20 +159,18 @@
fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
(problem as {state, subgoal, factss, ...} : prover_problem)
- (slice as ((slice_size, abduce, check_consistent, num_facts, fact_filter), _)) name =
+ (slice as ((slice_size, abduce, falsify, num_facts, fact_filter), _)) name =
let
val ctxt = Proof.context_of state
val _ = spying spy (fn () => (state, subgoal, name,
- "Launched" ^ (if abduce then " (abduce)" else "") ^
- (if check_consistent then " (check_consistent)" else "")))
+ "Launched" ^ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "")))
val _ =
if verbose then
writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^
- (if abduce then " (abduce)" else "") ^
- (if check_consistent then " (check_consistent)" else "") ^ "...")
+ (if abduce then " (abduce)" else "") ^ (if falsify then " (falsify)" else "") ^ "...")
else
()
@@ -177,8 +180,7 @@
|> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
- |> prefix ("Facts in " ^ name ^ " " ^
- (if check_consistent then "inconsistency" else "proof") ^ ": ")
+ |> prefix ("Facts in " ^ name ^ " " ^ (if falsify then "falsification" else "proof") ^ ": ")
|> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -206,7 +208,7 @@
|> AList.group (op =)
|> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
in
- "Success: Found " ^ (if check_consistent then "inconsistency" else "proof") ^ " with " ^
+ "Success: Found " ^ (if falsify then "falsification" else "proof") ^ " with " ^
string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^
(if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
end
@@ -220,18 +222,20 @@
|> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
end
-fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal
+fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state goal subgoal
(result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
let
val (output, chosen_preplay_outcome) =
if outcome = SOME ATP_Proof.TimedOut then
- (SH_Timeout, select_one_line_proof used_facts (fst preferred_methss) [])
+ (SH_TimeOut, select_one_line_proof used_facts (fst preferred_methss) [])
+ else if outcome = SOME ATP_Proof.OutOfResources then
+ (SH_ResourcesOut, select_one_line_proof used_facts (fst preferred_methss) [])
else if is_some outcome then
(SH_None, select_one_line_proof used_facts (fst preferred_methss) [])
else
let
val preplay_results =
- play_one_line_proofs minimize preplay_timeout used_facts state subgoal
+ play_one_line_proofs minimize preplay_timeout used_facts state goal subgoal
(snd preferred_methss)
val chosen_preplay_outcome =
select_one_line_proof used_facts (fst preferred_methss) preplay_results
@@ -243,9 +247,11 @@
(output, output_message)
end
-fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) =
+fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) =
if outcome = SOME ATP_Proof.TimedOut then
- (SH_Timeout, K "")
+ (SH_TimeOut, K "")
+ else if outcome = SOME ATP_Proof.OutOfResources then
+ (SH_ResourcesOut, K "")
else if is_some outcome then
(SH_None, K "")
else
@@ -253,9 +259,9 @@
(if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then
(case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of
[] => "The goal is inconsistent"
- | facts => "The goal is inconsistent with these facts: " ^ commas facts)
+ | facts => "The goal is falsified by these facts: " ^ commas facts)
else
- "The following facts are inconsistent: " ^
+ "Derived \"False\" from these facts alone: " ^
commas (map fst used_facts)))
fun check_expected_outcome ctxt prover_name expect outcome =
@@ -275,14 +281,15 @@
else
error ("Unexpected outcome: the external prover found a proof but preplay failed")
| ("unknown", SH_Unknown) => ()
- | ("timeout", SH_Timeout) => ()
+ | ("timeout", SH_TimeOut) => ()
+ | ("resources_out", SH_ResourcesOut) => ()
| ("none", SH_None) => ()
| _ => error ("Unexpected outcome: " ^ quote outcome_code))
end
-fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode found_something
- writeln_result learn (problem as {state, subgoal, ...})
- (slice as ((_, _, check_consistent, _, _), _)) prover_name =
+fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode
+ has_already_found_something found_something writeln_result learn
+ (problem as {state, subgoal, ...}) (slice as ((_, _, falsify, _, _), _)) prover_name =
let
val ctxt = Proof.context_of state
val hard_timeout = Time.scale 5.0 timeout
@@ -306,15 +313,16 @@
in
{comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1,
subgoal_count = 1, factss = map (apsnd (append new_facts)) factss,
+ has_already_found_something = has_already_found_something,
found_something = found_something "an inconsistency"}
end
- val problem = problem |> check_consistent ? flip_problem
+ val problem as {goal, ...} = problem |> falsify ? flip_problem
fun really_go () =
launch_prover params mode learn problem slice prover_name
- |> (if check_consistent then analyze_prover_result_for_consistency else
- preplay_prover_result params state subgoal)
+ |> (if falsify then analyze_prover_result_for_inconsistency else
+ preplay_prover_result params state goal subgoal)
fun go () =
if debug then
@@ -322,10 +330,10 @@
else
(really_go ()
handle
- ERROR msg => (SH_Unknown, fn () => "Warning: " ^ msg ^ "\n")
+ ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
| exn =>
if Exn.is_interrupt exn then Exn.reraise exn
- else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
+ else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n"))
val (outcome, message) = Timeout.apply hard_timeout go ()
val () = check_expected_outcome ctxt prover_name expect outcome
@@ -354,11 +362,10 @@
val default_slice_schedule =
(* FUDGE (loosely inspired by Seventeen evaluation) *)
- [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N,
- zipperpositionN, cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN,
- cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN,
- vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN,
- zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, cvc4N,
+ [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN,
+ cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN,
+ spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN,
+ iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N,
zipperpositionN]
fun schedule_of_provers provers num_slices =
@@ -380,16 +387,16 @@
@ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
end
-fun prover_slices_of_schedule ctxt factss
- ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
+fun prover_slices_of_schedule ctxt goal subgoal factss
+ ({abduce, falsify, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
...} : params)
schedule =
let
fun triplicate_slices original =
let
val shift =
- map (apfst (fn (slice_size, abduce, check_consistent, num_facts, fact_filter) =>
- (slice_size, abduce, check_consistent, num_facts,
+ map (apfst (fn (slice_size, abduce, falsify, num_facts, fact_filter) =>
+ (slice_size, abduce, falsify, num_facts,
if fact_filter = mashN then mepoN
else if fact_filter = mepoN then meshN
else mashN)))
@@ -407,16 +414,23 @@
| adjust_extra (extra as SMT_Slice _) = extra
fun adjust_slice max_slice_size
- ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) =
+ ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) =
let
val slice_size = Int.min (max_slice_size, slice_size0)
- val abduce = abduce |> the_default abduce0
- val check_consistent = check_consistent |> the_default check_consistent0
+ val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False})
+ val abduce =
+ (case abduce of
+ NONE => abduce0 andalso goal_not_False
+ | SOME max_candidates => max_candidates > 0)
+ val falsify =
+ (case falsify of
+ NONE => falsify0 andalso goal_not_False
+ | SOME falsify => falsify)
val fact_filter = fact_filter |> the_default fact_filter0
val max_facts = max_facts |> the_default num_facts0
val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
in
- ((slice_size, abduce, check_consistent, num_facts, fact_filter), adjust_extra extra)
+ ((slice_size, abduce, falsify, num_facts, fact_filter), adjust_extra extra)
end
val provers = distinct (op =) schedule
@@ -445,9 +459,8 @@
|> distinct (op =)
end
-fun run_sledgehammer (params as {verbose, spy, provers, check_consistent, induction_rules,
- max_facts, max_proofs, slices, ...})
- mode writeln_result i (fact_override as {only, ...}) state =
+fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts,
+ max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state =
if null provers then
error "No prover is set"
else
@@ -458,11 +471,17 @@
val _ = Proof.assert_backward state
val print = if mode = Normal andalso is_none writeln_result then writeln else K ()
- val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0
+ val found_proofs_and_falsifications = Synchronized.var "found_proofs_and_falsifications" 0
+
+ fun has_already_found_something () =
+ if mode = Normal then
+ Synchronized.value found_proofs_and_falsifications > 0
+ else
+ false
fun found_something a_proof_or_inconsistency prover_name =
if mode = Normal then
- (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1);
+ (Synchronized.change found_proofs_and_falsifications (fn n => n + 1);
(the_default writeln writeln_result) (prover_name ^ " found " ^
a_proof_or_inconsistency ^ "..."))
else
@@ -521,14 +540,16 @@
val factss = get_factss provers
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = factss, found_something = found_something "a proof"}
+ factss = factss, has_already_found_something = has_already_found_something,
+ found_something = found_something "a proof"}
val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
- val launch = launch_prover_and_preplay params mode found_something writeln_result learn
+ val launch = launch_prover_and_preplay params mode has_already_found_something
+ found_something writeln_result learn
val schedule =
if mode = Auto_Try then provers
else schedule_of_provers provers slices
- val prover_slices = prover_slices_of_schedule ctxt factss params schedule
+ val prover_slices = prover_slices_of_schedule ctxt goal i factss params schedule
val _ =
if verbose then
@@ -545,32 +566,33 @@
else
(learn chained_thms;
Par_List.map (fn (prover, slice) =>
- if Synchronized.value found_proofs_and_inconsistencies < max_proofs then
+ if Synchronized.value found_proofs_and_falsifications < max_proofs then
launch problem slice prover
else
(SH_None, ""))
prover_slices
|> max_outcome)
end
+
+ fun normal_failure () =
+ (the_default writeln writeln_result
+ ("No " ^ (if falsify = SOME true then "falsification" else "proof") ^
+ " found");
+ false)
in
(launch_provers ()
- handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
+ handle Timeout.TIMEOUT _ => (SH_TimeOut, ""))
|> `(fn (outcome, message) =>
(case outcome of
SH_Some _ => (the_default writeln writeln_result "Done"; true)
- | SH_Unknown => (the_default writeln writeln_result message; false)
- | SH_Timeout =>
- (the_default writeln writeln_result
- ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^
- " found");
- false)
- | SH_None => (the_default writeln writeln_result
- (if message = "" then
- "No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^
- " found"
- else
- "Warning: " ^ message);
- false)))
+ | SH_Unknown =>
+ if message = "" then normal_failure ()
+ else (the_default writeln writeln_result ("Warning: " ^ message); false)
+ | SH_TimeOut => normal_failure ()
+ | SH_ResourcesOut => normal_failure ()
+ | SH_None =>
+ if message = "" then normal_failure ()
+ else (the_default writeln writeln_result ("Warning: " ^ message); false)))
end)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Mar 02 17:46:29 2023 +0100
@@ -15,7 +15,7 @@
type atp_slice = atp_format * string * string * bool * string
type atp_config =
{exec : string list * string list,
- arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list,
+ arguments : bool -> bool -> string -> Time.time -> Path.T -> string list,
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
@@ -67,7 +67,7 @@
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
-(* desired slice size, abduce, check_consistent, desired number of facts, fact filter *)
+(* desired slice size, abduce, falsify, desired number of facts, fact filter *)
type base_slice = int * bool * bool * int * string
(* problem file format, type encoding, lambda translation scheme, uncurried aliases?,
@@ -76,7 +76,7 @@
type atp_config =
{exec : string list * string list,
- arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list,
+ arguments : bool -> bool -> string -> Time.time -> Path.T -> string list,
proof_delims : (string * string) list,
known_failures : (atp_failure * string) list,
prem_role : atp_formula_role,
@@ -176,10 +176,13 @@
val e_config : atp_config =
{exec = (["E_HOME"], ["eprover-ho", "eprover"]),
- arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem =>
- ["--tstp-in --tstp-out --silent " ^ extra_options ^
- " --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^
- File.bash_path problem],
+ arguments = fn abduce => fn _ => fn extra_options => fn timeout => fn problem =>
+ ["--tstp-in --tstp-out --silent " ^
+ (if abduce then
+ "--auto --print-saturated=ieIE --print-sat-info --soft-cpu-limit="
+ else
+ extra_options ^ " --cpu-limit=") ^
+ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem],
proof_delims =
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
tstp_proof_delims,
@@ -192,8 +195,9 @@
good_slices =
let
val (format, type_enc, lam_trans, extra_options) =
- if string_ord (getenv "E_VERSION", "2.7") <> LESS then
- (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
+ if string_ord (getenv "E_VERSION", "3.0") <> LESS then
+ (* '$ite' support appears to be unsound. *)
+ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule")
else
@@ -201,11 +205,11 @@
in
(* FUDGE *)
K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)),
((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, false, 128, mepoN), (format, type_enc, lam_trans, false, extra_options)),
+ ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)),
((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)),
- ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options)),
- ((1000 (* infinity *), false, false, 64, mashN), (format, type_enc, combsN, false, extra_options))]
+ ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))]
end,
good_max_mono_iters = default_max_mono_iters,
good_max_new_mono_instances = default_max_new_mono_instances}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 02 17:46:29 2023 +0100
@@ -54,7 +54,7 @@
("overlord", "false"),
("spy", "false"),
("abduce", "smart"),
- ("check_consistent", "smart"),
+ ("falsify", "smart"),
("type_enc", "smart"),
("strict", "false"),
("lam_trans", "smart"),
@@ -77,6 +77,7 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
+ ("dont_abduce", ("abduce", ["0"])),
("dont_preplay", ("preplay_timeout", ["0"])),
("dont_compress", ("compress", ["1"])),
("dont_slice", ("slices", ["1"])),
@@ -86,8 +87,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("dont_spy", "spy"),
- ("dont_abduce", "abduce"),
- ("dont_check_consistent", "check_consistent"),
+ ("dont_falsify", "falsify"),
("non_strict", "strict"),
("no_uncurried_aliases", "uncurried_aliases"),
("dont_learn", "learn"),
@@ -232,16 +232,12 @@
val overlord = lookup_bool "overlord"
val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd
- val check_consistent =
- if mode = Auto_Try then
- SOME false
- else
- lookup_option lookup_bool "check_consistent"
val abduce =
- if mode = Auto_Try then
- SOME false
- else
- lookup_option lookup_bool "abduce"
+ if mode = Auto_Try then SOME 0
+ else lookup_option lookup_int "abduce"
+ val falsify =
+ if mode = Auto_Try then SOME false
+ else lookup_option lookup_bool "falsify"
val type_enc =
if mode = Auto_Try then
NONE
@@ -275,7 +271,7 @@
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
- abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict,
+ abduce = abduce, falsify = falsify, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn,
fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 02 17:46:29 2023 +0100
@@ -21,6 +21,7 @@
val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int ->
one_line_params -> string
+ val abduce_text : Proof.context -> term list -> string
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -528,4 +529,8 @@
else
one_line_proof_text ctxt num_chained) one_line_params
+fun abduce_text ctxt tms =
+ "Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^
+ cat_lines (map (Syntax.string_of_term ctxt) tms)
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 02 17:46:29 2023 +0100
@@ -868,7 +868,8 @@
let
val problem =
{comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
- subgoal_count = 1, factss = [("", facts)], found_something = K ()}
+ subgoal_count = 1, factss = [("", facts)], has_already_found_something = K false,
+ found_something = K ()}
val slice = hd (get_slices ctxt prover)
in
get_minimizing_prover ctxt MaSh (K ()) prover params problem slice
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 02 17:46:29 2023 +0100
@@ -29,8 +29,8 @@
overlord : bool,
spy : bool,
provers : string list,
- abduce : bool option,
- check_consistent : bool option,
+ abduce : int option,
+ falsify : bool option,
type_enc : string option,
strict : bool,
lam_trans : string option,
@@ -63,6 +63,7 @@
subgoal : int,
subgoal_count : int,
factss : (string * fact list) list,
+ has_already_found_something : unit -> bool,
found_something : string -> unit}
datatype prover_slice_extra =
@@ -82,6 +83,7 @@
type prover = params -> prover_problem -> prover_slice -> prover_result
val SledgehammerN : string
+ val default_abduce_max_candidates : int
val str_of_mode : mode -> string
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
@@ -113,6 +115,8 @@
(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)
val SledgehammerN = "Sledgehammer"
+val default_abduce_max_candidates = 1
+
datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
fun str_of_mode Auto_Try = "Auto Try"
@@ -136,8 +140,8 @@
overlord : bool,
spy : bool,
provers : string list,
- abduce : bool option,
- check_consistent : bool option,
+ abduce : int option,
+ falsify : bool option,
type_enc : string option,
strict : bool,
lam_trans : string option,
@@ -182,6 +186,7 @@
subgoal : int,
subgoal_count : int,
factss : (string * fact list) list,
+ has_already_found_something : unit -> bool,
found_something : string -> unit}
datatype prover_slice_extra =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Mar 02 17:46:29 2023 +0100
@@ -99,15 +99,17 @@
| suffix_of_mode Minimize = "_min"
(* Important messages are important but not so important that users want to see them each time. *)
-val atp_important_message_keep_quotient = 25
+val important_message_keep_quotient = 25
fun run_atp mode name
- ({debug, verbose, overlord, strict, max_mono_iters, max_new_mono_instances, isar_proofs,
- compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params)
- ({comment, state, goal, subgoal, subgoal_count, factss, found_something} : prover_problem)
+ ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters,
+ max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout,
+ preplay_timeout, spy, ...} : params)
+ ({comment, state, goal, subgoal, subgoal_count, factss, has_already_found_something,
+ found_something} : prover_problem)
slice =
let
- val (basic_slice as (slice_size, _, _, _, _),
+ val (basic_slice as (slice_size, abduce, _, _, _),
ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) =
slice
val facts = facts_of_basic_slice basic_slice factss
@@ -185,11 +187,12 @@
val strictness = if strict then Strict else Non_Strict
val type_enc = choose_type_enc strictness good_format good_type_enc
val run_timeout = slice_timeout slice_size slices timeout
- val generous_run_timeout = if mode = MaSh then one_day else run_timeout
+ val generous_run_timeout =
+ if mode = MaSh then one_day
+ else if abduce then run_timeout + seconds 5.0
+ else run_timeout
val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () =>
- let
- val readable_names = not (Config.get ctxt atp_full_names)
- in
+ let val readable_names = not (Config.get ctxt atp_full_names) in
facts
|> not (is_type_enc_sound type_enc) ?
filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
@@ -203,7 +206,7 @@
(state, subgoal, name, "Generating ATP problem in " ^
string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
- val args = arguments ctxt full_proofs extra run_timeout prob_path
+ val args = arguments abduce full_proofs extra run_timeout prob_path
val command = space_implode " " (File.bash_path executable :: args)
fun run_command () =
@@ -220,6 +223,8 @@
cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
|> File.write_list prob_path
+ val local_name = name |> perhaps (try (unprefix remote_prefix))
+
val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) =
Timeout.apply generous_run_timeout run_command ()
|>> overlord ?
@@ -227,30 +232,36 @@
|> (fn accum as (output, _) =>
(accum,
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
- |>> `(atp_proof_of_tstplike_proof false (perhaps (try (unprefix remote_prefix)) name)
- atp_problem)
+ |>> `(atp_proof_of_tstplike_proof false local_name atp_problem)
handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable)))
handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut))
| ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg)))
+ val atp_abduce_candidates =
+ if abduce andalso outcome <> NONE andalso not (has_already_found_something ()) then
+ atp_abduce_candidates_of_output local_name atp_problem output
+ else
+ []
+
val () = spying spy (fn () =>
(state, subgoal, name, "Running command in " ^
string_of_int (Time.toMilliseconds run_time) ^ " ms"))
- val _ =
+ val outcome =
(case outcome of
- NONE => found_something name
- | _ => ())
+ NONE => (found_something name; NONE)
+ | _ => outcome)
in
(atp_problem_data,
- (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, outcome),
+ (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates,
+ outcome),
(good_format, type_enc))
end
- (* If the problem file has not been exported, remove it; otherwise, export
- the proof file too. *)
+ (* If the problem file has not been exported, remove it; otherwise, export the proof file
+ too. *)
fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else ()
- fun export (_, (output, _, _, _, _, _, _), _) =
+ fun export (_, (output, _, _, _, _, _, _, _), _) =
let
val proof_dest_dir_path = Path.explode proof_dest_dir
val make_export_file_name =
@@ -259,7 +270,8 @@
#> swap
#> uncurry Path.ext
in
- if proof_dest_dir = "" then Output.system_message "don't export proof"
+ if proof_dest_dir = "" then
+ Output.system_message "don't export proof"
else if File.exists proof_dest_dir_path then
File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output
else
@@ -267,20 +279,28 @@
end
val ((_, pool, lifted, sym_tab),
- (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, outcome),
+ (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof,
+ atp_abduce_candidates, outcome),
(format, type_enc)) =
with_cleanup clean_up run () |> tap export
val important_message =
- if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0
+ if mode = Normal andalso Random.random_range 0 (important_message_keep_quotient - 1) = 0
then extract_important_message output
else ""
- val (used_facts, preferred_methss, message) =
+ val (outcome, used_facts, preferred_methss, message) =
(case outcome of
NONE =>
let
val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
+ val _ =
+ if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof)
+ andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then
+ warning ("Derived \"False\" from these facts alone: " ^ commas (map fst used_facts))
+ else
+ ()
+
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val preferred = Metis_Method (NONE, NONE)
val preferred_methss =
@@ -291,7 +311,7 @@
else
[[preferred]])
in
- (used_facts, preferred_methss,
+ (NONE, used_facts, preferred_methss,
fn preplay =>
let
val _ = if verbose then writeln "Generating proof text..." else ()
@@ -330,7 +350,19 @@
end)
end
| SOME failure =>
- ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
+ let
+ val max_abduce_candidates =
+ the_default default_abduce_max_candidates abduce_max_candidates
+ val abduce_candidates = atp_abduce_candidates
+ |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab)
+ |> top_abduce_candidates max_abduce_candidates
+ in
+ if null abduce_candidates then
+ (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)
+ else
+ (NONE, [], (Auto_Method (* dummy *), []), fn _ =>
+ abduce_text ctxt abduce_candidates)
+ end)
in
{outcome = outcome, used_facts = used_facts, used_from = used_from,
preferred_methss = preferred_methss, run_time = run_time, message = message}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Mar 02 17:46:29 2023 +0100
@@ -83,8 +83,8 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
minimize, preplay_timeout, induction_rules, ...} : params)
- (slice as ((_, abduce, check_consistent, _, _), _)) silent (prover : prover) timeout i n state
- goal facts =
+ (slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
+ state goal facts =
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
(if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -92,8 +92,8 @@
val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
- type_enc = type_enc, abduce = SOME abduce, check_consistent = SOME check_consistent,
- strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
+ type_enc = type_enc, abduce = SOME 0, falsify = SOME false, strict = strict,
+ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false,
fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts),
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, max_proofs = 1,
@@ -102,10 +102,10 @@
expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = [("", facts)], found_something = K ()}
+ factss = [("", facts)], has_already_found_something = K false, found_something = K ()}
val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
message} =
- prover params problem slice
+ prover params problem ((1, false, false, length facts, fact_filter), slice_extra)
val result as {outcome, ...} =
if is_none outcome0 andalso
forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then
@@ -118,14 +118,12 @@
(case outcome of
SOME failure => string_of_atp_failure failure
| NONE =>
- "Found " ^ (if check_consistent then "inconsistency" else "proof") ^
+ "Found " ^ (if falsify then "falsification" else "proof") ^
(if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
" (" ^ string_of_time run_time ^ ")"));
result
end
-(* minimalization of facts *)
-
(* Give the external prover some slack. The ATP gets further slack because the
Sledgehammer preprocessing time is included in the estimate below but isn't
part of the timeout. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Thu Mar 02 17:05:24 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Thu Mar 02 17:46:29 2023 +0100
@@ -45,7 +45,7 @@
|> hd |> snd
val problem =
{comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- factss = [("", facts)], found_something = K ()}
+ factss = [("", facts)], has_already_found_something = K false, found_something = K ()}
val slice = hd (get_slices ctxt name)
in
(case prover params problem slice of