src/HOLCF/Sprod3.thy
author clasohm
Wed, 29 Jun 1994 12:03:41 +0200
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 625 119391dd1d59
permissions -rw-r--r--
added parentheses made necessary by change of constrain's precedence
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     1
(*  Title: 	HOLCF/sprod3.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
    Author: 	Franz Regensburger
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
Class instance of  ** for class pcpo
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
Sprod3 = Sprod2 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
arities "**" :: (pcpo,pcpo)pcpo			(* Witness sprod2.ML *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    12
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
consts  
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
	"@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
	"cop @spair" :: "'a -> 'b -> ('a**'b)" ("spair")
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
					(* continuous strict pairing *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
	sfst         :: "('a**'b)->'a"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
	ssnd         :: "('a**'b)->'b"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    21
rules 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
442
13ac1fd0a14d added parentheses made necessary by change of constrain's precedence
clasohm
parents: 243
diff changeset
    23
inst_sprod_pcpo	"(UU::'a**'b) = Ispair(UU,UU)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
spair_def	"spair  == (LAM x y.Ispair(x,y))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
sfst_def	"sfst   == (LAM p.Isfst(p))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
ssnd_def	"ssnd   == (LAM p.Issnd(p))"	
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
ssplit_def	"ssplit == (LAM f. strictify[LAM p.f[sfst[p]][ssnd[p]]])"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    28
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    29
end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
ML
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    33
(* ----------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    34
(* parse translations for the above mixfix                               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    35
(* ----------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    36
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    37
val parse_translation = [("@spair",mk_cinfixtr "@spair")];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    38
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    39