Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Set vs FSet for transitive closure of finite r...

Email Gateway (Aug 22 2022 at 15:13):

From: "S.J.Cooksey" <sjc205@kent.ac.uk>
Hello,

I think this is a question of taste. I'm doing some research with
Isabelle, and require defining my own transitive closure function. For
the termination proof of this function it seems desirable to pull out a
finite domain of the relation being closed.

Is it better to make the type of transitive closure something like

trans_clos:: "'a fset => ('a => 'a => bool) => 'a => 'a => bool"

or to use non-finite sets and prove finiteness for the given concrete
inputs.

Many thanks,

Simon Cooksey

Last updated: Apr 27 2024 at 04:17 UTC