[isabelle] *_sumC generated by function package



First steps with the function package were successful.

Now I don't know how to remove a proof obligation containing a function constant named 'function_id_sumC', where 'function_id' is the function under consideration:

 2. ?primes last_p n primesa last_pa na.
       (primes, last_p, n) = (primesa, last_pa, na) ?
       (if primes ! (length primes - 1) < n
        then
            if is_prime primes (last_p + 2)
            then make_prims_sumC (primes @ [last_p + 2], last_p + 2, n)
            else make_prims_sumC (primes, last_p + 2, n) else primes) =
       (if primesa ! (length primesa - 1) < na
        then
            if is_prime primesa (last_pa + 2)
then make_prims_sumC (primesa @ [last_pa + 2], last_pa + 2, na)
            else make_prims_sumC (primesa, last_pa + 2, na)
        else primesa)

Why did the function package generate this 'function_id_sumC' ?
And how can I prove the proof obligation ?

Thanks for your help,
Walther

PS: The function definition is in the attachment.

Attachment: GCD_1_Make_Primes.thy
Description: application/extension-thy



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