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