--- 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))"
--- 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]:
--- 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]:
--- 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]:
--- 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
--- 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
--- 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
--- 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]: