equal
deleted
inserted
replaced
39 |
39 |
40 QSigma :: "[i, i => i] => i" |
40 QSigma :: "[i, i => i] => i" |
41 "QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}" |
41 "QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}" |
42 |
42 |
43 syntax |
43 syntax |
44 "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) |
44 "_QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) |
45 "<*>" :: "[i, i] => i" (infixr 80) |
|
46 |
|
47 translations |
45 translations |
48 "QSUM x:A. B" => "QSigma(A, %x. B)" |
46 "QSUM x:A. B" => "QSigma(A, %x. B)" |
49 "A <*> B" => "QSigma(A, %_. B)" |
47 |
|
48 abbreviation |
|
49 qprod (infixr "<*>" 80) where |
|
50 "A <*> B == QSigma(A, %_. B)" |
50 |
51 |
51 constdefs |
52 constdefs |
52 qsum :: "[i,i]=>i" (infixr "<+>" 65) |
53 qsum :: "[i,i]=>i" (infixr "<+>" 65) |
53 "A <+> B == ({0} <*> A) Un ({1} <*> B)" |
54 "A <+> B == ({0} <*> A) Un ({1} <*> B)" |
54 |
55 |
58 QInr :: "i=>i" |
59 QInr :: "i=>i" |
59 "QInr(b) == <1;b>" |
60 "QInr(b) == <1;b>" |
60 |
61 |
61 qcase :: "[i=>i, i=>i, i]=>i" |
62 qcase :: "[i=>i, i=>i, i]=>i" |
62 "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
63 "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
63 |
|
64 |
|
65 print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *} |
|
66 |
64 |
67 |
65 |
68 subsection{*Quine ordered pairing*} |
66 subsection{*Quine ordered pairing*} |
69 |
67 |
70 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
68 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
384 val QInr_mono = thm "QInr_mono"; |
382 val QInr_mono = thm "QInr_mono"; |
385 val qsum_mono = thm "qsum_mono"; |
383 val qsum_mono = thm "qsum_mono"; |
386 *} |
384 *} |
387 |
385 |
388 end |
386 end |
389 |
|