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
     1 (*  Title: 	ZF/ex/Rmap
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Inductive definition of an operator to "map" a relation over a list
     7 *)
     8 
     9 Rmap = List +
    10 
    11 consts
    12   rmap :: "i=>i"
    13 
    14 inductive
    15   domains "rmap(r)" <= "list(domain(r))*list(range(r))"
    16   intrs
    17     NilI  "<Nil,Nil> : rmap(r)"
    18 
    19     ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> \
    20 \          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
    21 
    22   type_intrs "[domainI,rangeI] @ list.intrs"
    23 
    24 end
    25