src/HOLCF/sprod0.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
nipkow@243
     1
(*  Title: 	HOLCF/sprod0.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Strict product
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Sprod0 = Cfun3 +
nipkow@243
    10
nipkow@243
    11
(* new type for strict product *)
nipkow@243
    12
nipkow@243
    13
types "**" 2        (infixr 20)
nipkow@243
    14
nipkow@243
    15
arities "**" :: (pcpo,pcpo)term	
nipkow@243
    16
nipkow@243
    17
consts
nipkow@243
    18
  Sprod		:: "('a => 'b => bool)set"
nipkow@243
    19
  Spair_Rep	:: "['a,'b] => ['a,'b] => bool"
nipkow@243
    20
  Rep_Sprod	:: "('a ** 'b) => ('a => 'b => bool)"
nipkow@243
    21
  Abs_Sprod	:: "('a => 'b => bool) => ('a ** 'b)"
nipkow@243
    22
  Ispair	:: "['a,'b] => ('a ** 'b)"
nipkow@243
    23
  Isfst		:: "('a ** 'b) => 'a"
nipkow@243
    24
  Issnd		:: "('a ** 'b) => 'b"  
nipkow@243
    25
nipkow@243
    26
rules
nipkow@243
    27
nipkow@243
    28
  Spair_Rep_def		"Spair_Rep == (%a b. %x y.\
nipkow@243
    29
\				(~a=UU & ~b=UU --> x=a  & y=b ))"
nipkow@243
    30
nipkow@243
    31
  Sprod_def		"Sprod == {f. ? a b. f = Spair_Rep(a,b)}"
nipkow@243
    32
nipkow@243
    33
  (*faking a type definition... *)
nipkow@243
    34
  (* "**" is isomorphic to Sprod *)
nipkow@243
    35
nipkow@243
    36
  Rep_Sprod		"Rep_Sprod(p):Sprod"		
nipkow@243
    37
  Rep_Sprod_inverse	"Abs_Sprod(Rep_Sprod(p)) = p"	
nipkow@243
    38
  Abs_Sprod_inverse	"f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
nipkow@243
    39
nipkow@243
    40
   (*defining the abstract constants*)
nipkow@243
    41
nipkow@243
    42
  Ispair_def	"Ispair(a,b) == Abs_Sprod(Spair_Rep(a,b))"
nipkow@243
    43
nipkow@243
    44
  Isfst_def	"Isfst(p) == @z.\
nipkow@243
    45
\					(p=Ispair(UU,UU) --> z=UU)\
nipkow@243
    46
\		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=a)"  
nipkow@243
    47
nipkow@243
    48
  Issnd_def	"Issnd(p) == @z.\
nipkow@243
    49
\					(p=Ispair(UU,UU) --> z=UU)\
nipkow@243
    50
\		&(! a b. ~a=UU & ~b=UU & p=Ispair(a,b)   --> z=b)"  
nipkow@243
    51
nipkow@243
    52
end
nipkow@243
    53