author | paulson |
Mon, 29 Sep 1997 11:37:02 +0200 | |
changeset 3724 | f33e301a89f5 |
parent 1478 | 2b8c2a7547ab |
child 3840 | e0baea4d485a |
permissions | -rw-r--r-- |
(* Title: ZF/ex/Rmap ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Inductive definition of an operator to "map" a relation over a list *) Rmap = List + consts rmap :: i=>i inductive domains "rmap(r)" <= "list(domain(r))*list(range(r))" intrs NilI "<Nil,Nil> : rmap(r)" ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==> <Cons(x,xs), Cons(y,ys)> : rmap(r)" type_intrs "[domainI,rangeI] @ list.intrs" end