[isabelle] Converting bool to {0,1}

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 Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)

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