equal
deleted
inserted
replaced
229 \medskip As a typical example, we show that type $bool$ with |
229 \medskip As a typical example, we show that type $bool$ with |
230 exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and |
230 exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and |
231 $False$ as $1$ forms an Abelian group. |
231 $False$ as $1$ forms an Abelian group. |
232 *} |
232 *} |
233 |
233 |
234 defs |
234 defs (overloaded) |
235 times_bool_def: "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)" |
235 times_bool_def: "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)" |
236 inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool" |
236 inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool" |
237 unit_bool_def: "\<unit> \\<equiv> False" |
237 unit_bool_def: "\<unit> \\<equiv> False" |
238 |
238 |
239 text {* |
239 text {* |
289 This feature enables us to \emph{lift operations}, say to Cartesian |
289 This feature enables us to \emph{lift operations}, say to Cartesian |
290 products, direct sums or function spaces. Subsequently we lift |
290 products, direct sums or function spaces. Subsequently we lift |
291 $\TIMES$ component-wise to binary products $\alpha \times \beta$. |
291 $\TIMES$ component-wise to binary products $\alpha \times \beta$. |
292 *} |
292 *} |
293 |
293 |
294 defs |
294 defs (overloaded) |
295 times_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)" |
295 times_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)" |
296 |
296 |
297 text {* |
297 text {* |
298 It is very easy to see that associativity of $\TIMES^\alpha$ and |
298 It is very easy to see that associativity of $\TIMES^\alpha$ and |
299 $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence |
299 $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence |