doc-src/Logics/ZF.tex
 changeset 131 bb0caac13eff parent 114 96c627d2815e child 287 6b62a6ddbe15
equal inserted replaced
130:c035b6b9eafc 131:bb0caac13eff
  1094 \begin{figure}
  1094 \begin{figure}
  1095 \begin{ttbox}
  1095 \begin{ttbox}
  1096 \idx{one_def}        1    == succ(0)
  1096 \idx{one_def}        1    == succ(0)
  1097 \idx{bool_def}       bool == {0,1}
  1097 \idx{bool_def}       bool == {0,1}
  1098 \idx{cond_def}       cond(b,c,d) == if(b=1,c,d)
  1098 \idx{cond_def}       cond(b,c,d) == if(b=1,c,d)

  1099 \idx{not_def}        not(b) == cond(b,0,1)

  1100 \idx{and_def}        a and b == cond(a,b,0)

  1101 \idx{or_def}         a or b == cond(a,1,b)

  1102 \idx{xor_def}        a xor b == cond(a,not(b),b)
  1099
  1103
  1100 \idx{sum_def}        A+B == \{0\}*A Un \{1\}*B
  1104 \idx{sum_def}        A+B == \{0\}*A Un \{1\}*B
  1101 \idx{Inl_def}        Inl(a) == <0,a>
  1105 \idx{Inl_def}        Inl(a) == <0,a>
  1102 \idx{Inr_def}        Inr(b) == <1,b>
  1106 \idx{Inr_def}        Inr(b) == <1,b>
  1103 \idx{case_def}       case(c,d,u) == split(%y z. cond(y, d(z), c(z)), u)
  1107 \idx{case_def}       case(c,d,u) == split(%y z. cond(y, d(z), c(z)), u)
  1104 \subcaption{Definitions}
  1108 \subcaption{Definitions}
  1105
  1109
  1106 \idx{bool_1I}        1 : bool
  1110 \idx{bool_1I}        1 : bool
  1107 \idx{bool_0I}        0 : bool
  1111 \idx{bool_0I}        0 : bool
  1108
  1112
  1109 \idx{boolE}          [| c: bool;  P(1);  P(0) |] ==> P(c)
  1113 \idx{boolE}          [| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P
  1110 \idx{cond_1}         cond(1,c,d) = c
  1114 \idx{cond_1}         cond(1,c,d) = c
  1111 \idx{cond_0}         cond(0,c,d) = d
  1115 \idx{cond_0}         cond(0,c,d) = d
  1112
  1116
  1113 \idx{sum_InlI}       a : A ==> Inl(a) : A+B
  1117 \idx{sum_InlI}       a : A ==> Inl(a) : A+B
  1114 \idx{sum_InrI}       b : B ==> Inr(b) : A+B
  1118 \idx{sum_InrI}       b : B ==> Inr(b) : A+B
  1254
  1258
  1255 Figure~\ref{zf-equalities} presents commutative, associative, distributive,
  1259 Figure~\ref{zf-equalities} presents commutative, associative, distributive,
  1256 and idempotency laws of union and intersection, along with other equations.
  1260 and idempotency laws of union and intersection, along with other equations.
  1257 See file \ttindexbold{ZF/equalities.ML}.
  1261 See file \ttindexbold{ZF/equalities.ML}.
  1258
  1262
  1259 Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with a
  1263 Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with the usual
  1260 conditional operator.  It also defines the disjoint union of two sets, with
  1264 operators including a conditional.  It also defines the disjoint union of
  1261 injections and a case analysis operator.  See files
  1265 two sets, with injections and a case analysis operator.  See files
  1262 \ttindexbold{ZF/bool.ML} and \ttindexbold{ZF/sum.ML}.
  1266 \ttindexbold{ZF/bool.ML} and \ttindexbold{ZF/sum.ML}.
  1263
  1267
  1264 Figure~\ref{zf-qpair} defines a notion of ordered pair that admits
  1268 Figure~\ref{zf-qpair} defines a notion of ordered pair that admits
  1265 non-well-founded tupling.  Such pairs are written {\tt<$a$;$b$>}.  It also
  1269 non-well-founded tupling.  Such pairs are written {\tt<$a$;$b$>}.  It also
  1266 defines the eliminator \ttindexbold{qsplit}, the converse operator
  1270 defines the eliminator \ttindexbold{qsplit}, the converse operator