src/HOLCF/Cprod3.thy
author regensbu
Mon, 28 Nov 1994 19:48:30 +0100
changeset 752 b89462f9d5f1
parent 625 119391dd1d59
child 1168 74be52691d62
permissions -rw-r--r--
---------------------------------------------------------------------- Committing in HOLCF Use new translation mechanism and keyword syntax, cinfix.ML no longer needed. Optimized proofs in Cont.ML Modified Files: Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README Sprod3.thy Tr2.thy ccc1.thy ----------------------------------------------------------------------
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/cprod3.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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
Class instance of  * for class pcpo
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
*)
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
Cprod3 = Cprod2 +
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
arities "*" :: (pcpo,pcpo)pcpo			(* Witness cprod2.ML *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
consts  
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
    16
	cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
	cfst         :: "('a*'b)->'a"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
	csnd         :: "('a*'b)->'b"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
	csplit       :: "('a->'b->'c)->('a*'b)->'c"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
752
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
    21
syntax	"@cpair"     :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
    22
b89462f9d5f1 ----------------------------------------------------------------------
regensbu
parents: 625
diff changeset
    23
translations "x#y" == "cpair[x][y]"
625
119391dd1d59 New version
nipkow
parents: 442
diff changeset
    24
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
rules 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
442
13ac1fd0a14d added parentheses made necessary by change of constrain's precedence
clasohm
parents: 243
diff changeset
    27
inst_cprod_pcpo	"(UU::'a*'b) = <UU,UU>"
243
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
cpair_def	"cpair  == (LAM x y.<x,y>)"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
cfst_def	"cfst   == (LAM p.fst(p))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
csnd_def	"csnd   == (LAM p.snd(p))"	
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
csplit_def	"csplit == (LAM f p.f[cfst[p]][csnd[p]])"
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
end
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    38