author | paulson |
Thu, 31 May 2001 18:28:23 +0200 | |
changeset 11354 | 9b80fe19407f |
parent 11316 | b4e71bd751e4 |
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 = Main + consts rmap :: i=>i inductive domains "rmap(r)" <= "list(domain(r))*list(range(r))" intrs NilI "<Nil,Nil> \\<in> rmap(r)" ConsI "[| <x,y>: r; <xs,ys> \\<in> rmap(r) |] ==> <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)" type_intrs "[domainI,rangeI] @ list.intrs" end