# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1505835439 -3600
# Node ID bc3584f7ac0c2e590376998eddb496214f860614
# Parent  d5bf4bdb4fb7231368e589e631dbc36c14fcee00
Using the "constant_on" operator

diff -r d5bf4bdb4fb7 -r bc3584f7ac0c src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Sep 17 21:04:02 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Sep 19 16:37:19 2017 +0100
@@ -739,7 +739,7 @@
 lemma holomorphic_factor_zero_nonconstant:
   assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
       and "\<xi> \<in> S" "f \<xi> = 0"
-      and nonconst: "\<And>c. \<exists>z \<in> S. f z \<noteq> c"
+      and nonconst: "~ f constant_on S"
    obtains g r n
       where "0 < n"  "0 < r"  "ball \<xi> r \<subseteq> S"
             "g holomorphic_on ball \<xi> r"
@@ -747,7 +747,7 @@
             "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
 proof (cases "\<forall>n>0. (deriv ^^ n) f \<xi> = 0")
   case True then show ?thesis
-    using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by auto
+    using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by (simp add: constant_on_def)
 next
   case False
   then obtain n0 where "n0 > 0" and n0: "(deriv ^^ n0) f \<xi> \<noteq> 0" by blast
@@ -3074,18 +3074,19 @@
 
 lemma holomorphic_factor_zero_Ex1:
   assumes "open s" "connected s" "z \<in> s" and
-        holo:"f holomorphic_on s"
-        and "f z = 0" and "\<exists>w\<in>s. f w \<noteq> 0"
+        holf: "f holomorphic_on s"
+        and f: "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0"
   shows "\<exists>!n. \<exists>g r. 0 < n \<and> 0 < r \<and>
                 g holomorphic_on cball z r
                 \<and> (\<forall>w\<in>cball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0)"
 proof (rule ex_ex1I)
-  obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and
+  have "\<not> f constant_on s"
+    by (metis \<open>z\<in>s\<close> constant_on_def f)
+  then obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and
           g:"g holomorphic_on ball z r"
           "\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w"
           "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
-    using holomorphic_factor_zero_nonconstant[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
-    by (metis assms(3) assms(5) assms(6))
+    by (blast intro: holomorphic_factor_zero_nonconstant[OF holf \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>])
   define r' where "r' \<equiv> r/2"
   have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
   hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'"
diff -r d5bf4bdb4fb7 -r bc3584f7ac0c src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Sun Sep 17 21:04:02 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy	Tue Sep 19 16:37:19 2017 +0100
@@ -1000,7 +1000,7 @@
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
       and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
-      and nonconst: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
+      and nonconst: "~ g constant_on S"
       and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
       and "z0 \<in> S"
       shows "g z0 \<noteq> 0"
@@ -1164,14 +1164,14 @@
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
       and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
-      and nonconst: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
+      and nonconst: "~ g constant_on S"
       and inj: "\<And>n. inj_on (\<F> n) S"
     shows "inj_on g S"
 proof -
   have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2
   proof -
     obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2"
-      using nonconst by blast
+      using constant_on_def nonconst by blast
     have "(\<lambda>z. g z - g z1) holomorphic_on S"
       by (intro holomorphic_intros holg)
     then obtain r where "0 < r" "ball z2 r \<subseteq> S" "\<And>z. dist z2 z < r \<and> z \<noteq> z2 \<Longrightarrow> g z \<noteq> g z1"
@@ -1214,7 +1214,8 @@
         show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
           by simp
       qed
-      show "\<And>c. \<exists>z\<in>S - {z1}. g z - g z1 \<noteq> c"
+      show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}"
+        unfolding constant_on_def
         by (metis Diff_iff \<open>z0 \<in> S\<close> empty_iff insert_iff right_minus_eq z0 z12)
       show "\<And>n z. z \<in> S - {z1} \<Longrightarrow> \<F> n z - \<F> n z1 \<noteq> 0"
         by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 \<open>z1 \<in> S\<close>)
@@ -1360,8 +1361,9 @@
           using \<open>Z \<subseteq> S\<close> e hol\<G> by force
         show "\<And>n z. z \<in> ball v e \<Longrightarrow> (\<G> \<circ> j) n z \<noteq> 0"
           using \<G>not0 \<open>Z \<subseteq> S\<close> e by fastforce
-        show "\<exists>z\<in>ball v e. h z \<noteq> c" for c
-        proof -
+        show "\<not> h constant_on ball v e"
+        proof (clarsimp simp: constant_on_def)
+          fix c
           have False if "\<And>z. dist v z < e \<Longrightarrow> h z = c"  
           proof -
             have "h v = c"
@@ -1389,7 +1391,7 @@
             show False
               using \<open>C < cmod (\<F> (j n) y)\<close> le_C not_less by blast
           qed
-          then show ?thesis by force
+          then show "\<exists>x\<in>ball v e. h x \<noteq> c" by force
         qed
         show "h holomorphic_on ball v e"
           by (simp add: holh)
@@ -1828,7 +1830,6 @@
     by meson
 qed
 
-
 corollary Casorati_Weierstrass:
   assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})"
       and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"