src/HOL/Library/Complete_Partial_Order2.thy
changeset 62837 237ef2bab6c7
parent 62652 7248d106c607
child 62858 d72a6f9ee690
     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"