28 fix a b show "Pair_Rep a b : ?Prod" |
28 fix a b show "Pair_Rep a b : ?Prod" |
29 by blast |
29 by blast |
30 qed |
30 qed |
31 |
31 |
32 syntax (symbols) |
32 syntax (symbols) |
33 "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
33 "*" :: "[type, type] => type" ("(_ \\<times>/ _)" [21, 20] 20) |
34 syntax (HTML output) |
34 syntax (HTML output) |
35 "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) |
35 "*" :: "[type, type] => type" ("(_ \\<times>/ _)" [21, 20] 20) |
36 |
36 |
37 |
37 |
38 (* abstract constants and syntax *) |
38 (* abstract constants and syntax *) |
39 |
39 |
40 consts |
40 consts |
72 |
72 |
73 "SIGMA x:A. B" => "Sigma A (%x. B)" |
73 "SIGMA x:A. B" => "Sigma A (%x. B)" |
74 "A <*> B" => "Sigma A (_K B)" |
74 "A <*> B" => "Sigma A (_K B)" |
75 |
75 |
76 syntax (symbols) |
76 syntax (symbols) |
77 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) |
77 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
78 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
78 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80) |
79 |
79 |
80 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} |
80 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} |
81 |
81 |
82 |
82 |
83 (* definitions *) |
83 (* definitions *) |
84 |
84 |
85 local |
85 local |
86 |
86 |
87 defs |
87 defs |
88 Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" |
88 Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" |
89 fst_def: "fst p == SOME a. EX b. p = (a, b)" |
89 fst_def: "fst p == THE a. EX b. p = (a, b)" |
90 snd_def: "snd p == SOME b. EX a. p = (a, b)" |
90 snd_def: "snd p == THE b. EX a. p = (a, b)" |
91 split_def: "split == (%c p. c (fst p) (snd p))" |
91 split_def: "split == (%c p. c (fst p) (snd p))" |
92 prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))" |
92 prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))" |
93 Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" |
93 Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" |
94 |
94 |
95 |
95 |