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

author	clasohm
	Tue, 07 Feb 1995 11:59:32 +0100
changeset 892	d0dc8d057929
parent 752	b89462f9d5f1
child 1168	74be52691d62
permissions	-rw-r--r--