Re: [isabelle] Using Nominal Isabelle in Isabelle2013/2014



Dear Christian,

Thanks for your speedy reply.  I'll try and convert my development to
Nominal2 in that case.  Is there any sort of manual or user guide on using
the new package?  From my brief browsing of the examples supplied the
amount of work one needs to do to define functions in Nominal2 is
significantly higher than in Nominal1---is there any guidance on the new
tactics/theorems supplied to help close these obligations?

Thanks,
Dom


On 1 August 2014 10:26, Christian Urban <christian.urban at kcl.ac.uk> wrote:

>
> Hi Dominic,
>
> I would recommend using Nominal2 (either from the webpage
> or even from the AFP). Nominal_function throws up some
> proof obligations, which cannot be discharged by just using
> pat_completeness. In the binder cases you have to use
> *_FCB lemmas, which is substantially harder than the
> "usual" pattern. In addition you have to show equivariance
> for your function. If you send me an example of what you
> want to define, I am happy to have a look.
>
> Best wishes,
> Christian
>
>
> On Friday, August 1, 2014 at 10:16:37 (+0100), Dominic Mulligan wrote:
>  > Hi,
>  >
>  > Is it recommended that one uses Nominal2 or the original Nominal package
>  > with the latest version of Isabelle?  Nominal2 does not seem to have as
>  > much documentation (or automation, from my brief attempt to use it), is
>  > described as "alpha-ware" on the project website, and is not distributed
>  > with the standard Isabelle distribution.
>  >
>  > On the other hand, I'm trying to use the Nominal package as distributed
> in
>  > Isabelle2014-RC1 and coming unstuck trying to define a function over a
>  > nominal datatype using the "function" package that cannot be hammered
> into
>  > a nominal_primrec easily, and having trouble closing the generated proof
>  > obligations, with various exceptions being thrown by Isabelle (for
> example,
>  > pat_completeness fails with a dest_eq exception).
>  >
>  > So, now I'm wondering whether I'm doing something wrong, whether I've
> come
>  > across a bug, or whether I'm just using software that is now deprecated
>  > (the original Nominal package), and shouldn't be used with current
> versions
>  > of the system.
>  >
>  > Thanks,
>  > Dominic
>
> --
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.