src/HOL/HOLCF/Bifinite.thy

 (*  Title:      HOL/HOLCF/Bifinite.thy
     Author:     Brian Huffman
 *)
 
-section {* Profinite and bifinite cpos *}
+section \<open>Profinite and bifinite cpos\<close>
 
 theory Bifinite
 imports Map_Functions "~~/src/HOL/Library/Countable"
 begin
 
 default_sort cpo
 
-subsection {* Chains of finite deflations *}
+subsection \<open>Chains of finite deflations\<close>
 
 locale approx_chain =
   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
   assumes chain_approx [simp]: "chain (\<lambda>i. approx i)"
   assumes lub_approx [simp]: "(\<Squnion>i. approx i) = ID"

 lemma compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
 by (rule admD2, simp_all)
 
 end
 
-subsection {* Omega-profinite and bifinite domains *}
+subsection \<open>Omega-profinite and bifinite domains\<close>
 
 class bifinite = pcpo +
   assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
 
 class profinite = cpo +
   assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
 
-subsection {* Building approx chains *}
+subsection \<open>Building approx chains\<close>
 
 lemma approx_chain_iso:
   assumes a: "approx_chain a"
   assumes [simp]: "\<And>x. f\<cdot>(g\<cdot>x) = x"
   assumes [simp]: "\<And>y. g\<cdot>(f\<cdot>y) = y"

   assumes "approx_chain a" and "approx_chain b"
   shows "approx_chain (\<lambda>i. prod_map\<cdot>(a i)\<cdot>(b i))"
   using assms unfolding approx_chain_def
   by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
 
-text {* Approx chains for countable discrete types. *}
+text \<open>Approx chains for countable discrete types.\<close>
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
 
 lemma chain_discr_approx [simp]: "chain discr_approx"

 
 lemma discr_approx: "approx_chain discr_approx"
 using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
 by (rule approx_chain.intro)
 
-subsection {* Class instance proofs *}
+subsection \<open>Class instance proofs\<close>
 
 instance bifinite \<subseteq> profinite
 proof
   show "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
     using bifinite [where 'a='a]

 qed
 
 instance u :: (profinite) bifinite
   by standard (rule profinite)
 
-text {*
+text \<open>
   Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
-*}
+\<close>
 
 definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
 
 definition "decode_cfun = (\<Lambda> g x. sfun_rep\<cdot>g\<cdot>(up\<cdot>x))"
 

     using a b by (simp add: approx_chain_iso approx_chain_sfun_map)
   thus "\<exists>(a::nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b)). approx_chain a"
     by - (rule exI)
 qed
 
-text {*
+text \<open>
   Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
-*}
+\<close>
 
 definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
 
 definition "decode_prod_u = (\<Lambda>(:up\<cdot>x, up\<cdot>y:). up\<cdot>(x, y))"