equal
deleted
inserted
replaced
13 |
13 |
14 subsection {* Definition of strict product type *} |
14 subsection {* Definition of strict product type *} |
15 |
15 |
16 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" |
16 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" |
17 |
17 |
18 pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set" |
18 pcpodef ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set" |
19 unfolding sprod_def by simp_all |
19 unfolding sprod_def by simp_all |
20 |
20 |
21 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
21 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
22 by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) |
22 by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) |
23 |
23 |