src/HOL/HOLCF/UpperPD.thy

 (*  Title:      HOL/HOLCF/UpperPD.thy
     Author:     Brian Huffman
 *)
 
-section {* Upper powerdomain *}
+section \<open>Upper powerdomain\<close>
 
 theory UpperPD
 imports Compact_Basis
 begin
 
-subsection {* Basis preorder *}
+subsection \<open>Basis preorder\<close>
 
 definition
   upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where
   "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)"
 

 apply (simp add: 2)
 apply (simp add: upper_le_PDPlus_iff 3)
 done
 
 
-subsection {* Type definition *}
+subsection \<open>Type definition\<close>
 
 typedef 'a upper_pd  ("('(_')\<sharp>)") =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 

   ideal_completion upper_le upper_principal Rep_upper_pd
 using type_definition_upper_pd below_upper_pd_def
 using upper_principal_def pd_basis_countable
 by (rule upper_le.typedef_ideal_completion)
 
-text {* Upper powerdomain is pointed *}
+text \<open>Upper powerdomain is pointed\<close>
 
 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: upper_pd.principal_induct, simp, simp)
 
 instance upper_pd :: (bifinite) pcpo

 
 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
 by (rule upper_pd_minimal [THEN bottomI, symmetric])
 
 
-subsection {* Monadic unit and plus *}
+subsection \<open>Monadic unit and plus\<close>
 
 definition
   upper_unit :: "'a \<rightarrow> 'a upper_pd" where
   "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))"
 

 lemmas upper_plus_commute = upper_add.commute
 lemmas upper_plus_absorb = upper_add.idem
 lemmas upper_plus_left_commute = upper_add.left_commute
 lemmas upper_plus_left_absorb = upper_add.left_idem
 
-text {* Useful for @{text "simp add: upper_plus_ac"} *}
+text \<open>Useful for \<open>simp add: upper_plus_ac\<close>\<close>
 lemmas upper_plus_ac =
   upper_plus_assoc upper_plus_commute upper_plus_left_commute
 
-text {* Useful for @{text "simp only: upper_plus_aci"} *}
+text \<open>Useful for \<open>simp only: upper_plus_aci\<close>\<close>
 lemmas upper_plus_aci =
   upper_plus_ac upper_plus_absorb upper_plus_left_absorb
 
 lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs"
 apply (induct xs rule: upper_pd.principal_induct, simp)

 lemma compact_upper_plus [simp]:
   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)"
 by (auto dest!: upper_pd.compact_imp_principal)
 
 
-subsection {* Induction rules *}
+subsection \<open>Induction rules\<close>
 
 lemma upper_pd_induct1:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<sharp>"
   assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"

 apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
 apply (simp only: upper_plus_principal [symmetric] plus)
 done
 
 
-subsection {* Monadic bind *}
+subsection \<open>Monadic bind\<close>
 
 definition
   upper_bind_basis ::
   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   "upper_bind_basis = fold_pd

 lemma upper_bind_bind:
   "upper_bind\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>g = upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_bind\<cdot>(f\<cdot>x)\<cdot>g)"
 by (induct xs, simp_all)
 
 
-subsection {* Map *}
+subsection \<open>Map\<close>
 
 definition
   upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
   "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))"
 

     done
   thus "finite {xs. upper_map\<cdot>d\<cdot>xs = xs}"
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Upper powerdomain is bifinite *}
+subsection \<open>Upper powerdomain is bifinite\<close>
 
 lemma approx_chain_upper_map:
   assumes "approx_chain a"
   shows "approx_chain (\<lambda>i. upper_map\<cdot>(a i))"
   using assms unfolding approx_chain_def

   show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a"
     using bifinite [where 'a='a]
     by (fast intro!: approx_chain_upper_map)
 qed
 
-subsection {* Join *}
+subsection \<open>Join\<close>
 
 definition
   upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"