--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 03 23:01:39 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 03 23:03:30 2016 +0200
@@ -2,7 +2,7 @@
Author: Andreas Lochbihler, ETH Zurich
*)
-section {* Formalisation of chain-complete partial orders, continuity and admissibility *}
+section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
Main
@@ -83,10 +83,10 @@
fix x'
assume "x' \<in> (\<lambda>f. f x) ` Y"
then obtain f where "f \<in> Y" "x' = f x" by blast
- note `x' = f x` also
- from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD)
+ note \<open>x' = f x\<close> also
+ from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
qed
qed
@@ -108,9 +108,9 @@
fix x'
assume "x' \<in> f x ` Y"
then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
- also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD)
+ also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
also have "\<dots> \<le> ?rhs" using chain'[OF y]
- by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`)
+ by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
finally show "x' \<le> ?rhs" .
qed(rule x)
@@ -128,17 +128,17 @@
fix x'
assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
- also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`]
+ also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>]
proof(rule ccpo_Sup_least)
fix x
assume "x \<in> f y' ` Y"
then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"
- from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
- hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y`
+ from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
+ hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
- also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def)
- from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`)
+ also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
+ from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>)
finally show "x \<le> ?rhs" by(simp add: x)
qed
finally show "x' \<le> ?rhs" .
@@ -149,9 +149,9 @@
fix y
assume "y \<in> (\<lambda>x. f x x) ` Y"
then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
- also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)"
- by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`)
- also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`)
+ also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
+ by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
+ also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
finally show "y \<le> ?lhs" .
qed
qed
@@ -171,8 +171,8 @@
fix x
assume "x \<in> f ` Y"
then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
- also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper)
- hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono)
+ also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper)
+ hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono)
finally show "x \<le> \<dots>" .
qed
@@ -196,14 +196,14 @@
fix f g
assume "f \<in> Z" "g \<in> Z"
and "fun_ord op \<le> f g"
- from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
+ from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
proof(rule ccpo_Sup_least)
fix x
assume "x \<in> f ` Y"
then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
- also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def)
- also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`]
- by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+ also have "\<dots> \<le> g y" using \<open>fun_ord op \<le> f g\<close> by(simp add: fun_ord_def)
+ also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>]
+ by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
finally show "x \<le> \<Squnion>(g ` Y)" .
qed
qed
@@ -219,9 +219,9 @@
fix x'
assume "x' \<in> (\<lambda>f. f x) ` Z"
then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
- also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono])
+ also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
also have "f y \<le> ?rhs" using chain3
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
finally show "x' \<le> ?rhs" .
qed
qed
@@ -231,14 +231,14 @@
fix x
assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
- also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`]
+ also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>]
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> f ` Y"
then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
- also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
+ also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
finally show "x' \<le> ?rhs" .
qed
finally show "x \<le> ?rhs" .
@@ -254,10 +254,10 @@
fix x'
assume "x' \<in> (\<lambda>f. f y) ` Z"
then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
- also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`]
- by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+ also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
+ by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
also have "\<dots> \<le> ?lhs" using chain2
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
finally show "x' \<le> ?lhs" .
qed
finally show "x \<le> ?lhs" .
@@ -314,9 +314,9 @@
assume "x' \<in> (\<lambda>f. f x) ` ?iter"
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
also have "f x \<le> f y"
- by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+
+ by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
- by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
finally show "x' \<le> \<dots>" .
qed
qed
@@ -333,7 +333,7 @@
shows "monotone orda ordc (\<lambda>x. f x (t x))"
by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
-subsection {* Continuity *}
+subsection \<open>Continuity\<close>
definition cont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where
@@ -345,10 +345,10 @@
"mcont luba orda lubb ordb f \<longleftrightarrow>
monotone orda ordb f \<and> cont luba orda lubb ordb f"
-subsubsection {* Theorem collection @{text cont_intro} *}
+subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
named_theorems cont_intro "continuity and admissibility intro rules"
-ML {*
+ML \<open>
(* apply cont_intro rules as intro and try to solve
the remaining of the emerging subgoals with simp *)
fun cont_intro_tac ctxt =
@@ -374,13 +374,13 @@
end
handle THM _ => NONE
| TYPE _ => NONE
-*}
+\<close>
simproc_setup "cont_intro"
( "ccpo.admissible lub ord P"
| "mcont lub ord lub' ord' f"
| "monotone ord ord' f"
- ) = {* K cont_intro_simproc *}
+ ) = \<open>K cont_intro_simproc\<close>
lemmas [cont_intro] =
call_mono
@@ -604,10 +604,10 @@
fix x'
assume "x' \<in> (\<lambda>f. f x) ` ?iter"
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
- also from _ `x \<sqsubseteq> y` have "f x \<le> f y"
- by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]])
+ also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
+ by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
- by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
finally show "x' \<le> \<dots>" .
qed
next
@@ -783,7 +783,7 @@
end
-subsection {* Admissibility *}
+subsection \<open>Admissibility\<close>
lemma admissible_subst:
assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
@@ -860,10 +860,10 @@
fix x
assume "x \<in> f ` A"
then obtain y where "y \<in> A" "x = f y" by blast note this(2)
- also have "f y \<le> g y" using le `y \<in> A` by simp
+ also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp
also have "Complete_Partial_Order.chain op \<le> (g ` A)"
using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
- hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`)
+ hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>)
finally show "x \<le> \<dots>" .
qed
also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
@@ -992,7 +992,7 @@
end
-subsection {* @{term "op ="} as order *}
+subsection \<open>@{term "op ="} as order\<close>
definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
@@ -1038,7 +1038,7 @@
\<Longrightarrow> mcont the_Sup op = lub ord f"
by(simp add: mcont_def cont_eqI monotone_eqI)
-subsection {* ccpo for products *}
+subsection \<open>ccpo for products\<close>
definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
@@ -1197,7 +1197,7 @@
with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
- by(simp add: prod_lub_def `Y \<noteq> {}` lub_singleton_def)
+ by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
qed
lemma cont_prodD2:
@@ -1253,9 +1253,9 @@
have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
by(simp add: prod_lub_def)
also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y)"
- by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] `Y \<noteq> {}`)
+ by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] \<open>Y \<noteq> {}\<close>)
also from cont1 have "\<And>x. f (x, lubb (snd ` Y)) = \<Squnion>((\<lambda>y. f (x, y)) ` snd ` Y)"
- by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] `Y \<noteq> {}`)
+ by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] \<open>Y \<noteq> {}\<close>)
hence "\<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y) = \<Squnion>((\<lambda>x. \<dots> x) ` fst ` Y)" by simp
also have "\<dots> = \<Squnion>((\<lambda>x. f (fst x, snd x)) ` Y)"
unfolding image_image split_def using chain
@@ -1330,7 +1330,7 @@
shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
-subsection {* Complete lattices as ccpo *}
+subsection \<open>Complete lattices as ccpo\<close>
context complete_lattice begin
@@ -1374,8 +1374,8 @@
fix y
assume "y \<in> op \<squnion> x ` Y"
then obtain z where "y = x \<squnion> z" and "z \<in> Y" by blast
- from `z \<in> Y` have "z \<le> \<Squnion>Y" by(rule Sup_upper)
- with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding `y = x \<squnion> z` by(rule sup_mono) simp
+ from \<open>z \<in> Y\<close> have "z \<le> \<Squnion>Y" by(rule Sup_upper)
+ with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding \<open>y = x \<squnion> z\<close> by(rule sup_mono) simp
next
fix y
assume upper: "\<And>z. z \<in> op \<squnion> x ` Y \<Longrightarrow> z \<le> y"
@@ -1385,8 +1385,8 @@
assume "z \<in> insert x Y"
from assms obtain z' where "z' \<in> Y" by blast
let ?z = "if z \<in> Y then x \<squnion> z else x \<squnion> z'"
- have "z \<le> x \<squnion> ?z" using `z' \<in> Y` `z \<in> insert x Y` by auto
- also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: `z' \<in> Y`)
+ have "z \<le> x \<squnion> ?z" using \<open>z' \<in> Y\<close> \<open>z \<in> insert x Y\<close> by auto
+ also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: \<open>z' \<in> Y\<close>)
finally show "z \<le> y" .
qed
qed
@@ -1426,14 +1426,14 @@
interpretation lfp: partial_function_definitions "op \<le> :: _ :: complete_lattice \<Rightarrow> _" Sup
by(rule complete_lattice_partial_function_definitions)
-declaration {* Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
- @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE *}
+declaration \<open>Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
+ @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
interpretation gfp: partial_function_definitions "op \<ge> :: _ :: complete_lattice \<Rightarrow> _" Inf
by(rule complete_lattice_partial_function_definitions_dual)
-declaration {* Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
- @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE *}
+declaration \<open>Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
+ @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
lemma insert_mono [partial_function_mono]:
"monotone (fun_ord op \<subseteq>) op \<subseteq> A \<Longrightarrow> monotone (fun_ord op \<subseteq>) op \<subseteq> (\<lambda>y. insert x (A y))"
@@ -1505,23 +1505,23 @@
fix u
assume "u \<in> (\<lambda>x. g x z) ` Y"
then obtain y' where "u = g y' z" "y' \<in> Y" by auto
- from chain `y \<in> Y` `y' \<in> Y` have "ord y y' \<or> ord y' y" by(rule chainD)
+ from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "ord y y' \<or> ord y' y" by(rule chainD)
thus "u \<le> ?rhs"
proof
- note `u = g y' z` also
+ note \<open>u = g y' z\<close> also
assume "ord y y'"
with f have "f y \<subseteq> f y'" by(rule mcont_monoD)
- with `z \<in> f y`
+ with \<open>z \<in> f y\<close>
have "g y' z \<le> \<Squnion>(g y' ` f y')" by(auto intro: Sup_upper)
- also have "\<dots> \<le> ?rhs" using `y' \<in> Y` by(auto intro: Sup_upper)
+ also have "\<dots> \<le> ?rhs" using \<open>y' \<in> Y\<close> by(auto intro: Sup_upper)
finally show ?thesis .
next
- note `u = g y' z` also
+ note \<open>u = g y' z\<close> also
assume "ord y' y"
with g have "g y' z \<le> g y z" by(rule mcont_monoD)
- also have "\<dots> \<le> \<Squnion>(g y ` f y)" using `z \<in> f y`
+ also have "\<dots> \<le> \<Squnion>(g y ` f y)" using \<open>z \<in> f y\<close>
by(auto intro: Sup_upper)
- also have "\<dots> \<le> ?rhs" using `y \<in> Y` by(auto intro: Sup_upper)
+ also have "\<dots> \<le> ?rhs" using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
finally show ?thesis .
qed
qed
@@ -1537,11 +1537,11 @@
fix u
assume "u \<in> g y ` f y"
then obtain z where "u = g y z" "z \<in> f y" by auto
- note `u = g y z`
+ note \<open>u = g y z\<close>
also have "g y z \<le> \<Squnion>((\<lambda>x. g x z) ` Y)"
- using `y \<in> Y` by(auto intro: Sup_upper)
+ using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
also have "\<dots> = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
- also have "\<dots> \<le> ?lhs" using `z \<in> f y` `y \<in> Y`
+ also have "\<dots> \<le> ?lhs" using \<open>z \<in> f y\<close> \<open>y \<in> Y\<close>
by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
finally show "u \<le> ?lhs" .
qed
@@ -1567,7 +1567,7 @@
shows admissible_Bex: "ccpo.admissible Union op \<subseteq> (\<lambda>A. \<exists>x\<in>A. P x)"
by(rule ccpo.admissibleI)(auto)
-subsection {* Parallel fixpoint induction *}
+subsection \<open>Parallel fixpoint induction\<close>
context
fixes luba :: "'a set \<Rightarrow> 'a"
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Sun Apr 03 23:01:39 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Sun Apr 03 23:03:30 2016 +0200
@@ -964,7 +964,7 @@
proof -
have f0: "(f \<longlongrightarrow> 0) at_infinity"
proof -
- have DIM_complex[intro]: "2 \<le> DIM(complex)" --\<open>should not be necessary!\<close>
+ have DIM_complex[intro]: "2 \<le> DIM(complex)" \<comment>\<open>should not be necessary!\<close>
by simp
have "continuous_on (inverse ` (ball 0 r - {0})) f"
using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast
@@ -2149,61 +2149,61 @@
proof -
assume "n>m"
have "(h \<longlongrightarrow> 0) (at z within ball z r)"
- proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (n - m) * g w"])
- have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using `n>m` asm
+ proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (n - m) * g w"])
+ have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using \<open>n>m\<close> asm
by (auto simp add:field_simps power_diff)
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) ^ (n - m) * g x' = h x'" for x' by auto
next
def F\<equiv>"at z within ball z r"
and f'\<equiv>"\<lambda>x. (x - z) ^ (n-m)"
- have "f' z=0" using `n>m` unfolding f'_def by auto
+ have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def
by (intro continuous_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(g \<longlongrightarrow> g z) F"
- using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] `r>0`
+ using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \<open>r>0\<close>
unfolding F_def by auto
ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
qed
moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)"
using holomorphic_on_imp_continuous_on[OF h_holo]
- by (auto simp add:continuous_on_def `r>0`)
- moreover have "at z within ball z r \<noteq> bot" using `r>0`
+ by (auto simp add:continuous_on_def \<open>r>0\<close>)
+ moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close>
by (auto simp add:trivial_limit_within islimpt_ball)
ultimately have "h z=0" by (auto intro: tendsto_unique)
- thus False using asm `r>0` by auto
+ thus False using asm \<open>r>0\<close> by auto
qed
moreover have "m>n \<Longrightarrow> False"
proof -
assume "m>n"
have "(g \<longlongrightarrow> 0) (at z within ball z r)"
- proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (m - n) * h w"])
- have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using `m>n` asm
+ proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (m - n) * h w"])
+ have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using \<open>m>n\<close> asm
by (auto simp add:field_simps power_diff)
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) ^ (m - n) * h x' = g x'" for x' by auto
next
def F\<equiv>"at z within ball z r"
and f'\<equiv>"\<lambda>x. (x - z) ^ (m-n)"
- have "f' z=0" using `m>n` unfolding f'_def by auto
+ have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def
by (intro continuous_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(h \<longlongrightarrow> h z) F"
- using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] `r>0`
+ using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close>
unfolding F_def by auto
ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
qed
moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)"
using holomorphic_on_imp_continuous_on[OF g_holo]
- by (auto simp add:continuous_on_def `r>0`)
- moreover have "at z within ball z r \<noteq> bot" using `r>0`
+ by (auto simp add:continuous_on_def \<open>r>0\<close>)
+ moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close>
by (auto simp add:trivial_limit_within islimpt_ball)
ultimately have "g z=0" by (auto intro: tendsto_unique)
- thus False using asm `r>0` by auto
+ thus False using asm \<open>r>0\<close> by auto
qed
ultimately show "n=m" by fastforce
qed
@@ -2220,18 +2220,18 @@
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 s` `connected s` `z\<in>s` `f z=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))
def 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'"
"(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
- using g `ball z r \<subseteq> s` by auto
- moreover have "r'>0" unfolding r'_def using `0<r` by auto
+ using g \<open>ball z r \<subseteq> s\<close> by auto
+ moreover have "r'>0" unfolding r'_def using \<open>0<r\<close> by auto
ultimately show "\<exists>n 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)"
apply (intro exI[of _ n] exI[of _ g] exI[of _ r'])
- by (simp add:`0 < n`)
+ by (simp add:\<open>0 < n\<close>)
next
fix m n
def fac\<equiv>"\<lambda>n g r. \<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0"
@@ -2242,7 +2242,7 @@
obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2"
and "fac m h r2" using m_asm by auto
def r\<equiv>"min r1 r2"
- have "r>0" using `r1>0` `r2>0` unfolding r_def by auto
+ have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
moreover have "\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0"
using \<open>fac m h r2\<close> \<open>fac n g r1\<close> unfolding fac_def r_def
by fastforce
@@ -2257,11 +2257,11 @@
proof
fix p assume "p\<in>s"
then obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> s"
- using open_contains_ball_eq[OF `open s`] by auto
+ using open_contains_ball_eq[OF \<open>open s\<close>] by auto
obtain e2 where "0<e2" and "\<forall>x\<in>pts. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
- using finite_set_avoid[OF `finite pts`,of p] by auto
+ using finite_set_avoid[OF \<open>finite pts\<close>,of p] by auto
hence "\<forall>w\<in>ball p (min e1 e2). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" using e1_b by auto
- thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` `e1>0`
+ thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using \<open>e2>0\<close> \<open>e1>0\<close>
apply (rule_tac x="min e1 e2" in exI)
by auto
qed
@@ -2275,33 +2275,33 @@
then obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)"
using finite_ball_avoid[OF assms] by auto
def e2\<equiv>"e1/2"
- have "e2>0" and "e2<e1" unfolding e2_def using `e1>0` by auto
+ have "e2>0" and "e2<e1" unfolding e2_def using \<open>e1>0\<close> by auto
then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
- then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` e1 by auto
+ then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using \<open>e2>0\<close> e1 by auto
qed
lemma get_integrable_path:
assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b"
"path_image g \<subseteq> s-pts" "f contour_integrable_on g" using assms
-proof (induct arbitrary:s thesis a rule:finite_induct[OF `finite pts`]) print_cases
+proof (induct arbitrary:s thesis a rule:finite_induct[OF \<open>finite pts\<close>]) print_cases
case 1
obtain g where "valid_path g" "path_image g \<subseteq> s" "pathstart g = a" "pathfinish g = b"
- using connected_open_polynomial_connected[OF `open s`,of a b ] `connected (s - {})`
+ using connected_open_polynomial_connected[OF \<open>open s\<close>,of a b ] \<open>connected (s - {})\<close>
valid_path_polynomial_function "1.prems"(6) "1.prems"(7) by auto
moreover have "f contour_integrable_on g"
- using contour_integrable_holomorphic_simple[OF _ `open s` `valid_path g` `path_image g \<subseteq> s`,of f]
- `f holomorphic_on s - {}`
+ using contour_integrable_holomorphic_simple[OF _ \<open>open s\<close> \<open>valid_path g\<close> \<open>path_image g \<subseteq> s\<close>,of f]
+ \<open>f holomorphic_on s - {}\<close>
by auto
ultimately show ?case using "1"(1)[of g] by auto
next
case idt:(2 p pts)
obtain e where "e>0" and e:"\<forall>w\<in>ball a e. w \<in> s \<and> (w \<noteq> a \<longrightarrow> w \<notin> insert p pts)"
- using finite_ball_avoid[OF `open s` `finite (insert p pts)`,rule_format,of a]
- `a \<in> s - insert p pts`
+ using finite_ball_avoid[OF \<open>open s\<close> \<open>finite (insert p pts)\<close>,rule_format,of a]
+ \<open>a \<in> s - insert p pts\<close>
by auto
def a'\<equiv>"a+e/2"
- have "a'\<in>s-{p} -pts" using e[rule_format,of "a+e/2"] `e>0`
+ have "a'\<in>s-{p} -pts" using e[rule_format,of "a+e/2"] \<open>e>0\<close>
by (auto simp add:dist_complex_def a'_def)
then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b"
"path_image g' \<subseteq> s - {p} - pts" "f contour_integrable_on g'"
@@ -2312,7 +2312,7 @@
moreover have "pathstart g = a" and "pathfinish g = b" unfolding g_def by auto
moreover have "path_image g \<subseteq> s - insert p pts" unfolding g_def
proof (rule subset_path_image_join)
- have "closed_segment a a' \<subseteq> ball a e" using `e>0`
+ have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close>
by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
then show "path_image (linepath a a') \<subseteq> s - insert p pts" using e idt(9)
by auto
@@ -2321,7 +2321,7 @@
qed
moreover have "f contour_integrable_on g"
proof -
- have "closed_segment a a' \<subseteq> ball a e" using `e>0`
+ have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close>
by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
then have "continuous_on (closed_segment a a') f"
using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)]
@@ -2331,7 +2331,7 @@
using contour_integrable_continuous_linepath by auto
then show ?thesis unfolding g_def
apply (rule contour_integrable_joinI)
- by (auto simp add: `e>0`)
+ by (auto simp add: \<open>e>0\<close>)
qed
ultimately show ?case using idt.prems(1)[of g] by auto
qed
@@ -2343,32 +2343,32 @@
"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
using assms
-proof (induct arbitrary:s g rule:finite_induct[OF `finite pts`])
+proof (induct arbitrary:s g rule:finite_induct[OF \<open>finite pts\<close>])
case 1
then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique)
next
case (2 p pts)
- note fin[simp] = `finite (insert p pts)`
- and connected = `connected (s - insert p pts)`
- and valid[simp] = `valid_path g`
- and g_loop[simp] = `pathfinish g = pathstart g`
- and holo[simp]= `f holomorphic_on s - insert p pts`
- and path_img = `path_image g \<subseteq> s - insert p pts`
- and winding = `\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0`
- and h = `\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))`
+ note fin[simp] = \<open>finite (insert p pts)\<close>
+ and connected = \<open>connected (s - insert p pts)\<close>
+ and valid[simp] = \<open>valid_path g\<close>
+ and g_loop[simp] = \<open>pathfinish g = pathstart g\<close>
+ and holo[simp]= \<open>f holomorphic_on s - insert p pts\<close>
+ and path_img = \<open>path_image g \<subseteq> s - insert p pts\<close>
+ and winding = \<open>\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0\<close>
+ and h = \<open>\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))\<close>
have "h p>0" and "p\<in>s"
and h_p: "\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> insert p pts)"
- using h `insert p pts \<subseteq> s` by auto
+ using h \<open>insert p pts \<subseteq> s\<close> by auto
obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p"
"path_image pg \<subseteq> s-insert p pts" "f contour_integrable_on pg"
proof -
have "p + h p\<in>cball p (h p)" using h[rule_format,of p]
by (simp add: \<open>p \<in> s\<close> dist_norm)
- then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] `insert p pts \<subseteq> s`
+ then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close>
by fastforce
moreover have "pathstart g \<in> s - insert p pts " using path_img by auto
ultimately show ?thesis
- using get_integrable_path[OF `open s` connected fin holo,of "pathstart g" "p+h p"] that
+ using get_integrable_path[OF \<open>open s\<close> connected fin holo,of "pathstart g" "p+h p"] that
by blast
qed
obtain n::int where "n=winding_number g p"
@@ -2394,7 +2394,7 @@
and "pathstart (n_circ 0) = p + h p"
and "pathfinish (n_circ 0) = p + h p"
and "p \<notin> path_image (n_circ 0)"
- unfolding n_circ_def p_circ_pt_def using `h p > 0`
+ unfolding n_circ_def p_circ_pt_def using \<open>h p > 0\<close>
by (auto simp add: dist_norm)
show "winding_number (n_circ 0) p'=0 \<and> p'\<notin>path_image (n_circ 0)" when "p'\<notin>s- pts" for p'
unfolding n_circ_def p_circ_pt_def
@@ -2409,7 +2409,7 @@
case (Suc k)
have n_Suc:"n_circ (Suc k) = p_circ +++ n_circ k" unfolding n_circ_def by auto
have pcirc:"p \<notin> path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)"
- using Suc(3) unfolding p_circ_def using `h p > 0` by (auto simp add: p_circ_def)
+ using Suc(3) unfolding p_circ_def using \<open>h p > 0\<close> by (auto simp add: p_circ_def)
have pcirc_image:"path_image p_circ \<subseteq> s - insert p pts"
proof -
have "path_image p_circ \<subseteq> cball p (h p)" using \<open>0 < h p\<close> p_circ_def by auto
@@ -2426,15 +2426,15 @@
proof -
have "path_image p_circ = sphere p (h p)"
unfolding p_circ_def using \<open>0 < h p\<close> by auto
- then show ?thesis unfolding n_Suc using Suc.hyps(5) `h p>0`
+ then show ?thesis unfolding n_Suc using Suc.hyps(5) \<open>h p>0\<close>
by (auto simp add: path_image_join[OF pcirc(3)] dist_norm)
qed
- then show "p \<notin> path_image (n_circ (Suc k))" using `h p>0` by auto
+ then show "p \<notin> path_image (n_circ (Suc k))" using \<open>h p>0\<close> by auto
show "winding_number (n_circ (Suc k)) p = of_nat (Suc k)"
proof -
have "winding_number p_circ p = 1"
- by (simp add: `h p > 0` p_circ_def winding_number_circlepath_centre)
- moreover have "p \<notin> path_image (n_circ k)" using Suc(5) `h p>0` by auto
+ by (simp add: \<open>h p > 0\<close> p_circ_def winding_number_circlepath_centre)
+ moreover have "p \<notin> path_image (n_circ k)" using Suc(5) \<open>h p>0\<close> by auto
then have "winding_number (p_circ +++ n_circ k) p
= winding_number p_circ p + winding_number (n_circ k) p"
using valid_path_imp_path Suc.hyps(1) Suc.hyps(2) pcirc
@@ -2485,14 +2485,14 @@
using n_circ unfolding cp_def by auto
next
have "sphere p (h p) \<subseteq> s - insert p pts"
- using h[rule_format,of p] `insert p pts \<subseteq> s` by force
+ using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close> by force
moreover have "p + complex_of_real (h p) \<in> s - insert p pts"
using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE)
ultimately show "path_image cp \<subseteq> s - insert p pts" unfolding cp_def
using n_circ(5) by auto
next
show "winding_number cp p = - n"
- unfolding cp_def using winding_number_reversepath n_circ `h p>0` by auto
+ unfolding cp_def using winding_number_reversepath n_circ \<open>h p>0\<close> by auto
next
show "winding_number cp p'=0 \<and> p' \<notin> path_image cp" when "p'\<notin>s - pts" for p'
unfolding cp_def
@@ -2509,11 +2509,11 @@
qed
def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)"
have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
- proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ `finite pts` ])
+ proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \<open>finite pts\<close> ])
show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
- show "open (s - {p})" using `open s` by auto
- show " pts \<subseteq> s - {p}" using `insert p pts \<subseteq> s` ` p \<notin> pts` by blast
- show "f holomorphic_on s - {p} - pts" using holo `p \<notin> pts` by (metis Diff_insert2)
+ show "open (s - {p})" using \<open>open s\<close> by auto
+ show " pts \<subseteq> s - {p}" using \<open>insert p pts \<subseteq> s\<close> \<open> p \<notin> pts\<close> by blast
+ show "f holomorphic_on s - {p} - pts" using holo \<open>p \<notin> pts\<close> by (metis Diff_insert2)
show "valid_path g'"
unfolding g'_def cp_def using n_circ valid pg g_loop
by (auto intro!:valid_path_join )
@@ -2536,7 +2536,7 @@
have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z
+ winding_number (pg +++ cp +++ (reversepath pg)) z"
proof (rule winding_number_join)
- show "path g" using `valid_path g` by simp
+ show "path g" using \<open>valid_path g\<close> by simp
show "z \<notin> path_image g" using z path_img by auto
show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto
next
@@ -2568,7 +2568,7 @@
finally have "winding_number g' z = winding_number g z + winding_number cp z"
unfolding g'_def .
moreover have "winding_number g z + winding_number cp z = 0"
- using winding z `n=winding_number g p` by auto
+ using winding z \<open>n=winding_number g p\<close> by auto
ultimately show "winding_number g' z = 0" unfolding g'_def by auto
qed
show "\<forall>pa\<in>s - {p}. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s - {p} \<and> (w \<noteq> pa \<longrightarrow> w \<notin> pts))"
@@ -2581,7 +2581,7 @@
+ contour_integral (pg +++ cp +++ reversepath pg) f"
unfolding g'_def
apply (subst Cauchy_Integral_Thm.contour_integral_join)
- by (auto simp add:open_Diff[OF `open s`,OF finite_imp_closed[OF fin]]
+ by (auto simp add:open_Diff[OF \<open>open s\<close>,OF finite_imp_closed[OF fin]]
intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img]
contour_integrable_reversepath)
also have "... = contour_integral g f + contour_integral pg f
@@ -2596,7 +2596,7 @@
using contour_integral_reversepath
by (auto simp add:contour_integrable_reversepath)
also have "... = contour_integral g f - winding_number g p * contour_integral p_circ f"
- using `n=winding_number g p` by auto
+ using \<open>n=winding_number g p\<close> by auto
finally show ?thesis .
qed
moreover have "winding_number g' p' = winding_number g p'" when "p'\<in>pts" for p'
@@ -2631,7 +2631,7 @@
ultimately show ?case unfolding p_circ_def
apply (subst (asm) setsum.cong[OF refl,
of pts _ "\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"])
- by (auto simp add:setsum.insert[OF `finite pts` `p\<notin>pts`] algebra_simps)
+ by (auto simp add:setsum.insert[OF \<open>finite pts\<close> \<open>p\<notin>pts\<close>] algebra_simps)
qed
@@ -2652,7 +2652,7 @@
have "pts=pts1 \<union> pts2" "pts1 \<inter> pts2 = {}" "pts2 \<inter> s={}" "pts1\<subseteq>s"
unfolding pts1_def pts2_def by auto
have "contour_integral g f = (\<Sum>p\<in>pts1. circ p)" unfolding circ_def
- proof (rule Cauchy_theorem_aux[OF `open s` _ _ `pts1\<subseteq>s` _ `valid_path g` loop _ homo])
+ proof (rule Cauchy_theorem_aux[OF \<open>open s\<close> _ _ \<open>pts1\<subseteq>s\<close> _ \<open>valid_path g\<close> loop _ homo])
show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def)
show "finite pts1" using \<open>pts = pts1 \<union> pts2\<close> assms(3) by auto
show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def)
@@ -2663,14 +2663,14 @@
moreover have "setsum circ pts2=0"
proof -
have "winding_number g p=0" when "p\<in>pts2" for p
- using `pts2 \<inter> s={}` that homo[rule_format,of p] by auto
+ using \<open>pts2 \<inter> s={}\<close> that homo[rule_format,of p] by auto
thus ?thesis unfolding circ_def
apply (intro setsum.neutral)
by auto
qed
moreover have "?R=setsum circ pts1 + setsum circ pts2"
unfolding circ_def
- using setsum.union_disjoint[OF _ _ `pts1 \<inter> pts2 = {}`] `finite pts` `pts=pts1 \<union> pts2`
+ using setsum.union_disjoint[OF _ _ \<open>pts1 \<inter> pts2 = {}\<close>] \<open>finite pts\<close> \<open>pts=pts1 \<union> pts2\<close>
by blast
ultimately show ?thesis
apply (fold circ_def)
@@ -2717,8 +2717,8 @@
have "(\<exists>!n. n>0 \<and> (\<exists> h r. P h r n))"
proof -
have "\<exists>!n. \<exists>h r. n>0 \<and> P h r n"
- using holomorphic_factor_zero_Ex1[OF `open s` `connected s` `z\<in>s` holo `f z=0`
- `\<exists>w\<in>s. f w\<noteq>0`] unfolding P_def
+ using holomorphic_factor_zero_Ex1[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close>
+ \<open>\<exists>w\<in>s. f w\<noteq>0\<close>] unfolding P_def
apply (subst mult.commute)
by auto
thus ?thesis by auto
@@ -2738,10 +2738,10 @@
obtain r2 where "r2>0" "cball z r2 \<subseteq> s"
using assms(3) assms(5) open_contains_cball_eq by blast
def r3\<equiv>"min r1 r2"
- have "P h r3 n" using `P h r1 n` `r2>0` unfolding P_def r3_def
+ have "P h r3 n" using \<open>P h r1 n\<close> \<open>r2>0\<close> unfolding P_def r3_def
by auto
- moreover have "cball z r3 \<subseteq> s" using `cball z r2 \<subseteq> s` unfolding r3_def by auto
- ultimately show ?thesis using `n>0` unfolding P_def by auto
+ moreover have "cball z r3 \<subseteq> s" using \<open>cball z r2 \<subseteq> s\<close> unfolding r3_def by auto
+ ultimately show ?thesis using \<open>n>0\<close> unfolding P_def by auto
qed
lemma porder_exist:
@@ -2756,8 +2756,8 @@
def zo\<equiv>"zorder (inverse \<circ> f) z" and zp\<equiv>"zer_poly (inverse \<circ> f) z"
obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> s" and zp_holo: "zp holomorphic_on cball z r" and
zp_fac: "\<forall>w\<in>cball z r. (inverse \<circ> f) w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0"
- using zorder_exist[OF `open s` `connected s` `z\<in>s` holo,folded zo_def zp_def]
- `f z=0` `\<exists>w\<in>s. f w\<noteq>0`
+ using zorder_exist[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo,folded zo_def zp_def]
+ \<open>f z=0\<close> \<open>\<exists>w\<in>s. f w\<noteq>0\<close>
by auto
have n:"n=zo" and h:"h=inverse o zp"
unfolding n_def zo_def porder_def h_def zp_def pol_poly_def by simp_all
@@ -2767,8 +2767,8 @@
using zp_fac unfolding h n comp_def
by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq
inverse_mult_distrib mult.commute)
- moreover have "0 < n" unfolding n using `zo>0` by simp
- ultimately show ?thesis using `0 < r` `cball z r \<subseteq> s` by auto
+ moreover have "0 < n" unfolding n using \<open>zo>0\<close> by simp
+ ultimately show ?thesis using \<open>0 < r\<close> \<open>cball z r \<subseteq> s\<close> by auto
qed
lemma base_residue:
@@ -2785,7 +2785,7 @@
r_b:"cball z r \<subseteq> s" and
h_holo:"h holomorphic_on cball z r"
and h:"(\<forall>w\<in>cball z r. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)"
- using porder_exist[OF `open s` `connected s` `z\<in>s` holo `f z=0` non_c]
+ using porder_exist[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close> non_c]
unfolding n_def h_def by auto
def c\<equiv>"complex_of_real (2 * pi) * \<i>"
have "residue f z = (deriv ^^ (n - 1)) h z / fact (n-1)"
@@ -2795,15 +2795,15 @@
then have "((\<lambda>u. h u / (u - z) ^ n) has_contour_integral c * residue f z)
(circlepath z r)"
using Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n -1"
- ,unfolded Suc_diff_1[OF `n>0`],folded c_def] h_holo r_b
- by (auto simp add:`r>0` holomorphic_on_imp_continuous_on holomorphic_on_subset)
+ ,unfolded Suc_diff_1[OF \<open>n>0\<close>],folded c_def] h_holo r_b
+ by (auto simp add:\<open>r>0\<close> holomorphic_on_imp_continuous_on holomorphic_on_subset)
then have "(f has_contour_integral c * residue f z) (circlepath z r)"
proof (elim has_contour_integral_eq)
fix x assume "x \<in> path_image (circlepath z r)"
hence "x\<in>cball z r" using \<open>0 < r\<close> by auto
then show "h x / (x - z) ^ n = f x" using h by auto
qed
- then show ?thesis using `r>0` `cball z r \<subseteq> s` unfolding c_def by auto
+ then show ?thesis using \<open>r>0\<close> \<open>cball z r \<subseteq> s\<close> unfolding c_def by auto
qed
theorem residue_theorem:
@@ -2822,26 +2822,26 @@
def contour\<equiv>"\<lambda>p e. (f has_contour_integral c * residue f p) (circlepath p e)"
def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
have "poles \<subseteq> pts" and "finite pts"
- using poles `finite {p. f p=0}` unfolding pts_def is_pole_def by auto
+ using poles \<open>finite {p. f p=0}\<close> unfolding pts_def is_pole_def by auto
have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> contour p e)"
when "p\<in>s" for p
proof -
obtain e1 where e:"e1>0" and e:"avoid p e1"
- using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+ using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> contour p e2"
when "p\<in>poles" unfolding c_def contour_def
- proof (rule base_residue[of "ball p e1" p f,simplified,OF `e1>0`])
+ proof (rule base_residue[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>])
show "inverse \<circ> f holomorphic_on ball p e1"
proof -
def f'\<equiv>"inverse o f"
have "f holomorphic_on ball p e1 - {p}"
- using holo e `poles \<subseteq> pts` unfolding avoid_def
+ using holo e \<open>poles \<subseteq> pts\<close> unfolding avoid_def
apply (elim holomorphic_on_subset)
by auto
then have f'_holo:"f' holomorphic_on ball p e1 - {p}" unfolding f'_def comp_def
apply (elim holomorphic_on_inverse)
using e pts_def ball_subset_cball unfolding avoid_def by blast
- moreover have "isCont f' p" using `p\<in>poles` poles unfolding f'_def is_pole_def by auto
+ moreover have "isCont f' p" using \<open>p\<in>poles\<close> poles unfolding f'_def is_pole_def by auto
ultimately show "f' holomorphic_on ball p e1"
apply (elim no_isolated_singularity[rotated])
apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
@@ -2849,10 +2849,10 @@
holomorphic_on_imp_differentiable_at by fastforce
qed
next
- show "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+ show "f p = 0" using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
next
def p'\<equiv>"p+e1/2"
- have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+ have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
apply (rule_tac x=p' in bexI)
by (auto simp add:pts_def)
@@ -2861,7 +2861,7 @@
def e3\<equiv>"if p\<in>poles then e2 else e1"
have "avoid p e3"
using e2 e that avoid_def e3_def by auto
- moreover have "e3>0" using `e1>0` e2 unfolding e3_def by auto
+ moreover have "e3>0" using \<open>e1>0\<close> e2 unfolding e3_def by auto
moreover have " p\<in>poles \<longrightarrow> contour p e3" using e2 unfolding e3_def by auto
ultimately show ?thesis by auto
qed
@@ -2870,12 +2870,12 @@
def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (h p)) f"
have "contour_integral \<gamma> f = (\<Sum>p\<in>poles. winding_number \<gamma> p * cont p)"
unfolding cont_def
- proof (rule Cauchy_theorem_singularities[OF `open s` `connected (s-poles)` _ holo `valid_path \<gamma>`
- loop `path_image \<gamma> \<subseteq> s-poles` homo])
- show "finite poles" using `poles \<subseteq> pts` and `finite pts` by (simp add: finite_subset)
+ proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected (s-poles)\<close> _ holo \<open>valid_path \<gamma>\<close>
+ loop \<open>path_image \<gamma> \<subseteq> s-poles\<close> homo])
+ show "finite poles" using \<open>poles \<subseteq> pts\<close> and \<open>finite pts\<close> by (simp add: finite_subset)
next
show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> poles))"
- using `poles \<subseteq> pts` h unfolding avoid_def by blast
+ using \<open>poles \<subseteq> pts\<close> h unfolding avoid_def by blast
qed
also have "... = (\<Sum>p\<in>poles. c * (winding_number \<gamma> p * residue f p))"
proof (rule setsum.cong[of poles poles,simplified])
@@ -2886,7 +2886,7 @@
then have "cont p=c*residue f p"
unfolding cont_def
apply (intro contour_integral_unique)
- using h[unfolded contour_def] `p \<in> poles` by blast
+ using h[unfolded contour_def] \<open>p \<in> poles\<close> by blast
then show ?thesis by auto
next
assume "p\<notin>s"
@@ -2925,12 +2925,12 @@
def cont_zero\<equiv>"\<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
have "poles \<subseteq> pts" and "zeros \<subseteq> pts" and "finite zeros" and "pts=zeros \<union> poles"
- using poles `finite pts` unfolding pts_def zeros_def is_pole_def by auto
+ using poles \<open>finite pts\<close> unfolding pts_def zeros_def is_pole_def by auto
have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> cont_pole ff p e) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p e)"
when "p\<in>s" for p
proof -
obtain e1 where e:"e1>0" and e:"avoid p e1"
- using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+ using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
when "p\<in>poles"
proof -
@@ -2941,7 +2941,7 @@
have "inverse \<circ> f holomorphic_on ball p e1"
proof -
have "f holomorphic_on ball p e1 - {p}"
- using f_holo e `poles \<subseteq> pts` unfolding avoid_def
+ using f_holo e \<open>poles \<subseteq> pts\<close> unfolding avoid_def
apply (elim holomorphic_on_subset)
by auto
then have inv_holo:"(inverse o f) holomorphic_on ball p e1 - {p}"
@@ -2949,7 +2949,7 @@
apply (elim holomorphic_on_inverse)
using e pts_def ball_subset_cball unfolding avoid_def by blast
moreover have "isCont (inverse o f) p"
- using `p\<in>poles` poles unfolding is_pole_def by auto
+ using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
ultimately show "(inverse o f) holomorphic_on ball p e1"
apply (elim no_isolated_singularity[rotated])
apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
@@ -2957,11 +2957,11 @@
holomorphic_on_imp_differentiable_at unfolding comp_def
by fastforce
qed
- moreover have "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+ moreover have "f p = 0" using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0"
proof -
def p'\<equiv>"p+e1/2"
- have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+ have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
apply (rule_tac x=p' in bexI)
by (auto simp add:pts_def)
@@ -2971,50 +2971,50 @@
"cball p r \<subseteq> ball p e1" and
pp_holo:"pp holomorphic_on cball p r" and
pp_po:"(\<forall>w\<in>cball p r. f w = pp w / (w - p) ^ po \<and> pp w \<noteq> 0)"
- using porder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding po_def pp_def
+ using porder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding po_def pp_def
by auto
def e2\<equiv>"r/2"
- have "e2>0" using `r>0` unfolding e2_def by auto
+ have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
def anal\<equiv>"\<lambda>w. deriv pp w * h w / pp w" and prin\<equiv>"\<lambda>w. - of_nat po * h w / (w - p)"
have "((\<lambda>w. prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r \<subseteq> s"
using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
then have "cball p e2 \<subseteq> s"
- using `r>0` unfolding e2_def by auto
+ using \<open>r>0\<close> unfolding e2_def by auto
then have "(\<lambda>w. - of_nat po * h w) holomorphic_on cball p e2"
using h_holo
by (auto intro!: holomorphic_intros)
then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)"
using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. - of_nat po * h w"]
- `e2>0`
+ \<open>e2>0\<close>
unfolding prin_def
by (auto simp add: mult.assoc)
have "anal holomorphic_on ball p r" unfolding anal_def
- using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+ using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close>
by (auto intro!: holomorphic_intros)
then show "(anal has_contour_integral 0) (circlepath p e2)"
- using e2_def `r>0`
+ using e2_def \<open>r>0\<close>
by (auto elim!: Cauchy_theorem_disc_simple)
qed
then have "cont_pole ff' p e2" unfolding cont_pole_def po_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
def wp\<equiv>"w-p"
have "wp\<noteq>0" and "pp w \<noteq>0"
- unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto
+ unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto
moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
proof (rule DERIV_imp_deriv)
def der \<equiv> "- po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
- have po:"po = Suc (po - Suc 0) " using `po>0` by auto
+ have po:"po = Suc (po - Suc 0) " using \<open>po>0\<close> by auto
have "(pp has_field_derivative (deriv pp w)) (at w)"
- using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+ using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
holomorphic_on_imp_differentiable_at[of _ "ball p r"]
holomorphic_on_subset [OF pp_holo ball_subset_cball]
by (metis open_ball)
then show "(f' has_field_derivative der) (at w)"
- using `w\<noteq>p` `po>0` unfolding der_def f'_def
+ using \<open>w\<noteq>p\<close> \<open>po>0\<close> unfolding der_def f'_def
apply (auto intro!: derivative_eq_intros simp add:field_simps)
apply (subst (4) po)
apply (subst power_Suc)
@@ -3030,7 +3030,7 @@
then have "cont_pole ff p e2" unfolding cont_pole_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
have "deriv f' w = deriv f w"
proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
@@ -3038,14 +3038,14 @@
next
have "ball p e1 - {p} \<subseteq> s - poles"
using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
- then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+ then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
using ball_subset_cball by blast
then show "f holomorphic_on ball p r - {p}" using f_holo
by auto
next
show "open (ball p r - {p})" by auto
next
- show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+ show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
next
fix x assume "x \<in> ball p r - {p}"
then show "f' x = f x"
@@ -3058,7 +3058,7 @@
qed
moreover have "cball p e2 \<subseteq> ball p e1"
using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
- ultimately show ?thesis using `e2>0` by auto
+ ultimately show ?thesis using \<open>e2>0\<close> by auto
qed
then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
by auto
@@ -3075,12 +3075,12 @@
using \<open>poles \<subseteq> pts\<close> avoid_def ball_subset_cball e that zeros_def by fastforce
thus ?thesis using f_holo by auto
qed
- moreover have "f p = 0" using `p\<in>zeros`
+ moreover have "f p = 0" using \<open>p\<in>zeros\<close>
using DiffD1 mem_Collect_eq pts_def zeros_def by blast
moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0"
proof -
def p'\<equiv>"p+e1/2"
- have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+ have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
apply (rule_tac x=p' in bexI)
by (auto simp add:pts_def)
@@ -3090,50 +3090,50 @@
"cball p r \<subseteq> ball p e1" and
pp_holo:"zp holomorphic_on cball p r" and
pp_po:"(\<forall>w\<in>cball p r. f w = zp w * (w - p) ^ zo \<and> zp w \<noteq> 0)"
- using zorder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding zo_def zp_def
+ using zorder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding zo_def zp_def
by auto
def e2\<equiv>"r/2"
- have "e2>0" using `r>0` unfolding e2_def by auto
+ have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
def anal\<equiv>"\<lambda>w. deriv zp w * h w / zp w" and prin\<equiv>"\<lambda>w. of_nat zo * h w / (w - p)"
have "((\<lambda>w. prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r \<subseteq> s"
using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
then have "cball p e2 \<subseteq> s"
- using `r>0` unfolding e2_def by auto
+ using \<open>r>0\<close> unfolding e2_def by auto
then have "(\<lambda>w. of_nat zo * h w) holomorphic_on cball p e2"
using h_holo
by (auto intro!: holomorphic_intros)
then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)"
using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. of_nat zo * h w"]
- `e2>0`
+ \<open>e2>0\<close>
unfolding prin_def
by (auto simp add: mult.assoc)
have "anal holomorphic_on ball p r" unfolding anal_def
- using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+ using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close>
by (auto intro!: holomorphic_intros)
then show "(anal has_contour_integral 0) (circlepath p e2)"
- using e2_def `r>0`
+ using e2_def \<open>r>0\<close>
by (auto elim!: Cauchy_theorem_disc_simple)
qed
then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
def wp\<equiv>"w-p"
have "wp\<noteq>0" and "zp w \<noteq>0"
- unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto
+ unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto
moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
proof (rule DERIV_imp_deriv)
def der\<equiv>"zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
- have po:"zo = Suc (zo - Suc 0) " using `zo>0` by auto
+ have po:"zo = Suc (zo - Suc 0) " using \<open>zo>0\<close> by auto
have "(zp has_field_derivative (deriv zp w)) (at w)"
- using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+ using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
holomorphic_on_imp_differentiable_at[of _ "ball p r"]
holomorphic_on_subset [OF pp_holo ball_subset_cball]
by (metis open_ball)
then show "(f' has_field_derivative der) (at w)"
- using `w\<noteq>p` `zo>0` unfolding der_def f'_def
+ using \<open>w\<noteq>p\<close> \<open>zo>0\<close> unfolding der_def f'_def
by (auto intro!: derivative_eq_intros simp add:field_simps)
qed
ultimately show "prin w + anal w = ff' w"
@@ -3147,7 +3147,7 @@
then have "cont_zero ff p e2" unfolding cont_zero_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
have "deriv f' w = deriv f w"
proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
@@ -3155,14 +3155,14 @@
next
have "ball p e1 - {p} \<subseteq> s - poles"
using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
- then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+ then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
using ball_subset_cball by blast
then show "f holomorphic_on ball p r - {p}" using f_holo
by auto
next
show "open (ball p r - {p})" by auto
next
- show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+ show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
next
fix x assume "x \<in> ball p r - {p}"
then show "f' x = f x"
@@ -3175,13 +3175,13 @@
qed
moreover have "cball p e2 \<subseteq> ball p e1"
using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
- ultimately show ?thesis using `e2>0` by auto
+ ultimately show ?thesis using \<open>e2>0\<close> by auto
qed
then obtain e3 where e3:"p\<in>zeros \<longrightarrow> e3>0 \<and> cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3"
by auto
def e4\<equiv>"if p\<in>poles then e2 else if p\<in>zeros then e3 else e1"
- have "e4>0" using e2 e3 `e1>0` unfolding e4_def by auto
- moreover have "avoid p e4" using e2 e3 `e1>0` e unfolding e4_def avoid_def by auto
+ have "e4>0" using e2 e3 \<open>e1>0\<close> unfolding e4_def by auto
+ moreover have "avoid p e4" using e2 e3 \<open>e1>0\<close> e unfolding e4_def avoid_def by auto
moreover have "p\<in>poles \<longrightarrow> cont_pole ff p e4" and "p\<in>zeros \<longrightarrow> cont_zero ff p e4"
by (auto simp add: e2 e3 e4_def pts_def zeros_def)
ultimately show ?thesis by auto
@@ -3193,17 +3193,17 @@
def w\<equiv>"\<lambda>p. winding_number g p"
have "contour_integral g ff = (\<Sum>p\<in>pts. w p * cont p)"
unfolding cont_def w_def
- proof (rule Cauchy_theorem_singularities[OF `open s` connected finite _ `valid_path g` loop
+ proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> connected finite _ \<open>valid_path g\<close> loop
path_img homo])
- have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] `open s` by auto
- then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo `poles \<subseteq> pts` h_holo
+ have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto
+ then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo \<open>poles \<subseteq> pts\<close> h_holo
by (auto intro!: holomorphic_intros simp add:pts_def)
next
show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))"
using get_e using avoid_def by blast
qed
also have "... = (\<Sum>p\<in>zeros. w p * cont p) + (\<Sum>p\<in>poles. w p * cont p)"
- using `finite pts` unfolding `pts=zeros \<union> poles`
+ using \<open>finite pts\<close> unfolding \<open>pts=zeros \<union> poles\<close>
apply (subst setsum.union_disjoint)
by (auto simp add:zeros_def)
also have "... = c * ((\<Sum>p\<in>zeros. w p * h p * zorder f p) - (\<Sum>p\<in>poles. w p * h p * porder f p))"
@@ -3216,7 +3216,7 @@
assume "p \<in> s"
have "cont p = c * h p * (zorder f p)" unfolding cont_def
apply (rule contour_integral_unique)
- using get_e `p\<in>s` `p\<in>zeros` unfolding cont_zero_def
+ using get_e \<open>p\<in>s\<close> \<open>p\<in>zeros\<close> unfolding cont_zero_def
by (metis mult.assoc mult.commute)
thus ?thesis by auto
next
@@ -3236,7 +3236,7 @@
assume "p \<in> s"
have "cont p = - c * h p * (porder f p)" unfolding cont_def
apply (rule contour_integral_unique)
- using get_e `p\<in>s` `p\<in>poles` unfolding cont_pole_def
+ using get_e \<open>p\<in>s\<close> \<open>p\<in>poles\<close> unfolding cont_pole_def
by (metis mult.assoc mult.commute)
thus ?thesis by auto
next
@@ -3259,7 +3259,7 @@
proof (rule differentiable_at_imp_differentiable_on)
fix x assume "x\<in>s"
obtain f' where "(f has_field_derivative f') (at x) "
- using holomorphic_on_imp_differentiable_at[OF f_holo `open s` `x\<in>s`]
+ using holomorphic_on_imp_differentiable_at[OF f_holo \<open>open s\<close> \<open>x\<in>s\<close>]
unfolding field_differentiable_def by auto
then have " (f has_derivative op * f') (at x)"
using has_field_derivative_imp_has_derivative[of f f' "at x"] by auto
@@ -3290,8 +3290,8 @@
proof -
have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z
proof -
- have "cmod (f z) > cmod (g z)" using `z\<in>path_image \<gamma>` path_less by auto
- moreover have "f z = - g z" using `f z + g z =0` by (simp add: eq_neg_iff_add_eq_0)
+ have "cmod (f z) > cmod (g z)" using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
+ moreover have "f z = - g z" using \<open>f z + g z =0\<close> by (simp add: eq_neg_iff_add_eq_0)
then have "cmod (f z) = cmod (g z)" by auto
ultimately show False by auto
qed
@@ -3301,8 +3301,8 @@
proof -
have False when "z\<in>path_image \<gamma>" and "f z =0" for z
proof -
- have "cmod (g z) < cmod (f z) " using `z\<in>path_image \<gamma>` path_less by auto
- then have "cmod (g z) < 0" using `f z=0` by auto
+ have "cmod (g z) < cmod (f z) " using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
+ then have "cmod (g z) < 0" using \<open>f z=0\<close> by auto
then show False by auto
qed
then show ?thesis unfolding zeros_f_def using path_img by auto
@@ -3312,7 +3312,7 @@
def h\<equiv>"\<lambda>p. g p / f p + 1"
obtain spikes
where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x"
- using `valid_path \<gamma>`
+ using \<open>valid_path \<gamma>\<close>
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
proof -
@@ -3334,12 +3334,12 @@
by auto
qed
have valid_h:"valid_path (h \<circ> \<gamma>)"
- proof (rule valid_path_compose_holomorphic[OF `valid_path \<gamma>` _ _ path_f])
+ proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f])
show "h holomorphic_on s - zeros_f"
unfolding h_def using f_holo g_holo
by (auto intro!: holomorphic_intros simp add:zeros_f_def)
next
- show "open (s - zeros_f)" using `finite zeros_f` `open s` finite_imp_closed
+ show "open (s - zeros_f)" using \<open>finite zeros_f\<close> \<open>open s\<close> finite_imp_closed
by auto
qed
have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)"
@@ -3362,7 +3362,7 @@
moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)"
when "x\<in>{0..1} - spikes" for x
proof (rule vector_derivative_chain_at_general)
- show "\<gamma> differentiable at x" using that `valid_path \<gamma>` spikes by auto
+ show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto
next
def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
def t\<equiv>"\<gamma> x"
@@ -3374,13 +3374,13 @@
unfolding h_def der_def using g_holo f_holo
apply (auto intro!: derivative_eq_intros)
by (auto simp add: DERIV_deriv_iff_field_differentiable
- holomorphic_on_imp_differentiable_at[OF _ `open s`])
+ holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
qed
then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>)
= ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
unfolding has_contour_integral
- apply (intro has_integral_spike_eq[OF negligible_finite, OF `finite spikes`])
+ apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>])
by auto
ultimately show ?thesis by auto
qed
@@ -3390,8 +3390,8 @@
+ contour_integral \<gamma> (\<lambda>p. deriv h p / h p)"
proof -
have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>"
- proof (rule contour_integrable_holomorphic_simple[OF _ _ `valid_path \<gamma>` path_f])
- show "open (s - zeros_f)" using finite_imp_closed[OF `finite zeros_f`] `open s`
+ proof (rule contour_integrable_holomorphic_simple[OF _ _ \<open>valid_path \<gamma>\<close> path_f])
+ show "open (s - zeros_f)" using finite_imp_closed[OF \<open>finite zeros_f\<close>] \<open>open s\<close>
by auto
then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f"
using f_holo
@@ -3420,23 +3420,23 @@
ultimately show False by auto
qed
have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def
- using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ `open s`] path_img that
+ using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>] path_img that
by (auto intro!: deriv_add)
have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)"
proof -
def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
have "p\<in>s" using path_img that by auto
then have "(h has_field_derivative der p) (at p)"
- unfolding h_def der_def using g_holo f_holo `f p\<noteq>0`
+ unfolding h_def der_def using g_holo f_holo \<open>f p\<noteq>0\<close>
apply (auto intro!: derivative_eq_intros)
by (auto simp add: DERIV_deriv_iff_field_differentiable
- holomorphic_on_imp_differentiable_at[OF _ `open s`])
+ holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
then show ?thesis unfolding der_def using DERIV_imp_deriv by auto
qed
show ?thesis
apply (simp only:der_fg der_h)
- apply (auto simp add:field_simps `h p\<noteq>0` `f p\<noteq>0` `fg p\<noteq>0`)
- by (auto simp add:field_simps h_def `f p\<noteq>0` fg_def)
+ apply (auto simp add:field_simps \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>)
+ by (auto simp add:field_simps h_def \<open>f p\<noteq>0\<close> fg_def)
qed
then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p)
= contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)"
@@ -3445,19 +3445,19 @@
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
unfolding c_def zeros_fg_def w_def
- proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+ proof (rule argument_principle[OF \<open>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def .
show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
- show " finite {p. fg p = 0}" using `finite zeros_fg` unfolding zeros_fg_def .
+ show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
unfolding c_def zeros_f_def w_def
- proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+ proof (rule argument_principle[OF \<open>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def .
show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
- show "finite {p. f p = 0}" using `finite zeros_f` unfolding zeros_f_def .
+ show "finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
qed
ultimately have "c * (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
by auto