Re: [isabelle] *_sumC generated by function package



How does your proof look like?

Do you use make_prims_def ? <func>_def should be only used internally,
to unfold the function you should use make_prims.simps. The ...simps
rules are the one you use in your function specification.

 - Johannes

Am Montag, den 21.01.2013, 18:13 +0100 schrieb Walther Neuper:
> 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.







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