Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] value gcd


view this post on Zulip Email Gateway (Aug 22 2022 at 11:21):

From: Walther Neuper <wneuper@ist.tugraz.at>
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?

view this post on Zulip Email Gateway (Aug 22 2022 at 11:21):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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


Last updated: Nov 21 2024 at 12:39 UTC