slotosch@2640: (* Title: HOLCF/Sprod0.thy nipkow@243: ID: $Id$ clasohm@1479: Author: Franz Regensburger wenzelm@12030: License: GPL (GNU GENERAL PUBLIC LICENSE) nipkow@243: wenzelm@6382: Strict product with typedef. nipkow@243: *) nipkow@243: nipkow@243: Sprod0 = Cfun3 + nipkow@243: slotosch@2640: constdefs slotosch@2640: Spair_Rep :: ['a,'b] => ['a,'b] => bool slotosch@2640: "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))" nipkow@243: wenzelm@6382: typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}" nipkow@243: oheimb@2394: syntax (symbols) slotosch@2640: "**" :: [type, type] => type ("(_ \\/ _)" [21,20] 20) oheimb@2394: nipkow@243: consts clasohm@1479: Ispair :: "['a,'b] => ('a ** 'b)" clasohm@1479: Isfst :: "('a ** 'b) => 'a" clasohm@1479: Issnd :: "('a ** 'b) => 'b" nipkow@243: regensbu@1168: defs nipkow@243: (*defining the abstract constants*) nipkow@243: clasohm@1479: Ispair_def "Ispair a b == Abs_Sprod(Spair_Rep a b)" nipkow@243: slotosch@2640: Isfst_def "Isfst(p) == @z. (p=Ispair UU UU --> z=UU) clasohm@1479: &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)" nipkow@243: slotosch@2640: Issnd_def "Issnd(p) == @z. (p=Ispair UU UU --> z=UU) clasohm@1479: &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" nipkow@243: regensbu@1274: nipkow@243: end