equal
deleted
inserted
replaced
1 (* Title: Relation.thy |
|
2 ID: $Id$ |
|
3 Author: Riccardo Mattolini, Dip. Sistemi e Informatica |
|
4 and Lawrence C Paulson, Cambridge University Computer Laboratory |
|
5 Copyright 1994 Universita' di Firenze |
|
6 Copyright 1993 University of Cambridge |
|
7 |
|
8 Functions represented as relations in Higher-Order Set Theory |
|
9 *) |
|
10 |
|
11 Relation = Trancl + |
|
12 consts |
|
13 converse :: "('a*'a) set => ('a*'a) set" |
|
14 "^^" :: "[('a*'a) set,'a set] => 'a set" (infixl 90) |
|
15 Domain :: "('a*'a) set => 'a set" |
|
16 Range :: "('a*'a) set => 'a set" |
|
17 |
|
18 defs |
|
19 converse_def "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}" |
|
20 Domain_def "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}" |
|
21 Range_def "Range(r) == Domain(converse(r))" |
|
22 Image_def "r ^^ s == {y. y:Range(r) & (? x:s. (x,y):r)}" |
|
23 |
|
24 end |
|