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



Dear Dominic,

No there is no documentation apart from the examples. Yes, 
nominal_functions are harder to define, but it allows you to 
define more functions. So if you had problems with nominal_primrec 
in Nominal1, chances are you can define the function with nominal_function.

Best wishes,
Christian 

On Friday, August 1, 2014 at 10:31:44 (+0100), Dominic Mulligan wrote:
 > 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.