Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 19 2022 at 15:23):

From: Joachim Breitner <breitner@kit.edu>
Hi,

not sure if they are helpful, but “real world examples” from someone not
developing Nominal2 can be found at
http://darcs.nomeata.de/isa-launchbury/Launchbury/

In particular after having defined a few functions over my expr type
defined in Terms.thy, I created a lemma (eqvt_lam_case and
eqvt_let_case, also in Terms.thy) that included all the boring stuff and
reduced the number of variables I have to talk about. I ugess it is my
own variant of the _FCB lemmas (which I didn’t figure out how to use
succesfully).

Greetings,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 15:24):

From: Dominic Mulligan <dominic.p.mulligan@googlemail.com>
Dear Joachim,

Thanks for the pointer to your development. It looks like it will come in
useful.

Thanks,
Dominic

view this post on Zulip Email Gateway (Aug 19 2022 at 15:43):

From: Dominic Mulligan <dominic.p.mulligan@googlemail.com>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 15:45):

From: Christian Urban <christian.urban@kcl.ac.uk>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 15:46):

From: Dominic Mulligan <dominic.p.mulligan@googlemail.com>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 15:47):

From: Christian Urban <christian.urban@kcl.ac.uk>
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@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

--

Last updated: Nov 21 2024 at 12:39 UTC