doc-src/Logics/ZF.tex
changeset 131 bb0caac13eff
parent 114 96c627d2815e
child 287 6b62a6ddbe15
equal deleted 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