Email Gateway (Aug 18 2022 at 09:43): Email Gateway (Aug 18 2022 at 09:43):From: Dimitrios Vytiniotis <dimitriv@cis.upenn.edu>
Hello all, consider the (admittedly strange) fragment:
datatype tm = Z | S "tm"
consts foo :: "tm => tm set"
recdef foo "measure size"
"foo x = { Z. (x = Z) } \<union>
{ (S x1) | x1. x = S x1 /\ x1 : (foo x1) }";
Isabelle cannot prove monotonicity, because the equation "x = S x1"
seems to not be available. In particular, she tries to prove to me that:
forall x1. size x1 < size x
instead of:
forall x1. (x = S x1) --> (size x1 < size x)
Why is this happening? Why aren't the rest of the equations in the
comprehension used to derive the monotonicity requirement? Here's my
explanation:
Such a thing would still be sound. Because if the "x = S x1" was false
no call to "foo x1" would have to be done and hence no monotonicity
check would be necessary. The whole predicate (x = S x1 /\ x1: foo x1)
would be false and the particular set component empty. But the problem
would be that checking that the predicate is false would require in the
general case validating the predicate in a particular order (one that
does not attempt to run foo first) and perhaps there's no internal
mechanism in Isabelle to do such a thing. Is this the reason? Or is such
a thing not sound alltogether? It would be nice if such a definition was
possible.
Thanks!
--dimitris
ps: I know that I can rewrite the function in other ways that will make
it work but I really want to keep this style (basically because with
this style I do not have to write explicit pattern match cases for
fail-through cases---when the predicate fails, the set is empty and
that's it)
Email Gateway (Aug 18 2022 at 09:43):From: Stefan Berghofer <berghofe@in.tum.de>
Dimitrios Vytiniotis wrote:
Hello,
by declaring the congruence rule for conjunction via
declare conj_cong [recdef_cong]
before invoking recdef, you can instruct Isabelle to use the
equation "x = S x1" when proving the termination condition for
"x1 : (foo x1)". With the above declaration, the termination
proof for "foo" is completely automatic.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 09:43):From: Alexander Krauss <krauss@in.tum.de>
Dimitrios,
Also note that in the first comprehension, Z is parsed as a bound
variable ("The set of all Z, where x equals Z"). Is this really what you
want?
Alex
Last updated: May 03 2024 at 08:18 UTC