src/HOLCF/Bifinite.thy
changeset 26962 c8b20f615d6c
parent 26407 562a1d615336
child 27186 416d66c36d8f
--- a/src/HOLCF/Bifinite.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Bifinite.thy	Mon May 19 23:49:20 2008 +0200
@@ -11,17 +11,14 @@
 
 subsection {* Omega-profinite and bifinite domains *}
 
-axclass approx < cpo
-
-consts approx :: "nat \<Rightarrow> 'a::approx \<rightarrow> 'a"
+class profinite = cpo +
+  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
+  assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
+  assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
+  assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+  assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
 
-axclass profinite < approx
-  chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
-  lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
-  approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
-  finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
-
-axclass bifinite < profinite, pcpo
+class bifinite = profinite + pcpo
 
 lemma finite_range_imp_finite_fixes:
   "finite {x. \<exists>y. x = f y} \<Longrightarrow> finite {x. f x = x}"
@@ -178,13 +175,14 @@
  apply clarsimp
 done
 
-instance "->" :: (profinite, profinite) approx ..
+instantiation "->" :: (profinite, profinite) profinite
+begin
 
-defs (overloaded)
+definition
   approx_cfun_def:
-    "approx \<equiv> \<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
+    "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
 
-instance "->" :: (profinite, profinite) profinite
+instance
  apply (intro_classes, unfold approx_cfun_def)
     apply simp
    apply (simp add: lub_distribs eta_cfun)
@@ -194,6 +192,8 @@
  apply (intro finite_range_lemma finite_approx)
 done
 
+end
+
 instance "->" :: (profinite, bifinite) bifinite ..
 
 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"