Email Gateway (Aug 19 2022 at 08:55): Email Gateway (Aug 19 2022 at 08:55):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
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"?
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
Email Gateway (Aug 19 2022 at 08:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christoph,
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"?
No, there isn't (yet). In Library/Bit.thy, there is an isomorphic type
of bits 0/1, which might be helpful in your case also.
BTW, is there a way of searching for definitions of a given type,
similar to find_theorems?
find_consts is your friend.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:14):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Apr 26 2024 at 16:20 UTC