|
1478
|
1 |
(* Title: ZF/Coind/Map.thy
|
|
915
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Jacob Frost, Cambridge University Computer Laboratory
|
|
915
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
Map = QUniv +
|
|
|
8 |
|
|
|
9 |
consts
|
|
1401
|
10 |
TMap :: [i,i] => i
|
|
|
11 |
PMap :: [i,i] => i
|
|
933
|
12 |
defs
|
|
3840
|
13 |
TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A. m``{a}:B}"
|
|
915
|
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
|
|
1401
|
19 |
map_emp :: i
|
|
|
20 |
map_owr :: [i,i,i]=>i
|
|
|
21 |
map_app :: [i,i]=>i
|
|
933
|
22 |
defs
|
|
915
|
23 |
map_emp_def "map_emp == 0"
|
|
6068
|
24 |
map_owr_def "map_owr(m,a,b) ==
|
|
|
25 |
SUM x:{a} Un domain(m). if x=a then b else m``{x}"
|
|
915
|
26 |
map_app_def "map_app(m,a) == m``{a}"
|
|
|
27 |
|
|
|
28 |
end
|