# HG changeset patch # User wenzelm # Date 1695979183 -7200 # Node ID a9ac75d397df6708d9d17c3b7e02b8aae16cd8d2 # Parent 4de5b127c124e236fe3c25366ca48c276aee0118# Parent fc0814e9f7a8cce559891f5ba78d0dba0560b581 merged diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Analysis/Derivative.thy --- 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 (\w. f (c*w + a)) z = c * deriv f (c*z + a)" + apply (subst deriv_chain [where f="\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 (\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 \ :> df" and S: "open S" "\ \ S" and "df \ 0" shows "\ f constant_on S" diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Analysis/Path_Connected.thy --- 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 \ path_image c - {pathstart c,pathfinish c} \ {}" 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 \ f)" + unfolding simple_path_def +proof + show "path (g \ f)" + using assms unfolding simple_path_def by (intro path_continuous_image) auto + from assms have [simp]: "g (f x) = g (f y) \ f x = f y" if "x \ {0..1}" "y \ {0..1}" for x y + unfolding inj_on_def path_image_def using that by fastforce + show "loop_free (g \ f)" + using assms(1) by (auto simp: loop_free_def simple_path_def) +qed subsection\<^marker>\tag unimportant\\The operations on paths\ diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Analysis/Uniform_Limit.thy --- 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: "\\<^sub>F n in F. g n ` X \ U" and l: "l ` X \ U" + shows "uniform_limit X (\a b. f (g a b)) (f \ l) F" +proof (rule uniform_limitI) + fix \::real + assume "0 < \" + then obtain \ where "\ > 0" and \: "\u v. \u\U; v\U; dist u v < \\ \ dist (f u) (f v) < \" + by (metis cont uniformly_continuous_on_def) + show "\\<^sub>F n in F. \x\X. dist (f (g n x)) ((f \ l) x) < \" + using uniform_limitD [OF ul \\>0\] g unfolding o_def + by eventually_elim (use \ l in blast) +qed + lemma metric_uniform_limit_imp_uniform_limit: assumes f: "uniform_limit S f a F" assumes le: "eventually (\x. \y\S. dist (g x y) (b y) \ 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 "\\<^sub>F x in F. \y\S. dist (g x y) (b y) < e" by eventually_elim force diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Complex.thy --- 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) = (\x\s. Im(f x))" by (induct s rule: infinite_finite_induct) auto +lemma Rats_complex_of_real_iff [iff]: "complex_of_real x \ \ \ x \ \" +proof - + have "\a b. \0 < b; x = complex_of_int a / complex_of_int b\ \ x \ \" + 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: "(\i\I. Re (z i)) \ cmod (\i\I. z i)" by (metis Re_sum complex_Re_le_cmod) diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy --- 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]: - "\f holomorphic_on S; open S\ \ (deriv f) holomorphic_on S" -by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def) + "\f holomorphic_on S; open S\ \ (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 \ B" "open B" + shows "(\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 \ (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 \ S" - and fg: "\w. w \ S \ u * w \ T" - shows "(deriv ^^ n) (\w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)" + and fg: "\w. w \ S \ u*w + c \ T" + shows "(deriv ^^ n) (\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 (\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 (\w. u * w+c) ` S" by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T) - have holo3: "(\z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S" + have holo3: "(\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 "(\w. u * w+c) holomorphic_on S" "f holomorphic_on (\w. u * w+c) ` S" by (rule holo0 holomorphic_intros)+ - then have holo1: "(\w. f (u * w)) holomorphic_on S" + then have holo1: "(\w. f (u * w+c)) holomorphic_on S" by (rule holomorphic_on_compose [where g=f, unfolded o_def]) - have "deriv ((deriv ^^ n) (\w. f (u * w))) z = deriv (\z. u^n * (deriv ^^ n) f (u*z)) z" + have "deriv ((deriv ^^ n) (\w. f (u * w+c))) z = deriv (\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) (\w. f (u * w)) holomorphic_on S" + show "(deriv ^^ n) (\w. f (u * w+c)) holomorphic_on S" by (rule holomorphic_higher_deriv [OF holo1 S]) qed (simp add: Suc.IH) - also have "\ = u^n * deriv (\z. (deriv ^^ n) f (u * z)) z" + also have "\ = u^n * deriv (\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 "(\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 "(\w. (deriv ^^ n) f (u * w+c)) analytic_on S" + proof - + have "(deriv ^^ n) f \ (\w. u * w+c) holomorphic_on S" + using holomorphic_on_compose[OF _ holo2] \(\w. u * w+c) holomorphic_on S\ + 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 "\ = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)" + also have "\ = 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 \ S" + and fg: "\w. w \ S \ u * w \ T" + shows "(deriv ^^ n) (\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) (\w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z" diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy --- 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 \ S \ continuous_on S (\w. 1 / (w - z))" by (rule continuous_intros | force)+ diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Complex_Analysis/Laurent_Convergence.thy --- 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 \TODO: Better than @{thm deriv_compose_linear}?\ -lemma deriv_compose_linear': - assumes "f field_differentiable at (c*z + a)" - shows "deriv (\w. f (c*w + a)) z = c * deriv f (c*z + a)" - apply (subst deriv_chain[where f="\w. c*w + a",unfolded comp_def]) - using assms by (auto intro:derivative_intros) - -text \TODO: Better than @{thm 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 \ S" - and fg: "\w. w \ S \ u*w + c \ T" - shows "(deriv ^^ n) (\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 (\w. u * w+c) ` S" - by (meson fg f holomorphic_on_subset image_subset_iff) - have holo2: "(deriv ^^ n) f holomorphic_on (\w. u * w+c) ` S" - by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T) - have holo3: "(\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 "(\w. u * w+c) holomorphic_on S" "f holomorphic_on (\w. u * w+c) ` S" - by (rule holo0 holomorphic_intros)+ - then have holo1: "(\w. f (u * w+c)) holomorphic_on S" - by (rule holomorphic_on_compose [where g=f, unfolded o_def]) - have "deriv ((deriv ^^ n) (\w. f (u * w+c))) z = deriv (\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) (\w. f (u * w+c)) holomorphic_on S" - by (rule holomorphic_higher_deriv [OF holo1 S]) - qed (simp add: Suc.IH) - also have "\ = u^n * deriv (\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 "(\w. (deriv ^^ n) f (u * w+c)) analytic_on S" - proof - - have "(deriv ^^ n) f \ (\w. u * w+c) holomorphic_on S" - using holomorphic_on_compose[OF _ holo2] \(\w. u * w+c) holomorphic_on S\ - 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 "\ = 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) diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Complex_Analysis/Meromorphic.thy --- 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 (\x. f x = g x) (nhds x)" "x = y" - shows "f analytic_on {x} \ g analytic_on {y}" -proof - - have "g analytic_on {x}" if "f analytic_on {x}" "eventually (\x. f x = g x) (nhds x)" for f g - proof - - have "(\y. f (x + y)) has_fps_expansion fps_expansion f x" - by (rule analytic_at_imp_has_fps_expansion) fact - also have "?this \ (\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 \ complex) \ complex \ complex" where "remove_sings f z = (if \c. f \z\ c then Lim (at z) f else 0)" @@ -2330,4 +2313,4 @@ finally show ?thesis . qed -end \ No newline at end of file +end diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Conditionally_Complete_Lattices.thy --- 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 \ Inf {y<.. 'a::{conditionally_complete_linorder,linordered_field}" + assumes "bdd_above (range f)" "L > 0" and geL: "\x. f x \ 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) \ L" + by (simp add: cINF_greatest geL) + have bdd_invf: "bdd_above (range (\x. 1 / f x))" + proof (rule bdd_aboveI2) + show "\x. 1 / f x \ 1/L" + using assms by (auto simp: divide_simps) + qed + moreover have le_inverse_Inf: "1 / f x \ 1 / Inf (range f)" for x + proof - + have "Inf (range f) \ f x" + by (simp add: bdd_f cInf_lower) + then show ?thesis + using assms \L \ Inf (range f)\ by (auto simp: divide_simps) + qed + ultimately show *: "(SUP x. 1 / f x) \ 1 / Inf (range f)" + by (auto simp: cSup_le_iff cINF_lower) + have "1 / (SUP x. 1 / f x) \ 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 \ (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) \ 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) \ (SUP t. 1 / f t)" + using \L \ Inf (range f)\ \L>0\ by (auto simp: field_simps) +qed + +lemma Inf_inverse_eq_inverse_Sup: + fixes f::"'b \ 'a::{conditionally_complete_linorder,linordered_field}" + assumes "bdd_above (range f)" "L > 0" and geL: "\x. f x \ L" + shows "(INF x. 1 / f x) = 1 / (SUP x. f x)" +proof - + obtain M where "M>0" and M: "\x. f x \ M" + by (meson assms cSup_upper dual_order.strict_trans1 rangeI) + have bdd: "bdd_above (range (inverse \ f))" + using assms le_imp_inverse_le by (auto simp: bdd_above_def) + have "f x > 0" for x + using \L>0\ geL order_less_le_trans by blast + then have [simp]: "1 / inverse(f x) = f x" "1 / M \ 1 / f x" for x + using M \M>0\ by (auto simp: divide_simps) + show ?thesis + using Sup_inverse_eq_inverse_Inf [OF bdd, of "inverse M"] \M>0\ + by (simp add: inverse_eq_divide) +qed + lemma Inf_insert_finite: fixes S :: "'a::conditionally_complete_linorder set" shows "finite S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))" diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Int.thy --- 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" diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Tools/ATP/atp_proof.ML --- 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 diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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>\If\, 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>\The\ + 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) diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r fc0814e9f7a8 -r a9ac75d397df src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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) ::