|
5250
|
1 |
(* Title: HOL/ex/PiSets.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Florian Kammueller, University of Cambridge
|
|
|
4 |
|
|
5856
|
5 |
The bijection between elements of the Pi set and functional graphs
|
|
|
6 |
|
|
|
7 |
Also the nice -> operator for function space
|
|
5250
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
PiSets = Univ + Finite +
|
|
|
11 |
|
|
5856
|
12 |
syntax
|
|
|
13 |
"->" :: "['a set, 'b set] => ('a => 'b) set" (infixr 60)
|
|
5846
|
14 |
|
|
5856
|
15 |
translations
|
|
|
16 |
"A -> B" == "A funcset B"
|
|
5250
|
17 |
|
|
5846
|
18 |
constdefs
|
|
|
19 |
(* bijection between Pi_sig and Pi_=> *)
|
|
5250
|
20 |
PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
|
|
5846
|
21 |
"PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
|
|
5250
|
22 |
|
|
|
23 |
Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set"
|
|
5846
|
24 |
"Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
|
|
5250
|
25 |
|
|
|
26 |
end
|