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