Email Gateway (Jul 21 2026 at 16:27): Email Gateway (Jul 21 2026 at 16:27):From: Tobias Nipkow <nipkow@in.tum.de>
The transitive reflexive closure ^* on relations is not executable simply
because of reflexivity, which result is an infinite relation if the base type is
infinite. In contrast, the transitive closure ^+ is executable.
Here is a proposal of how to make ^* executable in specific contexts. We start
with "R^* `` A":
lemma rtrancl_Image_code[code_unfold]: "R^* A = R^+ A ∪ A"
by (metis Image_Id Un_Image reflcl_trancl)
Now terms of the form "R^* `` A" are executable (if R and A are finite).
This helps some, but related situations still pose a problem, eg "(R^*)^-1 `` A"
is not covered. Luckily, another lemma helps:
lemma rtrancl_converse_code[code_unfold]: "(R^*)^-1 A = (R^+)^-1 A ∪ A"
by (metis rtrancl_Image_code rtrancl_converse trancl_converse)
For my particular situation, this does the job. However, it looks like one may
end up with a lot of special case code_unfold lemmas.
Alternatively, one could define a special case of R^* that is reflexive only on
the elements already present in R. Using that alternative may require more
manual adjustments. But since one needs to prove most code equations manually
anyway, maybe that's the way to go.
Comments?
Tobias
Last updated: Jul 22 2026 at 14:00 UTC