equal
deleted
inserted
replaced
15 |
15 |
16 subsection {* Definition of strict product type *} |
16 subsection {* Definition of strict product type *} |
17 |
17 |
18 pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) = |
18 pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) = |
19 "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}" |
19 "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}" |
20 by simp |
20 by simp_all |
21 |
21 |
22 instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po |
22 instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po |
23 by (rule typedef_finite_po [OF type_definition_Sprod]) |
23 by (rule typedef_finite_po [OF type_definition_Sprod]) |
24 |
24 |
25 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
25 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |