[isabelle-dev] Nominal and FinFuns from the AFP

[Lukas Bulwahn]

Hi Christian,


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 
direction.

As Andreas has access to the Isabelle development and can freely change 
and contribute the entry, I do not see any further difficulties.


Lukas


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,
> Christian
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev