# 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
*In-reply-to*: <5091770E.7000205@cs.bham.ac.uk>
*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.*