Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] size_changes raises Option and Bind

view this post on Zulip Email Gateway (Aug 18 2022 at 19:24):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
In Isabelle 2011-1, size_change raises the exception Option (line 81 in
general/basics.ML) and Bind (line 277 of termination.ML) for the following
function definitions. The NOT operator seems to cause the trouble, because
size_change (and lexicographic_order) work perfectly well when I unfold NOT i =
-i - 1.

This either seems like a bug in termination or some bad setup for NOT.

theory Scratch imports "~~/src/HOL/Word/Bit_Int" begin

function bits :: "int => nat"
where
"bits i =
(if i < 0 then bits (NOT i)
else if i = 0 then 0
else bits (i div 2) + 1)"
by(pat_completeness) auto
termination apply(size_change) (* raises Option *)

function bits :: "int => nat"
where
"bits i = (if i < 0 then bits (NOT i) else 0)"
by(pat_completeness) auto
termination apply(size_change) (* raises Bind *)

Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 19:25):

From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,

Thanks for reporting this. It is a bug in size_change (more precisely,
the dependency graph construction). Embarrasingly, the edges in the
graph seem to have the wrong direction, which got unnoticed several
years. This shows that size_change still isn't used/tested much.

I am preparing a fix.

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 19:26):

From: Alexander Krauss <krauss@in.tum.de>
Now done, in Isabelle/2d48bf79b725.

The correct behaviour is that in the first function, some progress is
made by removing one of the calls, and in the second function, nothing
can be done, because a priori, the termination prover knows nothing
about NOT. So unfolding it is probably a good idea. Note that you can do
this locally in the termination proof, e.g. by (lexicographic_order
simp: ...).

Alex

Last updated: Nov 21 2024 at 12:39 UTC