isabelle: src/HOLCF/Cfun1.thy@84c2178db936 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 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
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	Definition of the type -> of continuous functions
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
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	14	typedef (CFun) ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	consts
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	17	fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	18	(* application *)
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	19	fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	20	(* usually Abs_Cfun *)
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	21	(* abstraction *)
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	22	less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	24	syntax "@fapp" :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 430 diff changeset	25
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 430 diff changeset	26	translations "f`x" == "fapp f x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
2394 91d8abf108be adaptions for symbol font oheimb parents: 2289 diff changeset	28	syntax (symbols)
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	29	"->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [6,5]5)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2289 diff changeset	30	"LAM " :: "[idts, 'a => 'b] => ('a -> 'b)"
91d8abf108be adaptions for symbol font oheimb parents: 2289 diff changeset	31	("(3\\<Lambda>_./ _)" [0, 10] 10)
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 430 diff changeset	32	defs
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	33	fabs_def "fabs==Abs_CFun"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	34	fapp_def "fapp==Rep_CFun"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	36	less_cfun_def "less == (% fo1 fo2. fapp fo1 << fapp 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	paulson
	Wed, 23 Apr 1997 11:00:48 +0200
changeset 3017	84c2178db936
parent 2838	2e908f29bc3d
child 3323	194ae2e0c193
permissions	-rw-r--r--