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



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.