1.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 03 23:01:39 2016 +0200
1.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 03 23:03:30 2016 +0200
1.3 @@ -2,7 +2,7 @@
1.4 Author: Andreas Lochbihler, ETH Zurich
1.5 *)
1.6
1.7 -section {* Formalisation of chain-complete partial orders, continuity and admissibility *}
1.8 +section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
1.9
1.10 theory Complete_Partial_Order2 imports
1.11 Main
1.12 @@ -83,10 +83,10 @@
1.13 fix x'
1.14 assume "x' \<in> (\<lambda>f. f x) ` Y"
1.15 then obtain f where "f \<in> Y" "x' = f x" by blast
1.16 - note `x' = f x` also
1.17 - from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD)
1.18 + note \<open>x' = f x\<close> also
1.19 + from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
1.20 also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
1.21 - by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`)
1.22 + by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
1.23 finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
1.24 qed
1.25 qed
1.26 @@ -108,9 +108,9 @@
1.27 fix x'
1.28 assume "x' \<in> f x ` Y"
1.29 then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
1.30 - also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD)
1.31 + also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
1.32 also have "\<dots> \<le> ?rhs" using chain'[OF y]
1.33 - by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`)
1.34 + by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
1.35 finally show "x' \<le> ?rhs" .
1.36 qed(rule x)
1.37
1.38 @@ -128,17 +128,17 @@
1.39 fix x'
1.40 assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
1.41 then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
1.42 - also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`]
1.43 + also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>]
1.44 proof(rule ccpo_Sup_least)
1.45 fix x
1.46 assume "x \<in> f y' ` Y"
1.47 then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
1.48 def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"
1.49 - from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
1.50 - hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y`
1.51 + from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
1.52 + hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
1.53 by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
1.54 - also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def)
1.55 - from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`)
1.56 + also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
1.57 + from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>)
1.58 finally show "x \<le> ?rhs" by(simp add: x)
1.59 qed
1.60 finally show "x' \<le> ?rhs" .
1.61 @@ -149,9 +149,9 @@
1.62 fix y
1.63 assume "y \<in> (\<lambda>x. f x x) ` Y"
1.64 then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
1.65 - also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)"
1.66 - by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`)
1.67 - also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`)
1.68 + also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
1.69 + by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
1.70 + also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
1.71 finally show "y \<le> ?lhs" .
1.72 qed
1.73 qed
1.74 @@ -171,8 +171,8 @@
1.75 fix x
1.76 assume "x \<in> f ` Y"
1.77 then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
1.78 - also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper)
1.79 - hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono)
1.80 + also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper)
1.81 + hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono)
1.82 finally show "x \<le> \<dots>" .
1.83 qed
1.84
1.85 @@ -196,14 +196,14 @@
1.86 fix f g
1.87 assume "f \<in> Z" "g \<in> Z"
1.88 and "fun_ord op \<le> f g"
1.89 - from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
1.90 + from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
1.91 proof(rule ccpo_Sup_least)
1.92 fix x
1.93 assume "x \<in> f ` Y"
1.94 then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
1.95 - also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def)
1.96 - also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`]
1.97 - by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
1.98 + also have "\<dots> \<le> g y" using \<open>fun_ord op \<le> f g\<close> by(simp add: fun_ord_def)
1.99 + also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>]
1.100 + by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
1.101 finally show "x \<le> \<Squnion>(g ` Y)" .
1.102 qed
1.103 qed
1.104 @@ -219,9 +219,9 @@
1.105 fix x'
1.106 assume "x' \<in> (\<lambda>f. f x) ` Z"
1.107 then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
1.108 - also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono])
1.109 + also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
1.110 also have "f y \<le> ?rhs" using chain3
1.111 - by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
1.112 + by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
1.113 finally show "x' \<le> ?rhs" .
1.114 qed
1.115 qed
1.116 @@ -231,14 +231,14 @@
1.117 fix x
1.118 assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
1.119 then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
1.120 - also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`]
1.121 + also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>]
1.122 proof(rule ccpo_Sup_least)
1.123 fix x'
1.124 assume "x' \<in> f ` Y"
1.125 then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
1.126 also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
1.127 - by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
1.128 - also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
1.129 + by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
1.130 + also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
1.131 finally show "x' \<le> ?rhs" .
1.132 qed
1.133 finally show "x \<le> ?rhs" .
1.134 @@ -254,10 +254,10 @@
1.135 fix x'
1.136 assume "x' \<in> (\<lambda>f. f y) ` Z"
1.137 then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
1.138 - also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`]
1.139 - by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
1.140 + also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
1.141 + by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
1.142 also have "\<dots> \<le> ?lhs" using chain2
1.143 - by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
1.144 + by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
1.145 finally show "x' \<le> ?lhs" .
1.146 qed
1.147 finally show "x \<le> ?lhs" .
1.148 @@ -314,9 +314,9 @@
1.149 assume "x' \<in> (\<lambda>f. f x) ` ?iter"
1.150 then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
1.151 also have "f x \<le> f y"
1.152 - by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+
1.153 + by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
1.154 also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
1.155 - by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
1.156 + by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
1.157 finally show "x' \<le> \<dots>" .
1.158 qed
1.159 qed
1.160 @@ -333,7 +333,7 @@
1.161 shows "monotone orda ordc (\<lambda>x. f x (t x))"
1.162 by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
1.163
1.164 -subsection {* Continuity *}
1.165 +subsection \<open>Continuity\<close>
1.166
1.167 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"
1.168 where
1.169 @@ -345,10 +345,10 @@
1.170 "mcont luba orda lubb ordb f \<longleftrightarrow>
1.171 monotone orda ordb f \<and> cont luba orda lubb ordb f"
1.172
1.173 -subsubsection {* Theorem collection @{text cont_intro} *}
1.174 +subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
1.175
1.176 named_theorems cont_intro "continuity and admissibility intro rules"
1.177 -ML {*
1.178 +ML \<open>
1.179 (* apply cont_intro rules as intro and try to solve
1.180 the remaining of the emerging subgoals with simp *)
1.181 fun cont_intro_tac ctxt =
1.182 @@ -374,13 +374,13 @@
1.183 end
1.184 handle THM _ => NONE
1.185 | TYPE _ => NONE
1.186 -*}
1.187 +\<close>
1.188
1.189 simproc_setup "cont_intro"
1.190 ( "ccpo.admissible lub ord P"
1.191 | "mcont lub ord lub' ord' f"
1.192 | "monotone ord ord' f"
1.193 - ) = {* K cont_intro_simproc *}
1.194 + ) = \<open>K cont_intro_simproc\<close>
1.195
1.196 lemmas [cont_intro] =
1.197 call_mono
1.198 @@ -604,10 +604,10 @@
1.199 fix x'
1.200 assume "x' \<in> (\<lambda>f. f x) ` ?iter"
1.201 then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
1.202 - also from _ `x \<sqsubseteq> y` have "f x \<le> f y"
1.203 - by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]])
1.204 + also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
1.205 + by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
1.206 also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
1.207 - by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
1.208 + by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
1.209 finally show "x' \<le> \<dots>" .
1.210 qed
1.211 next
1.212 @@ -783,7 +783,7 @@
1.213
1.214 end
1.215
1.216 -subsection {* Admissibility *}
1.217 +subsection \<open>Admissibility\<close>
1.218
1.219 lemma admissible_subst:
1.220 assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
1.221 @@ -860,10 +860,10 @@
1.222 fix x
1.223 assume "x \<in> f ` A"
1.224 then obtain y where "y \<in> A" "x = f y" by blast note this(2)
1.225 - also have "f y \<le> g y" using le `y \<in> A` by simp
1.226 + also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp
1.227 also have "Complete_Partial_Order.chain op \<le> (g ` A)"
1.228 using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
1.229 - hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`)
1.230 + hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>)
1.231 finally show "x \<le> \<dots>" .
1.232 qed
1.233 also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
1.234 @@ -992,7 +992,7 @@
1.235
1.236 end
1.237
1.238 -subsection {* @{term "op ="} as order *}
1.239 +subsection \<open>@{term "op ="} as order\<close>
1.240
1.241 definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
1.242 where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
1.243 @@ -1038,7 +1038,7 @@
1.244 \<Longrightarrow> mcont the_Sup op = lub ord f"
1.245 by(simp add: mcont_def cont_eqI monotone_eqI)
1.246
1.247 -subsection {* ccpo for products *}
1.248 +subsection \<open>ccpo for products\<close>
1.249
1.250 definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
1.251 where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
1.252 @@ -1197,7 +1197,7 @@
1.253 with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
1.254 moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
1.255 ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
1.256 - by(simp add: prod_lub_def `Y \<noteq> {}` lub_singleton_def)
1.257 + by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
1.258 qed
1.259
1.260 lemma cont_prodD2:
1.261 @@ -1253,9 +1253,9 @@
1.262 have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
1.263 by(simp add: prod_lub_def)
1.264 also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y)"
1.265 - by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] `Y \<noteq> {}`)
1.266 + by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] \<open>Y \<noteq> {}\<close>)
1.267 also from cont1 have "\<And>x. f (x, lubb (snd ` Y)) = \<Squnion>((\<lambda>y. f (x, y)) ` snd ` Y)"
1.268 - by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] `Y \<noteq> {}`)
1.269 + by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] \<open>Y \<noteq> {}\<close>)
1.270 hence "\<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y) = \<Squnion>((\<lambda>x. \<dots> x) ` fst ` Y)" by simp
1.271 also have "\<dots> = \<Squnion>((\<lambda>x. f (fst x, snd x)) ` Y)"
1.272 unfolding image_image split_def using chain
1.273 @@ -1330,7 +1330,7 @@
1.274 shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
1.275 by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
1.276
1.277 -subsection {* Complete lattices as ccpo *}
1.278 +subsection \<open>Complete lattices as ccpo\<close>
1.279
1.280 context complete_lattice begin
1.281
1.282 @@ -1374,8 +1374,8 @@
1.283 fix y
1.284 assume "y \<in> op \<squnion> x ` Y"
1.285 then obtain z where "y = x \<squnion> z" and "z \<in> Y" by blast
1.286 - from `z \<in> Y` have "z \<le> \<Squnion>Y" by(rule Sup_upper)
1.287 - with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding `y = x \<squnion> z` by(rule sup_mono) simp
1.288 + from \<open>z \<in> Y\<close> have "z \<le> \<Squnion>Y" by(rule Sup_upper)
1.289 + with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding \<open>y = x \<squnion> z\<close> by(rule sup_mono) simp
1.290 next
1.291 fix y
1.292 assume upper: "\<And>z. z \<in> op \<squnion> x ` Y \<Longrightarrow> z \<le> y"
1.293 @@ -1385,8 +1385,8 @@
1.294 assume "z \<in> insert x Y"
1.295 from assms obtain z' where "z' \<in> Y" by blast
1.296 let ?z = "if z \<in> Y then x \<squnion> z else x \<squnion> z'"
1.297 - have "z \<le> x \<squnion> ?z" using `z' \<in> Y` `z \<in> insert x Y` by auto
1.298 - also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: `z' \<in> Y`)
1.299 + have "z \<le> x \<squnion> ?z" using \<open>z' \<in> Y\<close> \<open>z \<in> insert x Y\<close> by auto
1.300 + also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: \<open>z' \<in> Y\<close>)
1.301 finally show "z \<le> y" .
1.302 qed
1.303 qed
1.304 @@ -1426,14 +1426,14 @@
1.305 interpretation lfp: partial_function_definitions "op \<le> :: _ :: complete_lattice \<Rightarrow> _" Sup
1.306 by(rule complete_lattice_partial_function_definitions)
1.307
1.308 -declaration {* Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
1.309 - @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE *}
1.310 +declaration \<open>Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
1.311 + @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
1.312
1.313 interpretation gfp: partial_function_definitions "op \<ge> :: _ :: complete_lattice \<Rightarrow> _" Inf
1.314 by(rule complete_lattice_partial_function_definitions_dual)
1.315
1.316 -declaration {* Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
1.317 - @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE *}
1.318 +declaration \<open>Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
1.319 + @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
1.320
1.321 lemma insert_mono [partial_function_mono]:
1.322 "monotone (fun_ord op \<subseteq>) op \<subseteq> A \<Longrightarrow> monotone (fun_ord op \<subseteq>) op \<subseteq> (\<lambda>y. insert x (A y))"
1.323 @@ -1505,23 +1505,23 @@
1.324 fix u
1.325 assume "u \<in> (\<lambda>x. g x z) ` Y"
1.326 then obtain y' where "u = g y' z" "y' \<in> Y" by auto
1.327 - from chain `y \<in> Y` `y' \<in> Y` have "ord y y' \<or> ord y' y" by(rule chainD)
1.328 + from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "ord y y' \<or> ord y' y" by(rule chainD)
1.329 thus "u \<le> ?rhs"
1.330 proof
1.331 - note `u = g y' z` also
1.332 + note \<open>u = g y' z\<close> also
1.333 assume "ord y y'"
1.334 with f have "f y \<subseteq> f y'" by(rule mcont_monoD)
1.335 - with `z \<in> f y`
1.336 + with \<open>z \<in> f y\<close>
1.337 have "g y' z \<le> \<Squnion>(g y' ` f y')" by(auto intro: Sup_upper)
1.338 - also have "\<dots> \<le> ?rhs" using `y' \<in> Y` by(auto intro: Sup_upper)
1.339 + also have "\<dots> \<le> ?rhs" using \<open>y' \<in> Y\<close> by(auto intro: Sup_upper)
1.340 finally show ?thesis .
1.341 next
1.342 - note `u = g y' z` also
1.343 + note \<open>u = g y' z\<close> also
1.344 assume "ord y' y"
1.345 with g have "g y' z \<le> g y z" by(rule mcont_monoD)
1.346 - also have "\<dots> \<le> \<Squnion>(g y ` f y)" using `z \<in> f y`
1.347 + also have "\<dots> \<le> \<Squnion>(g y ` f y)" using \<open>z \<in> f y\<close>
1.348 by(auto intro: Sup_upper)
1.349 - also have "\<dots> \<le> ?rhs" using `y \<in> Y` by(auto intro: Sup_upper)
1.350 + also have "\<dots> \<le> ?rhs" using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
1.351 finally show ?thesis .
1.352 qed
1.353 qed
1.354 @@ -1537,11 +1537,11 @@
1.355 fix u
1.356 assume "u \<in> g y ` f y"
1.357 then obtain z where "u = g y z" "z \<in> f y" by auto
1.358 - note `u = g y z`
1.359 + note \<open>u = g y z\<close>
1.360 also have "g y z \<le> \<Squnion>((\<lambda>x. g x z) ` Y)"
1.361 - using `y \<in> Y` by(auto intro: Sup_upper)
1.362 + using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
1.363 also have "\<dots> = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
1.364 - also have "\<dots> \<le> ?lhs" using `z \<in> f y` `y \<in> Y`
1.365 + also have "\<dots> \<le> ?lhs" using \<open>z \<in> f y\<close> \<open>y \<in> Y\<close>
1.366 by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
1.367 finally show "u \<le> ?lhs" .
1.368 qed
1.369 @@ -1567,7 +1567,7 @@
1.370 shows admissible_Bex: "ccpo.admissible Union op \<subseteq> (\<lambda>A. \<exists>x\<in>A. P x)"
1.371 by(rule ccpo.admissibleI)(auto)
1.372
1.373 -subsection {* Parallel fixpoint induction *}
1.374 +subsection \<open>Parallel fixpoint induction\<close>
1.375
1.376 context
1.377 fixes luba :: "'a set \<Rightarrow> 'a"