isabelle: src/HOLCF/Sprod0.thy@e9d2f771b3c7 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	1	(* Title: HOLCF/Sprod0.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
12030 46d57d0290a2 GPLed; wenzelm parents: 6382 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
6382 8b0c9205da75 fixed typedef representing set; wenzelm parents: 2640 diff changeset	6	Strict product with typedef.
243 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	Sprod0 = Cfun3 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	11	constdefs
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	12	Spair_Rep :: ['a,'b] => ['a,'b] => bool
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	13	"Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
6382 8b0c9205da75 fixed typedef representing set; wenzelm parents: 2640 diff changeset	15	typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 12030 diff changeset	17	syntax (xsymbols)
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	18	"**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
14565 c6dc17aab88a use more symbols in HTML output kleing parents: 12114 diff changeset	19	syntax (HTML output)
c6dc17aab88a use more symbols in HTML output kleing parents: 12114 diff changeset	20	"**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	21
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22	consts
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	23	Ispair :: "['a,'b] => ('a ** 'b)"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	24	Isfst :: "('a ** 'b) => 'a"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	25	Issnd :: "('a ** 'b) => 'b"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	27	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28	(defining the abstract constants)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	30	Ispair_def "Ispair a b == Abs_Sprod(Spair_Rep a b)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	32	Isfst_def "Isfst(p) == @z. (p=Ispair UU UU --> z=UU)
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	33	&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	35	Issnd_def "Issnd(p) == @z. (p=Ispair UU UU --> z=UU)
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	36	&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	38
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39	end

author	kleing
	Sat, 17 Apr 2004 00:50:45 +0200
changeset 14611	e9d2f771b3c7
parent 14565	c6dc17aab88a
child 14981	e73f8140af78
permissions	-rw-r--r--