src/HOL/HOLCF/Ssum.thy
changeset 45695 b108b3d7c49e
parent 44066 d74182c93f04
child 46125 00cd193a48dc
     1.1 --- a/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 16:27:10 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 17:30:01 2011 +0100
     1.3 @@ -13,11 +13,14 @@
     1.4  
     1.5  subsection {* Definition of strict sum type *}
     1.6  
     1.7 -pcpodef ('a, 'b) ssum (infixr "++" 10) = 
     1.8 -  "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
     1.9 -    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
    1.10 -    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
    1.11 -by simp_all
    1.12 +definition
    1.13 +  "ssum =
    1.14 +    {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
    1.15 +      (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
    1.16 +      (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
    1.17 +
    1.18 +pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
    1.19 +  unfolding ssum_def by simp_all
    1.20  
    1.21  instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    1.22  by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])