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"
|
|
13 |
"PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
|
|
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
|