31 "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" |
32 "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" |
32 [0,0,60] 60) |
33 [0,0,60] 60) |
33 |
34 |
34 "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" |
35 "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" |
35 [0,0,60] 60) |
36 [0,0,60] 60) |
36 |
37 |
37 "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) |
38 "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) |
38 "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
39 "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
39 "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
40 "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
40 |
41 |
41 translations |
42 translations |
43 "A -> B" => "Pi(A, _K(B))" |
44 "A -> B" => "Pi(A, _K(B))" |
44 "SUM x:A. B" => "Sigma(A, %x. B)" |
45 "SUM x:A. B" => "Sigma(A, %x. B)" |
45 "A * B" => "Sigma(A, _K(B))" |
46 "A * B" => "Sigma(A, _K(B))" |
46 "{x: A. B}" == "Subtype(A, %x. B)" |
47 "{x: A. B}" == "Subtype(A, %x. B)" |
47 |
48 |
48 rules |
49 print_translation {* |
|
50 [("Pi", dependent_tr' ("@Pi", "@->")), |
|
51 ("Sigma", dependent_tr' ("@Sigma", "@*"))] *} |
49 |
52 |
50 Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}" |
53 axioms |
51 Unit_def "Unit == {x. x=one}" |
54 Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" |
52 Bool_def "Bool == {x. x=true | x=false}" |
55 Unit_def: "Unit == {x. x=one}" |
53 Plus_def "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
56 Bool_def: "Bool == {x. x=true | x=false}" |
54 Pi_def "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" |
57 Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
55 Sigma_def "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" |
58 Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" |
56 Nat_def "Nat == lfp(% X. Unit + X)" |
59 Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" |
57 List_def "List(A) == lfp(% X. Unit + A*X)" |
60 Nat_def: "Nat == lfp(% X. Unit + X)" |
|
61 List_def: "List(A) == lfp(% X. Unit + A*X)" |
58 |
62 |
59 Lists_def "Lists(A) == gfp(% X. Unit + A*X)" |
63 Lists_def: "Lists(A) == gfp(% X. Unit + A*X)" |
60 ILists_def "ILists(A) == gfp(% X.{} + A*X)" |
64 ILists_def: "ILists(A) == gfp(% X.{} + A*X)" |
61 |
65 |
62 Tall_def "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" |
66 Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" |
63 Tex_def "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" |
67 Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" |
64 Lift_def "[A] == A Un {bot}" |
68 Lift_def: "[A] == A Un {bot}" |
65 |
69 |
66 SPLIT_def "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" |
70 SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" |
|
71 |
|
72 ML {* use_legacy_bindings (the_context ()) *} |
67 |
73 |
68 end |
74 end |
69 |
|
70 |
|
71 ML |
|
72 |
|
73 val print_translation = |
|
74 [("Pi", dependent_tr' ("@Pi", "@->")), |
|
75 ("Sigma", dependent_tr' ("@Sigma", "@*"))]; |
|
76 |
|