src/HOL/HOLCF/Compact_Basis.thy

 (*  Title:      HOL/HOLCF/Compact_Basis.thy
     Author:     Brian Huffman
 *)
 
-section {* A compact basis for powerdomains *}
+section \<open>A compact basis for powerdomains\<close>
 
 theory Compact_Basis
 imports Universal
 begin
 
 default_sort bifinite
 
-subsection {* A compact basis for powerdomains *}
+subsection \<open>A compact basis for powerdomains\<close>
 
 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
 
 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
   unfolding pd_basis_def

 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
 
 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
 
-text {* The powerdomain basis type is countable. *}
+text \<open>The powerdomain basis type is countable.\<close>
 
 lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
 proof -
   obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
     using compact_basis.countable ..

     by (simp add: inj_on_def set_encode_eq image_g_eq Rep_pd_basis_inject)
   thus ?thesis by - (rule exI)
   (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
 qed
 
-subsection {* Unit and plus constructors *}
+subsection \<open>Unit and plus constructors\<close>
 
 definition
   PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
   "PDUnit = (\<lambda>x. Abs_pd_basis {x})"
 

   shows "P x"
 apply (induct x rule: pd_basis_induct1)
 apply (rule PDUnit, erule PDPlus [OF PDUnit])
 done
 
-subsection {* Fold operator *}
+subsection \<open>Fold operator\<close>
 
 definition
   fold_pd ::
     "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   where "fold_pd g f t = semilattice_set.F f (g ` Rep_pd_basis t)"