[isabelle-dev] Nominal and FinFuns from the AFP
bulwahn at in.tum.de
Thu May 10 19:46:04 CEST 2012
For code generation purposes and especially Quickcheck, it is necessary
that the FinFun theory would be imported by any user.
With the new developments lifting and transfer, we are getting very
close that FinFun can be used without any further ado.
I do have some latest experiments and patches in the shelf to be
published after the release.
Therefore, I am also in strong favour for moving the AFP entry FinFun
into the distribution.
In the long run, it should probably even become part of the HOL-Main image.
In the short term, we could move the FinFun theory into the HOL library
of the development version after Isabelle 2012 and the AFP 2012 has been
released, if we agree that this moves this contribution in the right
As Andreas has access to the Isabelle development and can freely change
and contribute the entry, I do not see any further difficulties.
P.S.: The topic is interesting for isabelle-users as well in my opinion.
On 05/10/2012 05:09 PM, Christian Urban wrote:
> Dear All,
> In Nominal I am usually relying on types that are defined
> in HOL or that I define myself. However, I now came across
> the FinFun development in the AFP by Andreas Lochbihler (thanks
> to Larry). The finfun type seems to be rather useful to Nominal
> users, since it has finite support, in contrast to the function
> type, which in general hasn't.
> My question is how I should I interface with something that
> is in the AFP and with something that is (eventually) in the
> distribution? The problem is that Nominal always needs a wrapper
> infrastructure for types, such as a definition of a permutation.
> How should I write this wrapper, especially what should the import
> paths be, so that users can conveniently use FinFuns and Nominal?
> Should this wrapper be part of the AFP entry (in which case
> the paths are clear, but then Nominal users have to fetch the
> AFP explicitly and no Nominal example in the distribution can
> depend on it)?
> Or should the wrapper be part of Nominal (in which case I
> can use it in examples, but I have no idea what the import
> paths should be...the AFP can be anywhere)?
> Or, should FinFun be part of the distribution (which would
> make my life normal again)?
> Is there any received wisdom for this problem?
> Best wishes,
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev