--- a/src/HOL/Analysis/Derivative.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Analysis/Derivative.thy Fri Sep 29 11:19:43 2023 +0200
@@ -2403,6 +2403,12 @@
unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_intros)
+lemma deriv_compose_linear':
+ assumes "f field_differentiable at (c*z + a)"
+ shows "deriv (\<lambda>w. f (c*w + a)) z = c * deriv f (c*z + a)"
+ apply (subst deriv_chain [where f="\<lambda>w. c*w + a",unfolded comp_def])
+ using assms by (auto intro: derivative_intros)
+
lemma deriv_compose_linear:
assumes "f field_differentiable at (c * z)"
shows "deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
@@ -2413,7 +2419,6 @@
by simp
qed
-
lemma nonzero_deriv_nonconstant:
assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
shows "\<not> f constant_on S"
--- a/src/HOL/Analysis/Path_Connected.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Sep 29 11:19:43 2023 +0200
@@ -447,6 +447,18 @@
"simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} \<noteq> {}"
by (simp add: simple_path_endless)
+lemma simple_path_continuous_image:
+ assumes "simple_path f" "continuous_on (path_image f) g" "inj_on g (path_image f)"
+ shows "simple_path (g \<circ> f)"
+ unfolding simple_path_def
+proof
+ show "path (g \<circ> f)"
+ using assms unfolding simple_path_def by (intro path_continuous_image) auto
+ from assms have [simp]: "g (f x) = g (f y) \<longleftrightarrow> f x = f y" if "x \<in> {0..1}" "y \<in> {0..1}" for x y
+ unfolding inj_on_def path_image_def using that by fastforce
+ show "loop_free (g \<circ> f)"
+ using assms(1) by (auto simp: loop_free_def simple_path_def)
+qed
subsection\<^marker>\<open>tag unimportant\<close>\<open>The operations on paths\<close>
--- a/src/HOL/Analysis/Uniform_Limit.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy Fri Sep 29 11:19:43 2023 +0200
@@ -56,12 +56,28 @@
unfolding uniform_limit_iff eventually_at
by (fastforce dest: spec[where x = "e / 2" for e])
+lemma uniform_limit_compose:
+ assumes ul: "uniform_limit X g l F"
+ and cont: "uniformly_continuous_on U f"
+ and g: "\<forall>\<^sub>F n in F. g n ` X \<subseteq> U" and l: "l ` X \<subseteq> U"
+ shows "uniform_limit X (\<lambda>a b. f (g a b)) (f \<circ> l) F"
+proof (rule uniform_limitI)
+ fix \<epsilon>::real
+ assume "0 < \<epsilon>"
+ then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<And>u v. \<lbrakk>u\<in>U; v\<in>U; dist u v < \<delta>\<rbrakk> \<Longrightarrow> dist (f u) (f v) < \<epsilon>"
+ by (metis cont uniformly_continuous_on_def)
+ show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) ((f \<circ> l) x) < \<epsilon>"
+ using uniform_limitD [OF ul \<open>\<delta>>0\<close>] g unfolding o_def
+ by eventually_elim (use \<delta> l in blast)
+qed
+
lemma metric_uniform_limit_imp_uniform_limit:
assumes f: "uniform_limit S f a F"
assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
shows "uniform_limit S g b F"
proof (rule uniform_limitI)
- fix e :: real assume "0 < e"
+ fix e :: real
+ assume "0 < e"
from uniform_limitD[OF f this] le
show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
by eventually_elim force
--- a/src/HOL/Complex.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Complex.thy Fri Sep 29 11:19:43 2023 +0200
@@ -769,6 +769,14 @@
lemma Im_sum[simp]: "Im (sum f s) = (\<Sum>x\<in>s. Im(f x))"
by (induct s rule: infinite_finite_induct) auto
+lemma Rats_complex_of_real_iff [iff]: "complex_of_real x \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+proof -
+ have "\<And>a b. \<lbrakk>0 < b; x = complex_of_int a / complex_of_int b\<rbrakk> \<Longrightarrow> x \<in> \<rat>"
+ by (metis Rats_divide Rats_of_int Re_complex_of_real Re_divide_of_real of_real_of_int_eq)
+ then show ?thesis
+ by (auto simp: elim!: Rats_cases')
+qed
+
lemma sum_Re_le_cmod: "(\<Sum>i\<in>I. Re (z i)) \<le> cmod (\<Sum>i\<in>I. z i)"
by (metis Re_sum complex_Re_le_cmod)
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Fri Sep 29 11:19:43 2023 +0200
@@ -379,8 +379,14 @@
qed
lemma holomorphic_deriv [holomorphic_intros]:
- "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on S"
-by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
+ "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on S"
+ by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
+
+lemma holomorphic_deriv_compose:
+ assumes g: "g holomorphic_on B" and f: "f holomorphic_on A" and "f ` A \<subseteq> B" "open B"
+ shows "(\<lambda>x. deriv g (f x)) holomorphic_on A"
+ using holomorphic_on_compose_gen [OF f holomorphic_deriv[OF g]] assms
+ by (auto simp: o_def)
lemma analytic_deriv [analytic_intros]: "f analytic_on S \<Longrightarrow> (deriv f) analytic_on S"
using analytic_on_holomorphic holomorphic_deriv by auto
@@ -625,51 +631,64 @@
by (induction i arbitrary: z)
(auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)
-lemma higher_deriv_compose_linear:
+lemma higher_deriv_compose_linear':
fixes z::complex
assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \<in> S"
- and fg: "\<And>w. w \<in> S \<Longrightarrow> u * w \<in> T"
- shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
+ and fg: "\<And>w. w \<in> S \<Longrightarrow> u*w + c \<in> T"
+ shows "(deriv ^^ n) (\<lambda>w. f (u*w + c)) z = u^n * (deriv ^^ n) f (u*z + c)"
using z
proof (induction n arbitrary: z)
case 0 then show ?case by simp
next
case (Suc n z)
- have holo0: "f holomorphic_on (*) u ` S"
+ have holo0: "f holomorphic_on (\<lambda>w. u * w+c) ` S"
by (meson fg f holomorphic_on_subset image_subset_iff)
- have holo2: "(deriv ^^ n) f holomorphic_on (*) u ` S"
+ have holo2: "(deriv ^^ n) f holomorphic_on (\<lambda>w. u * w+c) ` S"
by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
- have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S"
+ have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z+c)) holomorphic_on S"
by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
- have u: "(*) u holomorphic_on S" "f holomorphic_on (*) u ` S"
+ have "(\<lambda>w. u * w+c) holomorphic_on S" "f holomorphic_on (\<lambda>w. u * w+c) ` S"
by (rule holo0 holomorphic_intros)+
- then have holo1: "(\<lambda>w. f (u * w)) holomorphic_on S"
+ then have holo1: "(\<lambda>w. f (u * w+c)) holomorphic_on S"
by (rule holomorphic_on_compose [where g=f, unfolded o_def])
- have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z)) z"
+ have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w+c))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z+c)) z"
proof (rule complex_derivative_transform_within_open [OF _ holo3 S Suc.prems])
- show "(deriv ^^ n) (\<lambda>w. f (u * w)) holomorphic_on S"
+ show "(deriv ^^ n) (\<lambda>w. f (u * w+c)) holomorphic_on S"
by (rule holomorphic_higher_deriv [OF holo1 S])
qed (simp add: Suc.IH)
- also have "\<dots> = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
+ also have "\<dots> = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z+c)) z"
proof -
have "(deriv ^^ n) f analytic_on T"
by (simp add: analytic_on_open f holomorphic_higher_deriv T)
- then have "(\<lambda>w. (deriv ^^ n) f (u * w)) analytic_on S"
- by (meson S u analytic_on_open holo2 holomorphic_on_compose holomorphic_transform o_def)
+ then have "(\<lambda>w. (deriv ^^ n) f (u * w+c)) analytic_on S"
+ proof -
+ have "(deriv ^^ n) f \<circ> (\<lambda>w. u * w+c) holomorphic_on S"
+ using holomorphic_on_compose[OF _ holo2] \<open>(\<lambda>w. u * w+c) holomorphic_on S\<close>
+ by simp
+ then show ?thesis
+ by (simp add: S analytic_on_open o_def)
+ qed
then show ?thesis
by (intro deriv_cmult analytic_on_imp_differentiable_at [OF _ Suc.prems])
qed
- also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
+ also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z+c)"
proof -
- have "(deriv ^^ n) f field_differentiable at (u * z)"
+ have "(deriv ^^ n) f field_differentiable at (u * z+c)"
using Suc.prems T f fg holomorphic_higher_deriv holomorphic_on_imp_differentiable_at by blast
then show ?thesis
- by (simp add: deriv_compose_linear)
+ by (simp add: deriv_compose_linear')
qed
finally show ?case
by simp
qed
+lemma higher_deriv_compose_linear:
+ fixes z::complex
+ assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \<in> S"
+ and fg: "\<And>w. w \<in> S \<Longrightarrow> u * w \<in> T"
+ shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
+ using higher_deriv_compose_linear' [where c=0] assms by simp
+
lemma higher_deriv_add_at:
assumes "f analytic_on {z}" "g analytic_on {z}"
shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Fri Sep 29 11:19:43 2023 +0200
@@ -1121,6 +1121,11 @@
by (metis Diff_empty contour_integrable_holomorphic finite.emptyI g os)
qed
+lemma analytic_imp_contour_integrable:
+ assumes "f analytic_on path_image p" "valid_path p"
+ shows "f contour_integrable_on p"
+ by (meson analytic_on_holomorphic assms contour_integrable_holomorphic_simple)
+
lemma continuous_on_inversediff:
fixes z:: "'a::real_normed_field" shows "z \<notin> S \<Longrightarrow> continuous_on S (\<lambda>w. 1 / (w - z))"
by (rule continuous_intros | force)+
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Fri Sep 29 11:19:43 2023 +0200
@@ -4,66 +4,6 @@
begin
-(* TODO: Move *)
-text \<open>TODO: Better than @{thm deriv_compose_linear}?\<close>
-lemma deriv_compose_linear':
- assumes "f field_differentiable at (c*z + a)"
- shows "deriv (\<lambda>w. f (c*w + a)) z = c * deriv f (c*z + a)"
- apply (subst deriv_chain[where f="\<lambda>w. c*w + a",unfolded comp_def])
- using assms by (auto intro:derivative_intros)
-
-text \<open>TODO: Better than @{thm higher_deriv_compose_linear}?\<close>
-lemma higher_deriv_compose_linear':
- fixes z::complex
- assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \<in> S"
- and fg: "\<And>w. w \<in> S \<Longrightarrow> u*w + c \<in> T"
- shows "(deriv ^^ n) (\<lambda>w. f (u*w + c)) z = u^n * (deriv ^^ n) f (u*z + c)"
-using z
-proof (induction n arbitrary: z)
- case 0 then show ?case by simp
-next
- case (Suc n z)
- have holo0: "f holomorphic_on (\<lambda>w. u * w+c) ` S"
- by (meson fg f holomorphic_on_subset image_subset_iff)
- have holo2: "(deriv ^^ n) f holomorphic_on (\<lambda>w. u * w+c) ` S"
- by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
- have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z+c)) holomorphic_on S"
- by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
- have "(\<lambda>w. u * w+c) holomorphic_on S" "f holomorphic_on (\<lambda>w. u * w+c) ` S"
- by (rule holo0 holomorphic_intros)+
- then have holo1: "(\<lambda>w. f (u * w+c)) holomorphic_on S"
- by (rule holomorphic_on_compose [where g=f, unfolded o_def])
- have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w+c))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z+c)) z"
- proof (rule complex_derivative_transform_within_open [OF _ holo3 S Suc.prems])
- show "(deriv ^^ n) (\<lambda>w. f (u * w+c)) holomorphic_on S"
- by (rule holomorphic_higher_deriv [OF holo1 S])
- qed (simp add: Suc.IH)
- also have "\<dots> = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z+c)) z"
- proof -
- have "(deriv ^^ n) f analytic_on T"
- by (simp add: analytic_on_open f holomorphic_higher_deriv T)
- then have "(\<lambda>w. (deriv ^^ n) f (u * w+c)) analytic_on S"
- proof -
- have "(deriv ^^ n) f \<circ> (\<lambda>w. u * w+c) holomorphic_on S"
- using holomorphic_on_compose[OF _ holo2] \<open>(\<lambda>w. u * w+c) holomorphic_on S\<close>
- by simp
- then show ?thesis
- by (simp add: S analytic_on_open o_def)
- qed
- then show ?thesis
- by (intro deriv_cmult analytic_on_imp_differentiable_at [OF _ Suc.prems])
- qed
- also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z+c)"
- proof -
- have "(deriv ^^ n) f field_differentiable at (u * z+c)"
- using Suc.prems T f fg holomorphic_higher_deriv holomorphic_on_imp_differentiable_at by blast
- then show ?thesis
- by (simp add: deriv_compose_linear')
- qed
- finally show ?case
- by simp
-qed
-
lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
by (metis fps_to_fls_of_nat of_nat_numeral)
--- a/src/HOL/Complex_Analysis/Meromorphic.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy Fri Sep 29 11:19:43 2023 +0200
@@ -2,23 +2,6 @@
imports Laurent_Convergence Riemann_Mapping
begin
-lemma analytic_at_cong:
- assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
- shows "f analytic_on {x} \<longleftrightarrow> g analytic_on {y}"
-proof -
- have "g analytic_on {x}" if "f analytic_on {x}" "eventually (\<lambda>x. f x = g x) (nhds x)" for f g
- proof -
- have "(\<lambda>y. f (x + y)) has_fps_expansion fps_expansion f x"
- by (rule analytic_at_imp_has_fps_expansion) fact
- also have "?this \<longleftrightarrow> (\<lambda>y. g (x + y)) has_fps_expansion fps_expansion f x"
- using that by (intro has_fps_expansion_cong refl) (auto simp: nhds_to_0' eventually_filtermap)
- finally show ?thesis
- by (rule has_fps_expansion_imp_analytic)
- qed
- from this[of f g] this[of g f] show ?thesis using assms
- by (auto simp: eq_commute)
-qed
-
definition remove_sings :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
"remove_sings f z = (if \<exists>c. f \<midarrow>z\<rightarrow> c then Lim (at z) f else 0)"
@@ -2330,4 +2313,4 @@
finally show ?thesis .
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Sep 29 11:19:43 2023 +0200
@@ -590,6 +590,68 @@
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
+lemma Sup_inverse_eq_inverse_Inf:
+ fixes f::"'b \<Rightarrow> 'a::{conditionally_complete_linorder,linordered_field}"
+ assumes "bdd_above (range f)" "L > 0" and geL: "\<And>x. f x \<ge> L"
+ shows "(SUP x. 1 / f x) = 1 / (INF x. f x)"
+proof (rule antisym)
+ have bdd_f: "bdd_below (range f)"
+ by (meson assms bdd_belowI2)
+ have "Inf (range f) \<ge> L"
+ by (simp add: cINF_greatest geL)
+ have bdd_invf: "bdd_above (range (\<lambda>x. 1 / f x))"
+ proof (rule bdd_aboveI2)
+ show "\<And>x. 1 / f x \<le> 1/L"
+ using assms by (auto simp: divide_simps)
+ qed
+ moreover have le_inverse_Inf: "1 / f x \<le> 1 / Inf (range f)" for x
+ proof -
+ have "Inf (range f) \<le> f x"
+ by (simp add: bdd_f cInf_lower)
+ then show ?thesis
+ using assms \<open>L \<le> Inf (range f)\<close> by (auto simp: divide_simps)
+ qed
+ ultimately show *: "(SUP x. 1 / f x) \<le> 1 / Inf (range f)"
+ by (auto simp: cSup_le_iff cINF_lower)
+ have "1 / (SUP x. 1 / f x) \<le> f y" for y
+ proof (cases "(SUP x. 1 / f x) < 0")
+ case True
+ with assms show ?thesis
+ by (meson less_asym' order_trans linorder_not_le zero_le_divide_1_iff)
+ next
+ case False
+ have "1 / f y \<le> (SUP x. 1 / f x)"
+ by (simp add: bdd_invf cSup_upper)
+ with False assms show ?thesis
+ by (metis (no_types) div_by_1 divide_divide_eq_right dual_order.strict_trans1 inverse_eq_divide
+ inverse_le_imp_le mult.left_neutral)
+ qed
+ then have "1 / (SUP x. 1 / f x) \<le> Inf (range f)"
+ using bdd_f by (simp add: le_cInf_iff)
+ moreover have "(SUP x. 1 / f x) > 0"
+ using assms cSUP_upper [OF _ bdd_invf] by (meson UNIV_I less_le_trans zero_less_divide_1_iff)
+ ultimately show "1 / Inf (range f) \<le> (SUP t. 1 / f t)"
+ using \<open>L \<le> Inf (range f)\<close> \<open>L>0\<close> by (auto simp: field_simps)
+qed
+
+lemma Inf_inverse_eq_inverse_Sup:
+ fixes f::"'b \<Rightarrow> 'a::{conditionally_complete_linorder,linordered_field}"
+ assumes "bdd_above (range f)" "L > 0" and geL: "\<And>x. f x \<ge> L"
+ shows "(INF x. 1 / f x) = 1 / (SUP x. f x)"
+proof -
+ obtain M where "M>0" and M: "\<And>x. f x \<le> M"
+ by (meson assms cSup_upper dual_order.strict_trans1 rangeI)
+ have bdd: "bdd_above (range (inverse \<circ> f))"
+ using assms le_imp_inverse_le by (auto simp: bdd_above_def)
+ have "f x > 0" for x
+ using \<open>L>0\<close> geL order_less_le_trans by blast
+ then have [simp]: "1 / inverse(f x) = f x" "1 / M \<le> 1 / f x" for x
+ using M \<open>M>0\<close> by (auto simp: divide_simps)
+ show ?thesis
+ using Sup_inverse_eq_inverse_Inf [OF bdd, of "inverse M"] \<open>M>0\<close>
+ by (simp add: inverse_eq_divide)
+qed
+
lemma Inf_insert_finite:
fixes S :: "'a::conditionally_complete_linorder set"
shows "finite S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
--- a/src/HOL/Int.thy Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Int.thy Fri Sep 29 11:19:43 2023 +0200
@@ -1738,6 +1738,12 @@
lemma power_int_numeral [simp]: "power_int x (numeral n) = x ^ numeral n"
by (simp add: power_int_def)
+lemma powi_numeral_reduce: "x powi numeral n = x * x powi int (pred_numeral n)"
+ by (simp add: numeral_eq_Suc)
+
+lemma powi_minus_numeral_reduce: "x powi - (numeral n) = inverse x * x powi - int(pred_numeral n)"
+ by (simp add: numeral_eq_Suc power_int_def)
+
lemma int_cases4 [case_names nonneg neg]:
fixes m :: int
obtains n where "m = int n" | n where "n > 0" "m = -int n"
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Sep 29 11:19:43 2023 +0200
@@ -514,8 +514,9 @@
|| $$ "(" |-- parse_hol_typed_var --| $$ ")") x
fun parse_simple_hol_term x =
- (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term
- >> (fn ((q, ys), t) =>
+ (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":")
+ -- parse_simple_hol_term
+ >> (fn ((q, ys), t) =>
fold_rev
(fn (var, ty) => fn r =>
AAbs (((var, the_default dummy_atype ty), r), [])
@@ -524,11 +525,12 @@
else
I))
ys t)
- || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not)
+ || Scan.this_string tptp_not |-- parse_simple_hol_term >> mk_app (mk_simple_aterm tptp_not)
|| scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
>> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
|| parse_hol_quantifier >> mk_simple_aterm
|| $$ "(" |-- parse_hol_term --| $$ ")"
+ || Scan.this_string tptp_not >> mk_simple_aterm
|| parse_literal_binary_op >> mk_simple_aterm
|| parse_nonliteral_binary_op >> mk_simple_aterm) x
and parse_applied_hol_term x =
@@ -541,7 +543,14 @@
and parse_hol_term x =
(parse_literal_hol_term -- Scan.repeat (parse_nonliteral_binary_op -- parse_literal_hol_term)
>> (fn (t1, c_ti_s) =>
- fold (fn (c, ti) => fn left => mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x
+ let
+ val cs = map fst c_ti_s
+ val tis = t1 :: map snd c_ti_s
+ val (tis_but_k, tk) = split_last tis
+ in
+ fold_rev (fn (ti, c) => fn right => mk_apps (mk_simple_aterm c) [ti, right])
+ (tis_but_k ~~ cs) tk
+ end)) x
fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x
@@ -624,7 +633,7 @@
val parse_spass_annotations =
Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
-(* We ignore the stars and the pluses that follow literals. *)
+(* We ignore the stars and the pluses that follow literals in SPASS's output. *)
fun parse_decorated_atom x =
(parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Sep 29 11:19:43 2023 +0200
@@ -107,6 +107,8 @@
fun lambda' v = Term.lambda_name (term_name' v, v)
+fun If_const T = Const (\<^const_name>\<open>If\<close>, HOLogic.boolT --> T --> T --> T)
+
fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t
fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t
@@ -240,6 +242,8 @@
val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
+val zip_internal_ite_prefix = "zip_internal_ite_"
+
fun var_index_of_textual textual = if textual then 0 else 1
fun quantify_over_var textual quant_of var_s var_T t =
@@ -253,10 +257,12 @@
| norm_var_types t = t
in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
-(* This assumes that distinct names are mapped to distinct names by "Variable.variant_frees". This
- does not hold in general but should hold for ATP-generated Skolem function names, since these end
- with a digit and "variant_frees" appends letters. *)
-fun fresh_up ctxt s = fst (hd (Variable.variant_frees ctxt [] [(s, ())]))
+(* This assumes that distinct names are mapped to distinct names by
+ "Variable.variant_frees". This does not hold in general but should hold for
+ ATP-generated Skolem function names, since these end with a digit and
+ "variant_frees" appends letters. *)
+fun desymbolize_and_fresh_up ctxt s =
+ fst (hd (Variable.variant_frees ctxt [] [(Name.desymbolize (SOME false) s, ())]))
(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
are typed. The code is similar to "term_of_atp_fo". *)
@@ -267,12 +273,16 @@
fun do_term opt_T u =
(case u of
- AAbs (((var, ty), term), []) =>
+ AAbs (((var, ty), term), us) =>
let
val typ = typ_of_atp_type ctxt ty
val var_name = repair_var_name var
val tm = do_term NONE term
- in quantify_over_var true lambda' var_name typ tm end
+ val lam = quantify_over_var true lambda' var_name typ tm
+ val args = map (do_term NONE) us
+ in
+ list_comb (lam, args)
+ end
| ATerm ((s, tys), us) =>
if s = "" (* special marker generated on parse error *) then
error "Isar proof reconstruction failed because the ATP proof contains unparsable \
@@ -302,6 +312,7 @@
else if s = tptp_ho_exists then HOLogic.exists_const dummyT
else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT
else if s = tptp_hilbert_the then \<^term>\<open>The\<close>
+ else if String.isPrefix zip_internal_ite_prefix s then If_const dummyT
else
(case unprefix_and_unascii const_prefix s of
SOME s' =>
@@ -337,7 +348,7 @@
(case unprefix_and_unascii fixed_var_prefix s of
SOME s => Free (s, T)
| NONE =>
- if not (is_tptp_variable s) then Free (fresh_up ctxt s, T)
+ if not (is_tptp_variable s) then Free (desymbolize_and_fresh_up ctxt s, T)
else Var ((repair_var_name s, var_index), T))
in list_comb (t, ts) end))
in do_term end
@@ -428,7 +439,7 @@
SOME s => Free (s, T)
| NONE =>
if textual andalso not (is_tptp_variable s) then
- Free (s |> textual ? fresh_up ctxt, T)
+ Free (desymbolize_and_fresh_up ctxt s, T)
else
Var ((repair_var_name s, var_index), T))
in list_comb (t, ts) end))
@@ -768,6 +779,17 @@
input_steps @ sko_steps @ map repair_deps other_steps
end
+val zf_stmt_prefix = "zf_stmt_"
+
+fun is_if_True_or_False_axiom true_or_false t =
+ (case t of
+ @{const Trueprop} $
+ (Const (@{const_name HOL.eq}, _) $
+ (Const (@{const_name If}, _) $ cond $ Var _ $ Var _) $
+ Var _) =>
+ cond aconv true_or_false
+ | _ => false)
+
fun factify_atp_proof facts hyp_ts concl_t atp_proof =
let
fun factify_step ((num, ss), role, t, rule, deps) =
@@ -779,7 +801,18 @@
else ([], Hypothesis, close_form (nth hyp_ts j))
| _ =>
(case resolve_facts facts (num :: ss) of
- [] => (ss, if member (op =) [Definition, Lemma] role then role else Plain, t)
+ [] =>
+ if role = Axiom andalso String.isPrefix zf_stmt_prefix num
+ andalso is_if_True_or_False_axiom @{const True} t then
+ (["if_True"], Axiom, t)
+ else if role = Axiom andalso String.isPrefix zf_stmt_prefix num
+ andalso is_if_True_or_False_axiom @{const False} t then
+ (["if_False"], Axiom, t)
+ else
+ (ss,
+ if role = Definition then Definition
+ else if role = Lemma then Lemma
+ else Plain, t)
| facts => (map fst facts, Axiom, t)))
in
((num, ss'), role', t', rule, deps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 29 11:19:43 2023 +0200
@@ -134,9 +134,12 @@
bool * (string option * string option) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
-val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
-val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
+val basic_systematic_methods =
+ [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method, Argo_Method]
+val basic_simp_based_methods =
+ [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
+val basic_arith_methods =
+ [Linarith_Method, Presburger_Method, Algebra_Method]
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
val systematic_methods =
@@ -258,6 +261,8 @@
and is_referenced_in_proof l (Proof {steps, ...}) =
exists (is_referenced_in_step l) steps
+ (* We try to introduce pure lemmas (not "obtains") close to where
+ they are used. *)
fun insert_lemma_in_step lem
(step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
proof_methods, comment}) =
@@ -283,7 +288,8 @@
end
and insert_lemma_in_steps lem [] = [lem]
| insert_lemma_in_steps lem (step :: steps) =
- if is_referenced_in_step (the (label_of_isar_step lem)) step then
+ if not (null (obtains_of_isar_step lem))
+ orelse is_referenced_in_step (the (label_of_isar_step lem)) step then
insert_lemma_in_step lem step @ steps
else
step :: insert_lemma_in_steps lem steps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Sep 29 11:19:43 2023 +0200
@@ -46,6 +46,7 @@
val steps_of_isar_proof : isar_proof -> isar_step list
val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof
+ val obtains_of_isar_step : isar_step -> (string * typ) list
val label_of_isar_step : isar_step -> label option
val facts_of_isar_step : isar_step -> facts
val proof_methods_of_isar_step : isar_step -> proof_method list
@@ -130,6 +131,9 @@
fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps =
Proof {fixes = fixes, assumptions = assumptions, steps = steps}
+fun obtains_of_isar_step (Prove {obtains, ...}) = obtains
+ | obtains_of_isar_step _ = []
+
fun label_of_isar_step (Prove {label, ...}) = SOME label
| label_of_isar_step _ = NONE
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Sep 29 11:19:43 2023 +0200
@@ -18,6 +18,7 @@
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
+ Argo_Method |
Blast_Method |
Simp_Method |
Auto_Method |
@@ -60,6 +61,7 @@
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
+ Argo_Method |
Blast_Method |
Simp_Method |
Auto_Method |
@@ -101,6 +103,7 @@
| SMT_Method (SMT_Verit strategy) =>
"smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
| SATx_Method => "satx"
+ | Argo_Method => "argo"
| Blast_Method => "blast"
| Simp_Method => if null ss then "simp" else "simp add:"
| Auto_Method => "auto"
@@ -141,6 +144,7 @@
Method.insert_tac ctxt global_facts THEN'
(case meth of
SATx_Method => SAT.satx_tac ctxt
+ | Argo_Method => Argo_Tactic.argo_tac ctxt []
| Blast_Method => blast_tac ctxt
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
| Fastforce_Method => Clasimp.fast_force_tac ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Sep 29 11:19:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Sep 29 11:19:43 2023 +0200
@@ -217,7 +217,8 @@
let
val misc_methodss =
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
- Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
+ Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
+ Argo_Method]]
val metis_methodss =
[Metis_Method (SOME full_typesN, NONE) ::