use new class package for classes profinite, bifinite; remove approx class
authorhuffman
Mon May 19 23:49:20 2008 +0200 (2008-05-19)
changeset 26962c8b20f615d6c
parent 26961 290e1571c829
child 26963 290d23780204
use new class package for classes profinite, bifinite; remove approx class
src/HOLCF/Bifinite.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cprod.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Sun May 18 17:04:48 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Mon May 19 23:49:20 2008 +0200
     1.3 @@ -11,17 +11,14 @@
     1.4  
     1.5  subsection {* Omega-profinite and bifinite domains *}
     1.6  
     1.7 -axclass approx < cpo
     1.8 -
     1.9 -consts approx :: "nat \<Rightarrow> 'a::approx \<rightarrow> 'a"
    1.10 +class profinite = cpo +
    1.11 +  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
    1.12 +  assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
    1.13 +  assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
    1.14 +  assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.15 +  assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
    1.16  
    1.17 -axclass profinite < approx
    1.18 -  chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
    1.19 -  lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
    1.20 -  approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.21 -  finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
    1.22 -
    1.23 -axclass bifinite < profinite, pcpo
    1.24 +class bifinite = profinite + pcpo
    1.25  
    1.26  lemma finite_range_imp_finite_fixes:
    1.27    "finite {x. \<exists>y. x = f y} \<Longrightarrow> finite {x. f x = x}"
    1.28 @@ -178,13 +175,14 @@
    1.29   apply clarsimp
    1.30  done
    1.31  
    1.32 -instance "->" :: (profinite, profinite) approx ..
    1.33 +instantiation "->" :: (profinite, profinite) profinite
    1.34 +begin
    1.35  
    1.36 -defs (overloaded)
    1.37 +definition
    1.38    approx_cfun_def:
    1.39 -    "approx \<equiv> \<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
    1.40 +    "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
    1.41  
    1.42 -instance "->" :: (profinite, profinite) profinite
    1.43 +instance
    1.44   apply (intro_classes, unfold approx_cfun_def)
    1.45      apply simp
    1.46     apply (simp add: lub_distribs eta_cfun)
    1.47 @@ -194,6 +192,8 @@
    1.48   apply (intro finite_range_lemma finite_approx)
    1.49  done
    1.50  
    1.51 +end
    1.52 +
    1.53  instance "->" :: (profinite, bifinite) bifinite ..
    1.54  
    1.55  lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
     2.1 --- a/src/HOLCF/ConvexPD.thy	Sun May 18 17:04:48 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Mon May 19 23:49:20 2008 +0200
     2.3 @@ -206,12 +206,13 @@
     2.4  
     2.5  subsection {* Approximation *}
     2.6  
     2.7 -instance convex_pd :: (profinite) approx ..
     2.8 +instantiation convex_pd :: (profinite) profinite
     2.9 +begin
    2.10  
    2.11 -defs (overloaded)
    2.12 -  approx_convex_pd_def: "approx \<equiv> convex_pd.completion_approx"
    2.13 +definition
    2.14 +  approx_convex_pd_def: "approx = convex_pd.completion_approx"
    2.15  
    2.16 -instance convex_pd :: (profinite) profinite
    2.17 +instance
    2.18  apply (intro_classes, unfold approx_convex_pd_def)
    2.19  apply (simp add: convex_pd.chain_completion_approx)
    2.20  apply (rule convex_pd.lub_completion_approx)
    2.21 @@ -219,6 +220,8 @@
    2.22  apply (rule convex_pd.finite_fixes_completion_approx)
    2.23  done
    2.24  
    2.25 +end
    2.26 +
    2.27  instance convex_pd :: (bifinite) bifinite ..
    2.28  
    2.29  lemma approx_convex_principal [simp]:
     3.1 --- a/src/HOLCF/Cprod.thy	Sun May 18 17:04:48 2008 +0200
     3.2 +++ b/src/HOLCF/Cprod.thy	Mon May 19 23:49:20 2008 +0200
     3.3 @@ -342,14 +342,14 @@
     3.4  
     3.5  subsection {* Product type is a bifinite domain *}
     3.6  
     3.7 -instance "*" :: (profinite, profinite) approx ..
     3.8 +instantiation "*" :: (profinite, profinite) profinite
     3.9 +begin
    3.10  
    3.11 -defs (overloaded)
    3.12 +definition
    3.13    approx_cprod_def:
    3.14 -    "approx \<equiv> \<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>"
    3.15 +    "approx = (\<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>)"
    3.16  
    3.17 -instance "*" :: (profinite, profinite) profinite
    3.18 -proof
    3.19 +instance proof
    3.20    fix i :: nat and x :: "'a \<times> 'b"
    3.21    show "chain (\<lambda>i. approx i\<cdot>x)"
    3.22      unfolding approx_cprod_def by simp
    3.23 @@ -367,6 +367,8 @@
    3.24          intro finite_cartesian_product finite_fixes_approx)
    3.25  qed
    3.26  
    3.27 +end
    3.28 +
    3.29  instance "*" :: (bifinite, bifinite) bifinite ..
    3.30  
    3.31  lemma approx_cpair [simp]:
     4.1 --- a/src/HOLCF/LowerPD.thy	Sun May 18 17:04:48 2008 +0200
     4.2 +++ b/src/HOLCF/LowerPD.thy	Mon May 19 23:49:20 2008 +0200
     4.3 @@ -158,12 +158,13 @@
     4.4  
     4.5  subsection {* Approximation *}
     4.6  
     4.7 -instance lower_pd :: (profinite) approx ..
     4.8 +instantiation lower_pd :: (profinite) profinite
     4.9 +begin
    4.10  
    4.11 -defs (overloaded)
    4.12 -  approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx"
    4.13 +definition
    4.14 +  approx_lower_pd_def: "approx = lower_pd.completion_approx"
    4.15  
    4.16 -instance lower_pd :: (profinite) profinite
    4.17 +instance
    4.18  apply (intro_classes, unfold approx_lower_pd_def)
    4.19  apply (simp add: lower_pd.chain_completion_approx)
    4.20  apply (rule lower_pd.lub_completion_approx)
    4.21 @@ -171,6 +172,8 @@
    4.22  apply (rule lower_pd.finite_fixes_completion_approx)
    4.23  done
    4.24  
    4.25 +end
    4.26 +
    4.27  instance lower_pd :: (bifinite) bifinite ..
    4.28  
    4.29  lemma approx_lower_principal [simp]:
     5.1 --- a/src/HOLCF/Sprod.thy	Sun May 18 17:04:48 2008 +0200
     5.2 +++ b/src/HOLCF/Sprod.thy	Mon May 19 23:49:20 2008 +0200
     5.3 @@ -230,14 +230,14 @@
     5.4  
     5.5  subsection {* Strict product is a bifinite domain *}
     5.6  
     5.7 -instance "**" :: (bifinite, bifinite) approx ..
     5.8 +instantiation "**" :: (bifinite, bifinite) bifinite
     5.9 +begin
    5.10  
    5.11 -defs (overloaded)
    5.12 +definition
    5.13    approx_sprod_def:
    5.14 -    "approx \<equiv> \<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:)"
    5.15 +    "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
    5.16  
    5.17 -instance "**" :: (bifinite, bifinite) bifinite
    5.18 -proof
    5.19 +instance proof
    5.20    fix i :: nat and x :: "'a \<otimes> 'b"
    5.21    show "chain (\<lambda>i. approx i\<cdot>x)"
    5.22      unfolding approx_sprod_def by simp
    5.23 @@ -259,6 +259,8 @@
    5.24      by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
    5.25  qed
    5.26  
    5.27 +end
    5.28 +
    5.29  lemma approx_spair [simp]:
    5.30    "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
    5.31  unfolding approx_sprod_def
     6.1 --- a/src/HOLCF/Ssum.thy	Sun May 18 17:04:48 2008 +0200
     6.2 +++ b/src/HOLCF/Ssum.thy	Mon May 19 23:49:20 2008 +0200
     6.3 @@ -216,11 +216,12 @@
     6.4  
     6.5  subsection {* Strict sum is a bifinite domain *}
     6.6  
     6.7 -instance "++" :: (bifinite, bifinite) approx ..
     6.8 +instantiation "++" :: (bifinite, bifinite) bifinite
     6.9 +begin
    6.10  
    6.11 -defs (overloaded)
    6.12 +definition
    6.13    approx_ssum_def:
    6.14 -    "approx \<equiv> \<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y))"
    6.15 +    "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
    6.16  
    6.17  lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
    6.18  unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
    6.19 @@ -228,8 +229,7 @@
    6.20  lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
    6.21  unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
    6.22  
    6.23 -instance "++" :: (bifinite, bifinite) bifinite
    6.24 -proof
    6.25 +instance proof
    6.26    fix i :: nat and x :: "'a \<oplus> 'b"
    6.27    show "chain (\<lambda>i. approx i\<cdot>x)"
    6.28      unfolding approx_ssum_def by simp
    6.29 @@ -248,3 +248,5 @@
    6.30  qed
    6.31  
    6.32  end
    6.33 +
    6.34 +end
     7.1 --- a/src/HOLCF/Up.thy	Sun May 18 17:04:48 2008 +0200
     7.2 +++ b/src/HOLCF/Up.thy	Mon May 19 23:49:20 2008 +0200
     7.3 @@ -311,14 +311,14 @@
     7.4  
     7.5  subsection {* Lifted cpo is a bifinite domain *}
     7.6  
     7.7 -instance u :: (profinite) approx ..
     7.8 +instantiation u :: (profinite) bifinite
     7.9 +begin
    7.10  
    7.11 -defs (overloaded)
    7.12 +definition
    7.13    approx_up_def:
    7.14 -    "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
    7.15 +    "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
    7.16  
    7.17 -instance u :: (profinite) bifinite
    7.18 -proof
    7.19 +instance proof
    7.20    fix i :: nat and x :: "'a u"
    7.21    show "chain (\<lambda>i. approx i\<cdot>x)"
    7.22      unfolding approx_up_def by simp
    7.23 @@ -336,6 +336,8 @@
    7.24      by (rule finite_subset, simp add: finite_fixes_approx)
    7.25  qed
    7.26  
    7.27 +end
    7.28 +
    7.29  lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
    7.30  unfolding approx_up_def by simp
    7.31  
     8.1 --- a/src/HOLCF/UpperPD.thy	Sun May 18 17:04:48 2008 +0200
     8.2 +++ b/src/HOLCF/UpperPD.thy	Mon May 19 23:49:20 2008 +0200
     8.3 @@ -156,12 +156,13 @@
     8.4  
     8.5  subsection {* Approximation *}
     8.6  
     8.7 -instance upper_pd :: (profinite) approx ..
     8.8 +instantiation upper_pd :: (profinite) profinite
     8.9 +begin
    8.10  
    8.11 -defs (overloaded)
    8.12 -  approx_upper_pd_def: "approx \<equiv> upper_pd.completion_approx"
    8.13 +definition
    8.14 +  approx_upper_pd_def: "approx = upper_pd.completion_approx"
    8.15  
    8.16 -instance upper_pd :: (profinite) profinite
    8.17 +instance
    8.18  apply (intro_classes, unfold approx_upper_pd_def)
    8.19  apply (simp add: upper_pd.chain_completion_approx)
    8.20  apply (rule upper_pd.lub_completion_approx)
    8.21 @@ -169,6 +170,8 @@
    8.22  apply (rule upper_pd.finite_fixes_completion_approx)
    8.23  done
    8.24  
    8.25 +end
    8.26 +
    8.27  instance upper_pd :: (bifinite) bifinite ..
    8.28  
    8.29  lemma approx_upper_principal [simp]: