src/HOLCF/ConvexPD.thy

 (*  Title:      HOLCF/ConvexPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
 header {* Convex powerdomain *}
 

 unfolding convex_le_def by (fast intro: upper_le_refl lower_le_refl)
 
 lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
 unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
 
-interpretation convex_le: preorder [convex_le]
+interpretation convex_le!: preorder convex_le
 by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
 
 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
 unfolding convex_le_def Rep_PDUnit by simp
 

 lemma Rep_convex_principal:
   "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
 unfolding convex_principal_def
 by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
 
-interpretation convex_pd:
-  ideal_completion [convex_le pd_take convex_principal Rep_convex_pd]
+interpretation convex_pd!:
+  ideal_completion convex_le pd_take convex_principal Rep_convex_pd
 apply unfold_locales
 apply (rule pd_take_convex_le)
 apply (rule pd_take_idem)
 apply (erule pd_take_convex_mono)
 apply (rule pd_take_convex_chain)

 lemma convex_plus_absorb: "xs +\<natural> xs = xs"
 apply (induct xs rule: convex_pd.principal_induct, simp)
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
+interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
   by unfold_locales
     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
 
 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
 by (rule aci_convex_plus.mult_left_commute)