src/HOL/HOLCF/Pcpo.thy

 (*  Title:      HOL/HOLCF/Pcpo.thy
     Author:     Franz Regensburger
 *)
 
-section {* Classes cpo and pcpo *}
+section \<open>Classes cpo and pcpo\<close>
 
 theory Pcpo
 imports Porder
 begin
 
-subsection {* Complete partial orders *}
-
-text {* The class cpo of chain complete partial orders *}
+subsection \<open>Complete partial orders\<close>
+
+text \<open>The class cpo of chain complete partial orders\<close>
 
 class cpo = po +
   assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
 begin
 
-text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
+text \<open>in cpo's everthing equal to THE lub has lub properties for every chain\<close>
 
 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
   by (fast dest: cpo elim: is_lub_lub)
 
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
   by (blast dest: cpo intro: is_lub_lub)
 
-text {* Properties of the lub *}
+text \<open>Properties of the lub\<close>
 
 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
   by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
 
 lemma is_lub_thelub:

 apply (fast elim!: chain_mono)
 apply (drule sym)
 apply (force elim!: is_ub_thelub)
 done
 
-text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
+text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close>
 
 lemma lub_mono:
   "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
 by (fast elim: lub_below below_lub)
 
-text {* the = relation between two chains is preserved by their lubs *}
+text \<open>the = relation between two chains is preserved by their lubs\<close>
 
 lemma lub_eq:
   "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
   by simp
 

   shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)"
   by (simp add: diag_lub 1 2)
 
 end
 
-subsection {* Pointed cpos *}
-
-text {* The class pcpo of pointed cpos *}
+subsection \<open>Pointed cpos\<close>
+
+text \<open>The class pcpo of pointed cpos\<close>
 
 class pcpo = cpo +
   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
 begin
 

 apply simp
 done
 
 end
 
-text {* Old "UU" syntax: *}
+text \<open>Old "UU" syntax:\<close>
 
 syntax UU :: logic
 
 translations "UU" => "CONST bottom"
 
-text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
-
-setup {*
+text \<open>Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}.\<close>
+
+setup \<open>
   Reorient_Proc.add
     (fn Const(@{const_name bottom}, _) => true | _ => false)
-*}
+\<close>
 
 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
 
-text {* useful lemmas about @{term \<bottom>} *}
+text \<open>useful lemmas about @{term \<bottom>}\<close>
 
 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
 by (simp add: po_eq_conv)
 
 lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"

 by (subst eq_bottom_iff)
 
 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
 by (simp only: eq_bottom_iff lub_below_iff)
 
-subsection {* Chain-finite and flat cpos *}
-
-text {* further useful classes for HOLCF domains *}
+subsection \<open>Chain-finite and flat cpos\<close>
+
+text \<open>further useful classes for HOLCF domains\<close>
 
 class chfin = po +
   assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
 begin
 

 lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
   by (safe dest!: ax_flat)
 
 end
 
-subsection {* Discrete cpos *}
+subsection \<open>Discrete cpos\<close>
 
 class discrete_cpo = below +
   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
 begin
 
 subclass po
 proof qed simp_all
 
-text {* In a discrete cpo, every chain is constant *}
+text \<open>In a discrete cpo, every chain is constant\<close>
 
 lemma discrete_chain_const:
   assumes S: "chain S"
   shows "\<exists>x. S = (\<lambda>i. x)"
 proof (intro exI ext)