src/ZF/Coind/Map.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 3840 e0baea4d485a permissions -rw-r--r--
expanded tabs
```     1 (*  Title:      ZF/Coind/Map.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
```
```     4     Copyright   1995  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 Map = QUniv +
```
```     8
```
```     9 consts
```
```    10   TMap :: [i,i] => i
```
```    11   PMap :: [i,i] => i
```
```    12 defs
```
```    13   TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
```
```    14   PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
```
```    15
```
```    16 (* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
```
```    17
```
```    18 consts
```
```    19   map_emp :: i
```
```    20   map_owr :: [i,i,i]=>i
```
```    21   map_app :: [i,i]=>i
```
```    22 defs
```
```    23   map_emp_def "map_emp == 0"
```
```    24   map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
```
```    25   map_app_def "map_app(m,a) == m``{a}"
```
```    26
```
```    27 end
```