# HG changeset patch
# User wenzelm
# Date 1626467576 -7200
# Node ID c4c612d92fcc924c0a6c9211e0032b0a8eb48d8f
# Parent  4cca14dc577c16c51252c01e85ea7f6799230b56# Parent  d609fa3e816d5fa6b727bfcf1dba0cbc2701f200
merged

diff -r d609fa3e816d -r c4c612d92fcc src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Jul 16 22:32:56 2021 +0200
@@ -803,9 +803,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers.
-
 \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
 used to prove universally quantified equations using unconditional equations,
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -137,6 +137,24 @@
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic lemmas about paths\<close>
 
+lemma path_of_real: "path complex_of_real" 
+  unfolding path_def by (intro continuous_intros)
+
+lemma path_const: "path (\<lambda>t. a)" for a::"'a::real_normed_vector"
+  unfolding path_def by (intro continuous_intros)
+
+lemma path_minus: "path g \<Longrightarrow> path (\<lambda>t. - g t)" for g::"real\<Rightarrow>'a::real_normed_vector"
+  unfolding path_def by (intro continuous_intros)
+
+lemma path_add: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t + g t)" for f::"real\<Rightarrow>'a::real_normed_vector"
+  unfolding path_def by (intro continuous_intros)
+
+lemma path_diff: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t - g t)" for f::"real\<Rightarrow>'a::real_normed_vector"
+  unfolding path_def by (intro continuous_intros)
+
+lemma path_mult: "\<lbrakk>path f; path g\<rbrakk> \<Longrightarrow> path (\<lambda>t. f t * g t)" for f::"real\<Rightarrow>'a::real_normed_field"
+  unfolding path_def by (intro continuous_intros)
+
 lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g"
   by (simp add: pathin_def path_def)
 
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -1493,16 +1493,7 @@
     and "affine T"
     and "rel_interior S \<inter> T \<noteq> {}"
   shows "closure (S \<inter> T) = closure S \<inter> T"
-proof -
-  have "affine hull T = T"
-    using assms by auto
-  then have "rel_interior T = T"
-    using rel_interior_affine_hull[of T] by metis
-  moreover have "closure T = T"
-    using assms affine_closed[of T] by auto
-  ultimately show ?thesis
-    using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
-qed
+  by (metis affine_imp_convex assms convex_closure_inter_two rel_interior_affine rel_interior_eq_closure)
 
 lemma connected_component_1_gen:
   fixes S :: "'a :: euclidean_space set"
@@ -1523,16 +1514,7 @@
     and "affine T"
     and "rel_interior S \<inter> T \<noteq> {}"
   shows "rel_interior (S \<inter> T) = rel_interior S \<inter> T"
-proof -
-  have "affine hull T = T"
-    using assms by auto
-  then have "rel_interior T = T"
-    using rel_interior_affine_hull[of T] by metis
-  moreover have "closure T = T"
-    using assms affine_closed[of T] by auto
-  ultimately show ?thesis
-    using convex_rel_interior_inter_two[of S T] assms affine_imp_convex by auto
-qed
+  by (simp add: affine_imp_convex assms convex_rel_interior_inter_two rel_interior_affine)
 
 lemma convex_affine_rel_frontier_Int:
    fixes S T :: "'n::euclidean_space set"
@@ -1547,49 +1529,8 @@
 lemma rel_interior_convex_Int_affine:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
-    shows "rel_interior(S \<inter> T) = interior S \<inter> T"
-proof -
-  obtain a where aS: "a \<in> interior S" and aT:"a \<in> T"
-    using assms by force
-  have "rel_interior S = interior S"
-    by (metis (no_types) aS affine_hull_nonempty_interior equals0D rel_interior_interior)
-  then show ?thesis
-    by (metis (no_types) affine_imp_convex assms convex_rel_interior_inter_two hull_same rel_interior_affine_hull)
-qed
-
-lemma closure_convex_Int_affine:
-  fixes S :: "'a::euclidean_space set"
-  assumes "convex S" "affine T" "rel_interior S \<inter> T \<noteq> {}"
-  shows "closure(S \<inter> T) = closure S \<inter> T"
-proof
-  have "closure (S \<inter> T) \<subseteq> closure T"
-    by (simp add: closure_mono)
-  also have "... \<subseteq> T"
-    by (simp add: affine_closed assms)
-  finally show "closure(S \<inter> T) \<subseteq> closure S \<inter> T"
-    by (simp add: closure_mono)
-next
-  obtain a where "a \<in> rel_interior S" "a \<in> T"
-    using assms by auto
-  then have ssT: "subspace ((\<lambda>x. (-a)+x) ` T)" and "a \<in> S"
-    using affine_diffs_subspace rel_interior_subset assms by blast+
-  show "closure S \<inter> T \<subseteq> closure (S \<inter> T)"
-  proof
-    fix x  assume "x \<in> closure S \<inter> T"
-    show "x \<in> closure (S \<inter> T)"
-    proof (cases "x = a")
-      case True
-      then show ?thesis
-        using \<open>a \<in> S\<close> \<open>a \<in> T\<close> closure_subset by fastforce
-    next
-      case False
-      then have "x \<in> closure(open_segment a x)"
-        by auto
-      then show ?thesis
-        using \<open>x \<in> closure S \<inter> T\<close> assms convex_affine_closure_Int by blast
-    qed
-  qed
-qed
+  shows "rel_interior(S \<inter> T) = interior S \<inter> T"
+  by (metis Int_emptyI assms convex_affine_rel_interior_Int empty_iff interior_rel_interior_gen)
 
 lemma subset_rel_interior_convex:
   fixes S T :: "'n::euclidean_space set"
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Complex_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -82,6 +82,38 @@
   thus ?thesis by simp
 qed
 
+corollary analytic_continuation':
+  assumes "f holomorphic_on S" "open S" "connected S"
+      and "U \<subseteq> S" "\<xi> \<in> S" "\<xi> islimpt U"
+      and "f constant_on U"
+    shows "f constant_on S"
+proof -
+  obtain c where c: "\<And>x. x \<in> U \<Longrightarrow> f x - c = 0"
+    by (metis \<open>f constant_on U\<close> constant_on_def diff_self)
+  have "(\<lambda>z. f z - c) holomorphic_on S"
+    using assms by (intro holomorphic_intros)
+  with c analytic_continuation assms have "\<And>x. x \<in> S \<Longrightarrow> f x - c = 0"
+    by blast
+  then show ?thesis
+    unfolding constant_on_def by force
+qed
+
+lemma holomorphic_compact_finite_zeros:
+  assumes S: "f holomorphic_on S" "open S" "connected S"
+      and "compact K" "K \<subseteq> S"
+      and "\<not> f constant_on S"
+    shows "finite {z\<in>K. f z = 0}"
+proof (rule ccontr)
+  assume "infinite {z\<in>K. f z = 0}"
+  then obtain z where "z \<in> K" and z: "z islimpt {z\<in>K. f z = 0}"
+    using \<open>compact K\<close> by (auto simp: compact_eq_Bolzano_Weierstrass)
+  moreover have "{z\<in>K. f z = 0} \<subseteq> S"
+    using \<open>K \<subseteq> S\<close> by blast
+    ultimately show False
+    using assms analytic_continuation [OF S] unfolding constant_on_def
+    by blast
+qed
+
 subsection\<open>Open mapping theorem\<close>
 
 lemma holomorphic_contract_to_zero:
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -427,6 +427,25 @@
   "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<le> Sup A"
   by (auto intro!: cSup_upper2[of "SOME a. a \<in> A"] intro: someI cInf_lower)
 
+  context
+    fixes f :: "'a \<Rightarrow> 'b::conditionally_complete_lattice"
+    assumes "mono f"
+  begin
+  
+  lemma mono_cInf: "\<lbrakk>bdd_below A; A\<noteq>{}\<rbrakk> \<Longrightarrow> f (Inf A) \<le> (INF x\<in>A. f x)"
+    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cINF_greatest cInf_lower monoD)
+  
+  lemma mono_cSup: "\<lbrakk>bdd_above A; A\<noteq>{}\<rbrakk> \<Longrightarrow> (SUP x\<in>A. f x) \<le> f (Sup A)"
+    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cSUP_least cSup_upper monoD)
+  
+  lemma mono_cINF: "\<lbrakk>bdd_below (A`I); I\<noteq>{}\<rbrakk> \<Longrightarrow> f (INF i\<in>I. A i) \<le> (INF x\<in>I. f (A x))"
+    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cINF_greatest cINF_lower monoD)
+  
+  lemma mono_cSUP: "\<lbrakk>bdd_above (A`I); I\<noteq>{}\<rbrakk> \<Longrightarrow> (SUP x\<in>I. f (A x)) \<le> f (SUP i\<in>I. A i)"
+    by (simp add: \<open>mono f\<close> conditionally_complete_lattice_class.cSUP_least cSUP_upper monoD)
+  
+  end
+
 end
 
 instance complete_lattice \<subseteq> conditionally_complete_lattice
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Deriv.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -959,6 +959,12 @@
   shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F"
   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])
 
+lemma has_vector_derivative_divide[derivative_intros]:
+  fixes a :: "'a::real_normed_field"
+  shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative (x / a)) F"
+  using has_vector_derivative_mult_left [of f x F "inverse a"]
+  by (simp add: field_class.field_divide_inverse)
+
 
 subsection \<open>Derivatives\<close>
 
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Groups.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -639,6 +639,11 @@
 
 end
 
+lemma mono_add:
+  fixes a :: "'a::ordered_ab_semigroup_add" 
+  shows "mono ((+) a)"
+  by (simp add: add_left_mono monoI)
+
 text \<open>Strict monotonicity in both arguments\<close>
 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -764,6 +764,9 @@
   finally show ?thesis by simp
 qed
 
+lemma bdd_below_norm_image: "bdd_below (norm ` A)"
+  by (meson bdd_belowI2 norm_ge_zero)
+
 end
 
 class real_normed_algebra = real_algebra + real_normed_vector +
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Rings.thy	Fri Jul 16 22:32:56 2021 +0200
@@ -1884,6 +1884,11 @@
 
 end
 
+lemma mono_mult:
+  fixes a :: "'a::ordered_semiring" 
+  shows "a \<ge> 0 \<Longrightarrow> mono ((*) a)"
+  by (simp add: mono_def mult_left_mono)
+
 class ordered_semiring_0 = semiring_0 + ordered_semiring
 begin
 
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 16 22:32:56 2021 +0200
@@ -47,7 +47,6 @@
   val iproverN : string
   val leo2N : string
   val leo3N : string
-  val pirateN : string
   val satallaxN : string
   val spassN : string
   val vampireN : string
@@ -110,7 +109,6 @@
 val iproverN = "iprover"
 val leo2N = "leo2"
 val leo3N = "leo3"
-val pirateN = "pirate"
 val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
@@ -638,32 +636,6 @@
    >> (fn ((((num, rule), deps), u), names) =>
           [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
 
-fun parse_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
-fun parse_pirate_dependencies x =
-  Scan.repeat (parse_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
-fun parse_pirate_file_source x =
-  ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
-     --| $$ ")") x
-fun parse_pirate_inference_source x =
-  (scan_general_id -- ($$ "(" |-- parse_pirate_dependencies --| $$ ")")) x
-fun parse_pirate_source x =
-  (parse_pirate_file_source >> (fn s => File_Source ("", SOME s))
-   || parse_pirate_inference_source >> Inference_Source) x
-
-(* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *)
-fun parse_pirate_line x =
-  (scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "."
-     --| Scan.this_string "origin" --| $$ "(" -- parse_pirate_source --| $$ ")"
-   >> (fn ((((num, u), source))) =>
-     let
-       val (names, rule, deps) =
-         (case source of
-           File_Source (_, SOME s) => ([s], spass_input_rule, [])
-         | Inference_Source (rule, deps) => ([], rule, deps))
-     in
-       [((num, names), Unknown, u, rule, map (rpair []) deps)]
-     end)) x
-
 fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
 
 (* Syntax: SZS core <name> ... <name> *)
@@ -674,7 +646,6 @@
 fun parse_line local_name problem =
   (* Satallax is handled separately, in "atp_satallax.ML". *)
   if local_name = spassN then parse_spass_line
-  else if local_name = pirateN then parse_pirate_line
   else if local_name = z3_tptpN then parse_z3_tptp_core_line
   else parse_tstp_line problem
 
diff -r d609fa3e816d -r c4c612d92fcc src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jul 16 22:32:41 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jul 16 22:32:56 2021 +0200
@@ -482,9 +482,6 @@
 val vampire_full_proof_options =
   " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
-val remote_vampire_command =
-  "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
-
 val vampire_config : atp_config =
   let
     val format = TFF (Without_FOOL, Monomorphic)
@@ -663,9 +660,6 @@
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
     (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
-val remote_vampire =
-  remotify_atp vampire "Vampire" ["THF-4.4"]
-    (K (((400, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 val remote_zipperposition =
   remotify_atp zipperposition "Zipperpin" ["2.0"]
@@ -728,7 +722,7 @@
 val atps =
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
    remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx]
+   remote_waldmeister, remote_zipperposition, dummy_tfx]
 
 val _ = Theory.setup (fold add_atp atps)