isabelle: src/HOLCF/Cfun1.thy@70704dd48bd5 (annotated)

6382 8b0c9205da75 fixed typedef representing set; wenzelm parents: 5291 diff changeset	1	(* Title: HOLCF/Cfun1.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: 10863 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: 5291 diff changeset	6	Definition of the type -> of continuous functions.
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10	Cfun1 = Cont +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11
2838 2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 2640 diff changeset	12	default cpo
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 2640 diff changeset	13
6382 8b0c9205da75 fixed typedef representing set; wenzelm parents: 5291 diff changeset	14	typedef (CFun) ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}" (CfunI)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2838 diff changeset	16	(* to make << defineable *)
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2838 diff changeset	17	instance "->" :: (cpo,cpo)sq_ord
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2838 diff changeset	18
5291 5706f0ef1d43 eliminated fabs,fapp. slotosch parents: 4121 diff changeset	19	syntax
10863 fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	20	Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	21	(* application *)
10863 fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	22	Abs_CFun :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	23	(* abstraction *)
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	24	less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 12030 diff changeset	26	syntax (xsymbols)
3394 fa31c7dca468 changed priority of -> from [6,5]5 to [1,0]0 mueller parents: 3323 diff changeset	27	"->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [1,0]0)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2289 diff changeset	28	"LAM " :: "[idts, 'a => 'b] => ('a -> 'b)"
91d8abf108be adaptions for symbol font oheimb parents: 2289 diff changeset	29	("(3\\<Lambda>_./ _)" [0, 10] 10)
10863 fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	30	Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\\<cdot>_)" [999,1000] 999)
fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	31
fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	32	syntax (HTML output)
fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	33	Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\\<cdot>_)" [999,1000] 999)
fef84fefd33f Added <cdot> syntax for continuous application $. nipkow parents: 10834 diff changeset	34
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 430 diff changeset	35	defs
5291 5706f0ef1d43 eliminated fabs,fapp. slotosch parents: 4121 diff changeset	36	less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
243 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	end

author	oheimb
	Wed, 03 Apr 2002 10:21:13 +0200
changeset 13076	70704dd48bd5
parent 12114	a8e860c86252
child 14981	e73f8140af78
permissions	-rw-r--r--