equal
deleted
inserted
replaced
1 (* Title: HOLCF/cfun1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Definition of the type -> of continuous functions |
|
7 |
|
8 *) |
|
9 |
|
10 Cfun1 = Cont + |
|
11 |
|
12 |
|
13 (* new type of continuous functions *) |
|
14 |
|
15 types "->" 2 (infixr 5) |
|
16 |
|
17 arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *) |
|
18 |
|
19 consts |
|
20 Cfun :: "('a => 'b)set" |
|
21 fapp :: "('a -> 'b)=>('a => 'b)" ("(_[_])" [11,0] 1000) |
|
22 (* usually Rep_Cfun *) |
|
23 (* application *) |
|
24 |
|
25 fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10) |
|
26 (* usually Abs_Cfun *) |
|
27 (* abstraction *) |
|
28 |
|
29 less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool" |
|
30 |
|
31 rules |
|
32 |
|
33 Cfun_def "Cfun == {f. contX(f)}" |
|
34 |
|
35 (*faking a type definition... *) |
|
36 (* -> is isomorphic to Cfun *) |
|
37 |
|
38 Rep_Cfun "fapp(fo):Cfun" |
|
39 Rep_Cfun_inverse "fabs(fapp(fo)) = fo" |
|
40 Abs_Cfun_inverse "f:Cfun ==> fapp(fabs(f))=f" |
|
41 |
|
42 (*defining the abstract constants*) |
|
43 less_cfun_def "less_cfun(fo1,fo2) == ( fapp(fo1) << fapp(fo2) )" |
|
44 |
|
45 end |
|