isabelle: src/HOLCF/Sprod3.thy@efca1e0710fb (annotated)

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
657 2b16819fbd71 simplified syntax of infix continuous functiuons nipkow parents: 625 diff changeset	13	consts
2b16819fbd71 simplified syntax of infix continuous functiuons nipkow parents: 625 diff changeset	14	spair :: "'a -> 'b -> ('a*'b)" ( continuous strict pairing *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15	sfst :: "('a**'b)->'a"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	ssnd :: "('a**'b)->'b"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17	ssplit :: "('a->'b->'c)->('a**'b)->'c"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18
657 2b16819fbd71 simplified syntax of infix continuous functiuons nipkow parents: 625 diff changeset	19	syntax "@spair" :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
2b16819fbd71 simplified syntax of infix continuous functiuons nipkow parents: 625 diff changeset	20	translations "x##y" == "spair[x][y]"
625 119391dd1d59 New version nipkow parents: 442 diff changeset	21
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23
442 13ac1fd0a14d added parentheses made necessary by change of constrain's precedence clasohm parents: 243 diff changeset	24	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	25	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	26	sfst_def "sfst == (LAM p.Isfst(p))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27	ssnd_def "ssnd == (LAM p.Issnd(p))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28	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	29
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31
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

author	lcp
	Mon, 21 Nov 1994 10:51:40 +0100
changeset 718	efca1e0710fb
parent 657	2b16819fbd71
child 752	b89462f9d5f1
permissions	-rw-r--r--