author | wenzelm |
Mon, 10 Dec 2001 20:59:43 +0100 | |
changeset 12459 | 6978ab7cac64 |
parent 11443 | 77ed7e2b56c8 |
permissions | -rw-r--r-- |
11443 | 1 |
(* Title: HOL/ex/PiSets.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Kammueller, University of Cambridge |
|
4 |
||
5 |
The bijection between elements of the Pi set and functional graphs |
|
6 |
*) |
|
7 |
||
8 |
PiSets = Group + |
|
9 |
||
10 |
constdefs |
|
11 |
(* bijection between Pi_sig and Pi_=> *) |
|
12 |
PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set" |
|
12459
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
11443
diff
changeset
|
13 |
"PiBij A B == %f: Pi A B. {(x, y). x: A & y = f x}" |
11443 | 14 |
|
15 |
Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set" |
|
16 |
"Graph A B == {f. f \\<in> Pow(Sigma A B) & (\\<forall>x\\<in>A. \\<exists>!y. (x, y) \\<in> f)}" |
|
17 |
||
18 |
end |