src/HOLCF/Ssum.thy
 changeset 35525 fa231b86cb1e parent 35491 92e0028a46f2 child 35547 991a6af75978
equal 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))"`