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



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.