Re: [isabelle] *_sumC generated by function package



On 01/21/2013 06:13 PM, Walther Neuper wrote:
Why did the function package generate this 'function_id_sumC' ?

Here, unfortunately, the internal encoding shines through. In your concrete case, the currying was converted to tuples, in other cases, several mutual recursive functions may be converted to a function on a sum type (hence the suffix).

In your concrete case, the simplifier loops because the equation for is_prime loops in the presence of the usual splitting of ifs.
Thus, "by pat_completeness (simp del: is_prime.simps)" does the trick here.

In general, you cannot prove much about the _sumC functions. The goals are usually provable when treating them as uninterpreted.

Alex





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