5250
|
1 |
(* Title: HOL/ex/PiSets.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, University of Cambridge
|
|
4 |
|
|
5 |
Theory for Pi type in terms of sets.
|
|
6 |
*)
|
|
7 |
|
|
8 |
PiSets = Univ + Finite +
|
|
9 |
|
|
10 |
consts
|
|
11 |
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
|
|
12 |
|
|
13 |
consts
|
|
14 |
restrict :: "['a => 'b, 'a set] => ('a => 'b)"
|
|
15 |
|
|
16 |
defs
|
|
17 |
restrict_def "restrict f A == (%x. if x : A then f x else (@ y. True))"
|
|
18 |
|
|
19 |
syntax
|
|
20 |
"@Pi" :: "[idt, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
|
|
21 |
"@->" :: "['a set, 'b set] => ('a => 'b) set" ("_ -> _" [91,90]90)
|
|
22 |
(* or "->" ... (infixr 60) and at the end print_translation (... op ->) *)
|
|
23 |
"@lam" :: "[idt, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10)
|
|
24 |
(* Could as well take pttrn *)
|
|
25 |
|
|
26 |
translations
|
|
27 |
"PI x:A. B" => "Pi A (%x. B)"
|
|
28 |
"A -> B" => "Pi A (_K B)"
|
|
29 |
"lam x:A. f" == "restrict (%x. f) A"
|
|
30 |
(* Larry fragen: "lam (x,y): A. f" == "restrict (%(x,y). f) A" *)
|
|
31 |
defs
|
|
32 |
Pi_def "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
|
|
33 |
|
|
34 |
consts
|
|
35 |
Fset_apply :: "[('a => 'b) set, 'a]=> 'b set" ("_ @@ _" [90,91]90)
|
|
36 |
|
|
37 |
defs
|
|
38 |
Fset_apply_def "F @@ a == (%f. f a) `` F"
|
|
39 |
|
|
40 |
consts
|
|
41 |
compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
|
|
42 |
|
|
43 |
defs
|
|
44 |
compose_def "compose A g f == lam x : A. g(f x)"
|
|
45 |
|
|
46 |
consts
|
|
47 |
Inv :: "['a set, 'a => 'b] => ('b => 'a)"
|
|
48 |
|
|
49 |
defs
|
|
50 |
Inv_def "Inv A f == (% x. (@ y. y : A & f y = x))"
|
|
51 |
|
|
52 |
(* new: bijection between Pi_sig and Pi_=> *)
|
|
53 |
consts
|
|
54 |
PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set"
|
|
55 |
|
|
56 |
defs
|
|
57 |
PiBij_def "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}"
|
|
58 |
|
|
59 |
consts
|
|
60 |
Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set"
|
|
61 |
|
|
62 |
defs
|
|
63 |
Graph_def "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}"
|
|
64 |
|
|
65 |
end
|
|
66 |
|
|
67 |
ML
|
|
68 |
val print_translation = [("Pi", dependent_tr' ("@Pi", "@->"))];
|