src/HOL/HOLCF/LowerPD.thy

 
 subsection {* Monadic unit and plus *}
 
 definition
   lower_unit :: "'a \<rightarrow> 'a lower_pd" where
-  "lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
+  "lower_unit = compact_basis.extension (\<lambda>a. lower_principal (PDUnit a))"
 
 definition
   lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
-  "lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
+  "lower_plus = lower_pd.extension (\<lambda>t. lower_pd.extension (\<lambda>u.
       lower_principal (PDPlus t u)))"
 
 abbreviation
   lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
     (infixl "+\<flat>" 65) where

   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
 
 lemma lower_unit_Rep_compact_basis [simp]:
   "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
 unfolding lower_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_lower_mono)
+by (simp add: compact_basis.extension_principal PDUnit_lower_mono)
 
 lemma lower_plus_principal [simp]:
   "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
 unfolding lower_plus_def
-by (simp add: lower_pd.basis_fun_principal
-    lower_pd.basis_fun_mono PDPlus_lower_mono)
+by (simp add: lower_pd.extension_principal
+    lower_pd.extension_mono PDPlus_lower_mono)
 
 interpretation lower_add: semilattice lower_add proof
   fix xs ys zs :: "'a lower_pd"
   show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
     apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)

 apply simp
 done
 
 definition
   lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
-  "lower_bind = lower_pd.basis_fun lower_bind_basis"
+  "lower_bind = lower_pd.extension lower_bind_basis"
 
 syntax
   "_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
     ("(3\<Union>\<flat>_\<in>_./ _)" [0, 0, 10] 10)
 

   "\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
 
 lemma lower_bind_principal [simp]:
   "lower_bind\<cdot>(lower_principal t) = lower_bind_basis t"
 unfolding lower_bind_def
-apply (rule lower_pd.basis_fun_principal)
+apply (rule lower_pd.extension_principal)
 apply (erule lower_bind_basis_mono)
 done
 
 lemma lower_bind_unit [simp]:
   "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"