powerdomain theories require class 'bifinite' instead of 'domain'
authorhuffman
Sun Dec 19 06:39:19 2010 -0800 (2010-12-19)
changeset 41288a19edebad961
parent 41287 029a6fc1bfb8
child 41289 f655912ac235
powerdomain theories require class 'bifinite' instead of 'domain'
src/HOL/HOLCF/Compact_Basis.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/UpperPD.thy
     1.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:34:41 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Sun Dec 19 06:39:19 2010 -0800
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Representable
     1.5  begin
     1.6  
     1.7 -default_sort "domain"
     1.8 +default_sort bifinite
     1.9  
    1.10  subsection {* A compact basis for powerdomains *}
    1.11  
     2.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:34:41 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Dec 19 06:39:19 2010 -0800
     2.3 @@ -125,7 +125,7 @@
     2.4  
     2.5  type_notation (xsymbols) convex_pd ("('(_')\<natural>)")
     2.6  
     2.7 -instantiation convex_pd :: ("domain") below
     2.8 +instantiation convex_pd :: (bifinite) below
     2.9  begin
    2.10  
    2.11  definition
    2.12 @@ -134,11 +134,11 @@
    2.13  instance ..
    2.14  end
    2.15  
    2.16 -instance convex_pd :: ("domain") po
    2.17 +instance convex_pd :: (bifinite) po
    2.18  using type_definition_convex_pd below_convex_pd_def
    2.19  by (rule convex_le.typedef_ideal_po)
    2.20  
    2.21 -instance convex_pd :: ("domain") cpo
    2.22 +instance convex_pd :: (bifinite) cpo
    2.23  using type_definition_convex_pd below_convex_pd_def
    2.24  by (rule convex_le.typedef_ideal_cpo)
    2.25  
    2.26 @@ -157,7 +157,7 @@
    2.27  lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    2.28  by (induct ys rule: convex_pd.principal_induct, simp, simp)
    2.29  
    2.30 -instance convex_pd :: ("domain") pcpo
    2.31 +instance convex_pd :: (bifinite) pcpo
    2.32  by intro_classes (fast intro: convex_pd_minimal)
    2.33  
    2.34  lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
    2.35 @@ -474,7 +474,7 @@
    2.36    using assms unfolding approx_chain_def
    2.37    by (simp add: lub_APP convex_map_ID finite_deflation_convex_map)
    2.38  
    2.39 -instance convex_pd :: ("domain") bifinite
    2.40 +instance convex_pd :: (bifinite) bifinite
    2.41  proof
    2.42    show "\<exists>(a::nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd). approx_chain a"
    2.43      using bifinite [where 'a='a]
    2.44 @@ -537,7 +537,7 @@
    2.45  
    2.46  text {* DEFL of type constructor = type combinator *}
    2.47  
    2.48 -lemma DEFL_convex: "DEFL('a convex_pd) = convex_defl\<cdot>DEFL('a)"
    2.49 +lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
    2.50  by (rule defl_convex_pd_def)
    2.51  
    2.52  
     3.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:34:41 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Dec 19 06:39:19 2010 -0800
     3.3 @@ -80,7 +80,7 @@
     3.4  
     3.5  type_notation (xsymbols) lower_pd ("('(_')\<flat>)")
     3.6  
     3.7 -instantiation lower_pd :: ("domain") below
     3.8 +instantiation lower_pd :: (bifinite) below
     3.9  begin
    3.10  
    3.11  definition
    3.12 @@ -89,11 +89,11 @@
    3.13  instance ..
    3.14  end
    3.15  
    3.16 -instance lower_pd :: ("domain") po
    3.17 +instance lower_pd :: (bifinite) po
    3.18  using type_definition_lower_pd below_lower_pd_def
    3.19  by (rule lower_le.typedef_ideal_po)
    3.20  
    3.21 -instance lower_pd :: ("domain") cpo
    3.22 +instance lower_pd :: (bifinite) cpo
    3.23  using type_definition_lower_pd below_lower_pd_def
    3.24  by (rule lower_le.typedef_ideal_cpo)
    3.25  
    3.26 @@ -112,7 +112,7 @@
    3.27  lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    3.28  by (induct ys rule: lower_pd.principal_induct, simp, simp)
    3.29  
    3.30 -instance lower_pd :: ("domain") pcpo
    3.31 +instance lower_pd :: (bifinite) pcpo
    3.32  by intro_classes (fast intro: lower_pd_minimal)
    3.33  
    3.34  lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
    3.35 @@ -466,7 +466,7 @@
    3.36    using assms unfolding approx_chain_def
    3.37    by (simp add: lub_APP lower_map_ID finite_deflation_lower_map)
    3.38  
    3.39 -instance lower_pd :: ("domain") bifinite
    3.40 +instance lower_pd :: (bifinite) bifinite
    3.41  proof
    3.42    show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a"
    3.43      using bifinite [where 'a='a]
    3.44 @@ -527,7 +527,7 @@
    3.45  
    3.46  end
    3.47  
    3.48 -lemma DEFL_lower: "DEFL('a lower_pd) = lower_defl\<cdot>DEFL('a)"
    3.49 +lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)"
    3.50  by (rule defl_lower_pd_def)
    3.51  
    3.52  
     4.1 --- a/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:34:41 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Sun Dec 19 06:39:19 2010 -0800
     4.3 @@ -78,7 +78,7 @@
     4.4  
     4.5  type_notation (xsymbols) upper_pd ("('(_')\<sharp>)")
     4.6  
     4.7 -instantiation upper_pd :: ("domain") below
     4.8 +instantiation upper_pd :: (bifinite) below
     4.9  begin
    4.10  
    4.11  definition
    4.12 @@ -87,11 +87,11 @@
    4.13  instance ..
    4.14  end
    4.15  
    4.16 -instance upper_pd :: ("domain") po
    4.17 +instance upper_pd :: (bifinite) po
    4.18  using type_definition_upper_pd below_upper_pd_def
    4.19  by (rule upper_le.typedef_ideal_po)
    4.20  
    4.21 -instance upper_pd :: ("domain") cpo
    4.22 +instance upper_pd :: (bifinite) cpo
    4.23  using type_definition_upper_pd below_upper_pd_def
    4.24  by (rule upper_le.typedef_ideal_cpo)
    4.25  
    4.26 @@ -110,7 +110,7 @@
    4.27  lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    4.28  by (induct ys rule: upper_pd.principal_induct, simp, simp)
    4.29  
    4.30 -instance upper_pd :: ("domain") pcpo
    4.31 +instance upper_pd :: (bifinite) pcpo
    4.32  by intro_classes (fast intro: upper_pd_minimal)
    4.33  
    4.34  lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
    4.35 @@ -461,7 +461,7 @@
    4.36    using assms unfolding approx_chain_def
    4.37    by (simp add: lub_APP upper_map_ID finite_deflation_upper_map)
    4.38  
    4.39 -instance upper_pd :: ("domain") bifinite
    4.40 +instance upper_pd :: (bifinite) bifinite
    4.41  proof
    4.42    show "\<exists>(a::nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd). approx_chain a"
    4.43      using bifinite [where 'a='a]
    4.44 @@ -522,7 +522,7 @@
    4.45  
    4.46  end
    4.47  
    4.48 -lemma DEFL_upper: "DEFL('a upper_pd) = upper_defl\<cdot>DEFL('a)"
    4.49 +lemma DEFL_upper: "DEFL('a::domain upper_pd) = upper_defl\<cdot>DEFL('a)"
    4.50  by (rule defl_upper_pd_def)
    4.51  
    4.52