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

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/sprod3.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
243 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
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	11	arities "*" :: (pcpo,pcpo)pcpo ( Witness sprod2.ML *)
243 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
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	14	spair :: "'a -> 'b -> ('a*'b)" ( continuous strict pairing *)
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	15	sfst :: "('a**'b)->'a"
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	16	ssnd :: "('a**'b)->'b"
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	17	ssplit :: "('a->'b->'c)->('a**'b)->'c"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	19	syntax
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	20	"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(\|_,/ _\|'))")
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 657 diff changeset	21
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	22	translations
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	23	"(\|x, y, z\|)" == "(\|x, (\|y, z\|)\|)"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	24	"(\|x, y\|)" == "spair`x`y"
625 119391dd1d59 New version nipkow parents: 442 diff changeset	25
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	26	syntax (symbols)
2420 cb21eef65704 corrected 8bit symbols oheimb parents: 2394 diff changeset	27	"@stuple" :: "['a, args] => 'a ** 'b" ("(1\\<lparr>_,/ _\\<rparr>)")
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	28
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	31	inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	32
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 752 diff changeset	33	defs
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	34	spair_def "spair == (LAM x y.Ispair x y)"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	35	sfst_def "sfst == (LAM p.Isfst p)"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	36	ssnd_def "ssnd == (LAM p.Issnd p)"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	37	ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	38
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	39
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43

author	paulson
	Fri, 31 Jan 1997 17:13:19 +0100
changeset 2572	8a47f85e7a03
parent 2420	cb21eef65704
child 2640	ee4dfce170a0
permissions	-rw-r--r--