equal
deleted
inserted
replaced
17 definition "ssum = |
17 definition "ssum = |
18 {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or> |
18 {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or> |
19 (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or> |
19 (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or> |
20 (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}" |
20 (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}" |
21 |
21 |
22 pcpodef ('a, 'b) ssum ("(_ \<oplus>/ _)" [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set" |
22 pcpodef ('a, 'b) ssum (\<open>(_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set" |
23 by (simp_all add: ssum_def) |
23 by (simp_all add: ssum_def) |
24 |
24 |
25 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
25 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
26 by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) |
26 by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) |
27 |
27 |
28 type_notation (ASCII) |
28 type_notation (ASCII) |
29 ssum (infixr "++" 10) |
29 ssum (infixr \<open>++\<close> 10) |
30 |
30 |
31 |
31 |
32 subsection \<open>Definitions of constructors\<close> |
32 subsection \<open>Definitions of constructors\<close> |
33 |
33 |
34 definition sinl :: "'a \<rightarrow> ('a ++ 'b)" |
34 definition sinl :: "'a \<rightarrow> ('a ++ 'b)" |