src/HOLCF/Ssum.thy
changeset 35525 fa231b86cb1e
parent 35491 92e0028a46f2
child 35547 991a6af75978
equal deleted inserted replaced
35524:a2a59e92b02e 35525:fa231b86cb1e
    10 
    10 
    11 defaultsort pcpo
    11 defaultsort pcpo
    12 
    12 
    13 subsection {* Definition of strict sum type *}
    13 subsection {* Definition of strict sum type *}
    14 
    14 
    15 pcpodef (Ssum)  ('a, 'b) "++" (infixr "++" 10) = 
    15 pcpodef (Ssum)  ('a, 'b) ssum (infixr "++" 10) = 
    16   "{p :: tr \<times> ('a \<times> 'b).
    16   "{p :: tr \<times> ('a \<times> 'b).
    17     (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
    17     (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
    18     (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
    18     (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
    19 by simp_all
    19 by simp_all
    20 
    20 
    21 instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    21 instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    22 by (rule typedef_finite_po [OF type_definition_Ssum])
    22 by (rule typedef_finite_po [OF type_definition_Ssum])
    23 
    23 
    24 instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    24 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    25 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
    25 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
    26 
    26 
    27 syntax (xsymbols)
    27 syntax (xsymbols)
    28   "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    28   ssum          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    29 syntax (HTML output)
    29 syntax (HTML output)
    30   "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    30   ssum          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
    31 
    31 
    32 subsection {* Definitions of constructors *}
    32 subsection {* Definitions of constructors *}
    33 
    33 
    34 definition
    34 definition
    35   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
    35   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
   148 apply (simp add: sinl_Abs_Ssum Ssum_def)
   148 apply (simp add: sinl_Abs_Ssum Ssum_def)
   149 apply (rule disjI2, rule disjI2, rule_tac x=b in exI)
   149 apply (rule disjI2, rule disjI2, rule_tac x=b in exI)
   150 apply (simp add: sinr_Abs_Ssum Ssum_def)
   150 apply (simp add: sinr_Abs_Ssum Ssum_def)
   151 done
   151 done
   152 
   152 
   153 lemma ssumE [cases type: ++]:
   153 lemma ssumE [cases type: ssum]:
   154   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
   154   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
   155    \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
   155    \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
   156    \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   156    \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   157 by (cut_tac z=p in Exh_Ssum, auto)
   157 by (cut_tac z=p in Exh_Ssum, auto)
   158 
   158 
   159 lemma ssum_induct [induct type: ++]:
   159 lemma ssum_induct [induct type: ssum]:
   160   "\<lbrakk>P \<bottom>;
   160   "\<lbrakk>P \<bottom>;
   161    \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
   161    \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
   162    \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
   162    \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
   163 by (cases x, simp_all)
   163 by (cases x, simp_all)
   164 
   164 
   201 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
   201 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
   202 by (cases z, simp_all)
   202 by (cases z, simp_all)
   203 
   203 
   204 subsection {* Strict sum preserves flatness *}
   204 subsection {* Strict sum preserves flatness *}
   205 
   205 
   206 instance "++" :: (flat, flat) flat
   206 instance ssum :: (flat, flat) flat
   207 apply (intro_classes, clarify)
   207 apply (intro_classes, clarify)
   208 apply (case_tac x, simp)
   208 apply (case_tac x, simp)
   209 apply (case_tac y, simp_all add: flat_below_iff)
   209 apply (case_tac y, simp_all add: flat_below_iff)
   210 apply (case_tac y, simp_all add: flat_below_iff)
   210 apply (case_tac y, simp_all add: flat_below_iff)
   211 done
   211 done
   294     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   294     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
   295 qed
   295 qed
   296 
   296 
   297 subsection {* Strict sum is a bifinite domain *}
   297 subsection {* Strict sum is a bifinite domain *}
   298 
   298 
   299 instantiation "++" :: (bifinite, bifinite) bifinite
   299 instantiation ssum :: (bifinite, bifinite) bifinite
   300 begin
   300 begin
   301 
   301 
   302 definition
   302 definition
   303   approx_ssum_def:
   303   approx_ssum_def:
   304     "approx = (\<lambda>n. ssum_map\<cdot>(approx n)\<cdot>(approx n))"
   304     "approx = (\<lambda>n. ssum_map\<cdot>(approx n)\<cdot>(approx n))"