# Re: [isabelle] Converting bool to {0,1}

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Converting bool to {0,1}
• From: Tobias Nipkow <nipkow at in.tum.de>
• Date: Thu, 01 Nov 2012 17:44:18 +0100
• References: <5091770E.7000205@cs.bham.ac.uk>
• User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121026 Thunderbird/16.0.2

```Am 31/10/2012 20:07, schrieb Christoph LANGE:
> Dear Isabelle community,
>
> in the course of developing our auction theory toolbox (see previous
> announcement), several questions occurred.  Let me start with a trivial one, but
> harder ones will follow:
>
> Is there a built-in function that converts {False, True} to {0, 1}, i.e. that
> would do the job of "if x then 1 else 0"?

If you frequently want to use boolean values in arithmetic formulas it may help
to install a coercion from bool to nat (or possibly directly real):

definition nat_of_bool :: "bool => nat" where
[code_unfold]: "nat_of_bool b = (if b then 1 else 0)"

declare [[coercion "nat_of_bool::bool=>nat"]]

For example

value "True+ 1 = 2"

now yields True.

Isabelle will insert nat_of_bool wherever it is needed. This is nice for input
but the coercion becomes visible in the output (which could also be circumvented)

Tobias

> A naïve search of the library source files for "bool \<Rightarrow> nat" didn't
> show any useful results.
>
> BTW, is there a way of searching for definitions of a given type, similar to
> find_theorems?
>
> Cheers, and thanks in advance,
>
> Christoph
>

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.