equal
deleted
inserted
replaced
|
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 |