# HG changeset patch
# User huffman
# Date 1211233760 -7200
# Node ID c8b20f615d6cebc20fd79c66f7d821f74fa90a2f
# Parent  290e1571c82946ff1ea6798985396abfc55824e0
use new class package for classes profinite, bifinite; remove approx class

diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Bifinite.thy
--- 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))"
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Mon May 19 23:49:20 2008 +0200
@@ -206,12 +206,13 @@
 
 subsection {* Approximation *}
 
-instance convex_pd :: (profinite) approx ..
+instantiation convex_pd :: (profinite) profinite
+begin
 
-defs (overloaded)
-  approx_convex_pd_def: "approx \<equiv> convex_pd.completion_approx"
+definition
+  approx_convex_pd_def: "approx = convex_pd.completion_approx"
 
-instance convex_pd :: (profinite) profinite
+instance
 apply (intro_classes, unfold approx_convex_pd_def)
 apply (simp add: convex_pd.chain_completion_approx)
 apply (rule convex_pd.lub_completion_approx)
@@ -219,6 +220,8 @@
 apply (rule convex_pd.finite_fixes_completion_approx)
 done
 
+end
+
 instance convex_pd :: (bifinite) bifinite ..
 
 lemma approx_convex_principal [simp]:
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Cprod.thy	Mon May 19 23:49:20 2008 +0200
@@ -342,14 +342,14 @@
 
 subsection {* Product type is a bifinite domain *}
 
-instance "*" :: (profinite, profinite) approx ..
+instantiation "*" :: (profinite, profinite) profinite
+begin
 
-defs (overloaded)
+definition
   approx_cprod_def:
-    "approx \<equiv> \<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>"
+    "approx = (\<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>)"
 
-instance "*" :: (profinite, profinite) profinite
-proof
+instance proof
   fix i :: nat and x :: "'a \<times> 'b"
   show "chain (\<lambda>i. approx i\<cdot>x)"
     unfolding approx_cprod_def by simp
@@ -367,6 +367,8 @@
         intro finite_cartesian_product finite_fixes_approx)
 qed
 
+end
+
 instance "*" :: (bifinite, bifinite) bifinite ..
 
 lemma approx_cpair [simp]:
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Mon May 19 23:49:20 2008 +0200
@@ -158,12 +158,13 @@
 
 subsection {* Approximation *}
 
-instance lower_pd :: (profinite) approx ..
+instantiation lower_pd :: (profinite) profinite
+begin
 
-defs (overloaded)
-  approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx"
+definition
+  approx_lower_pd_def: "approx = lower_pd.completion_approx"
 
-instance lower_pd :: (profinite) profinite
+instance
 apply (intro_classes, unfold approx_lower_pd_def)
 apply (simp add: lower_pd.chain_completion_approx)
 apply (rule lower_pd.lub_completion_approx)
@@ -171,6 +172,8 @@
 apply (rule lower_pd.finite_fixes_completion_approx)
 done
 
+end
+
 instance lower_pd :: (bifinite) bifinite ..
 
 lemma approx_lower_principal [simp]:
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Sprod.thy	Mon May 19 23:49:20 2008 +0200
@@ -230,14 +230,14 @@
 
 subsection {* Strict product is a bifinite domain *}
 
-instance "**" :: (bifinite, bifinite) approx ..
+instantiation "**" :: (bifinite, bifinite) bifinite
+begin
 
-defs (overloaded)
+definition
   approx_sprod_def:
-    "approx \<equiv> \<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:)"
+    "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
 
-instance "**" :: (bifinite, bifinite) bifinite
-proof
+instance proof
   fix i :: nat and x :: "'a \<otimes> 'b"
   show "chain (\<lambda>i. approx i\<cdot>x)"
     unfolding approx_sprod_def by simp
@@ -259,6 +259,8 @@
     by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
 qed
 
+end
+
 lemma approx_spair [simp]:
   "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
 unfolding approx_sprod_def
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Ssum.thy	Mon May 19 23:49:20 2008 +0200
@@ -216,11 +216,12 @@
 
 subsection {* Strict sum is a bifinite domain *}
 
-instance "++" :: (bifinite, bifinite) approx ..
+instantiation "++" :: (bifinite, bifinite) bifinite
+begin
 
-defs (overloaded)
+definition
   approx_ssum_def:
-    "approx \<equiv> \<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y))"
+    "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
 
 lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
@@ -228,8 +229,7 @@
 lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
 
-instance "++" :: (bifinite, bifinite) bifinite
-proof
+instance proof
   fix i :: nat and x :: "'a \<oplus> 'b"
   show "chain (\<lambda>i. approx i\<cdot>x)"
     unfolding approx_ssum_def by simp
@@ -248,3 +248,5 @@
 qed
 
 end
+
+end
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Up.thy	Mon May 19 23:49:20 2008 +0200
@@ -311,14 +311,14 @@
 
 subsection {* Lifted cpo is a bifinite domain *}
 
-instance u :: (profinite) approx ..
+instantiation u :: (profinite) bifinite
+begin
 
-defs (overloaded)
+definition
   approx_up_def:
-    "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
+    "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
 
-instance u :: (profinite) bifinite
-proof
+instance proof
   fix i :: nat and x :: "'a u"
   show "chain (\<lambda>i. approx i\<cdot>x)"
     unfolding approx_up_def by simp
@@ -336,6 +336,8 @@
     by (rule finite_subset, simp add: finite_fixes_approx)
 qed
 
+end
+
 lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
 unfolding approx_up_def by simp
 
diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Mon May 19 23:49:20 2008 +0200
@@ -156,12 +156,13 @@
 
 subsection {* Approximation *}
 
-instance upper_pd :: (profinite) approx ..
+instantiation upper_pd :: (profinite) profinite
+begin
 
-defs (overloaded)
-  approx_upper_pd_def: "approx \<equiv> upper_pd.completion_approx"
+definition
+  approx_upper_pd_def: "approx = upper_pd.completion_approx"
 
-instance upper_pd :: (profinite) profinite
+instance
 apply (intro_classes, unfold approx_upper_pd_def)
 apply (simp add: upper_pd.chain_completion_approx)
 apply (rule upper_pd.lub_completion_approx)
@@ -169,6 +170,8 @@
 apply (rule upper_pd.finite_fixes_completion_approx)
 done
 
+end
+
 instance upper_pd :: (bifinite) bifinite ..
 
 lemma approx_upper_principal [simp]: