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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and