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 

10212

10 
PiSets = Datatype_Universe + Finite +

5250

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
