Re: [isabelle] value gcd



Dear Walther,

You have not yet proven that your function definition terminates. Therefore, the defining equation (gcd.psimps) still carries the precondition that the function terminates. The code generator cannot handle such preconditions, so these psimps equations are not registered as code equations. Once you have proved termination, the function package derives the unconditional equations gcd.simps from the conditional ones and registers them with the code generator. Everything should work fine then.

You can find out what is happening by inspecting the code equations for gcd with the command

  code_thms gcd

You will see that there are not equations registered.

Best,
Andreas

On 29/09/15 11:33, Walther Neuper wrote:
Given ...

   theory Demo imports Main
   begin
     function gcd :: "int => int => int"
       where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
     by auto
     value "5 mod 3::int"
       --{*evaluates to "2" :: "int"*}
     value "gcd 123456 7890::int"
       --{*evaluates to "Demo.gcd 123456 7890" :: "int"*}
   end

... why does "gcd" not evaluate, although "mod" evaluates?

Walther

PS: And how find an answer to such a question myself?





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