Re: [isabelle] sets in HOL/CF



Am 02.09.2010 um 21:59 schrieb Alexander Krauss:

> Brian Huffman wrote:
>> If you want to be able to define a function of type "nat -> nat set"
>> with fixrec, it turns out that fixrec can do it, but it requires you
>> to do some work to set things up first.
> 
> A related remark: A recursive function that returns a set can also be defined using the inductive(_set) package. You have to rephrase the definition using introduction rules, and manually derive the recursive equations afterwards, but that is usually straightforward.

Actually, Lukas's newly introduced "inductive_simps" command makes it easier than ever to derive recursive equations from inductive definitions. I think it's in Isabelle2009-2. I'm not aware of any documentation (beyond a few uses in Isabelle theories, which you can grep for) but it works pretty much like "inductive_cases".

Jasmin






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