src/ZF/ex/Rmap.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 1155 928a16e02f9f
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp@515
     1
(*  Title: 	ZF/ex/Rmap
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Inductive definition of an operator to "map" a relation over a list
lcp@515
     7
*)
lcp@515
     8
lcp@515
     9
Rmap = List +
lcp@515
    10
lcp@515
    11
consts
lcp@515
    12
  rmap :: "i=>i"
lcp@515
    13
lcp@515
    14
inductive
lcp@515
    15
  domains "rmap(r)" <= "list(domain(r))*list(range(r))"
lcp@515
    16
  intrs
lcp@515
    17
    NilI  "<Nil,Nil> : rmap(r)"
lcp@515
    18
lcp@515
    19
    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
lcp@515
    20
\          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
lcp@515
    21
lcp@515
    22
  type_intrs "[domainI,rangeI] @ list.intrs"
lcp@515
    23
lcp@515
    24
end
lcp@515
    25