equal
deleted
inserted
replaced
1 (* Title: HOLCF/ccc1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Merge Theories Cprof, Sprod, Ssum, Up, Fix and |
|
7 define constants for categorical reasoning |
|
8 *) |
|
9 |
|
10 ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix + |
|
11 |
|
12 instance flat<chfin (flat_imp_chain_finite) |
|
13 |
|
14 consts |
|
15 ID :: "('a::cpo) -> 'a" |
|
16 cfcomp :: "('b->'c)->(('a::cpo)->('b::cpo))->'a->('c::cpo)" |
|
17 |
|
18 syntax "@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100) |
|
19 |
|
20 translations "f1 oo f2" == "cfcomp`f1`f2" |
|
21 |
|
22 defs |
|
23 |
|
24 ID_def "ID ==(LAM x.x)" |
|
25 oo_def "cfcomp == (LAM f g x.f`(g`x))" |
|
26 |
|
27 end |
|
28 |
|
29 |
|
30 |
|
31 |
|