author | paulson |
Thu, 31 May 2001 18:28:23 +0200 | |
changeset 11354 | 9b80fe19407f |
parent 11316 | b4e71bd751e4 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/ex/Rmap |
515 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
515 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Inductive definition of an operator to "map" a relation over a list |
|
7 |
*) |
|
8 |
||
11354
9b80fe19407f
examples files start from Main instead of various ZF theories
paulson
parents:
11316
diff
changeset
|
9 |
Rmap = Main + |
515 | 10 |
|
11 |
consts |
|
1401 | 12 |
rmap :: i=>i |
515 | 13 |
|
14 |
inductive |
|
15 |
domains "rmap(r)" <= "list(domain(r))*list(range(r))" |
|
16 |
intrs |
|
11316 | 17 |
NilI "<Nil,Nil> \\<in> rmap(r)" |
515 | 18 |
|
11316 | 19 |
ConsI "[| <x,y>: r; <xs,ys> \\<in> rmap(r) |] ==> |
20 |
<Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)" |
|
515 | 21 |
|
3841 | 22 |
type_intrs "[domainI,rangeI] @ list.intrs" |
515 | 23 |
|
24 |
end |
|
25 |