*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Quotients of nominal types*From*: Aleks Kissinger <aleks0 at gmail.com>*Date*: Tue, 13 Aug 2013 14:23:27 +0100*Cc*: Christian Urban <christian.urban at kcl.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1308121749110.16959@macbroy21.informatik.tu-muenchen.de>*References*: <CAJGV=ubzhS4=8M1M7hrNVmEVpZg+aEqHokY7yrAdPaT=52EBwg@mail.gmail.com> <m2ob93s6il.fsf@kcl.ac.uk> <alpine.LNX.2.00.1308121528280.28307@macbroy21.informatik.tu-muenchen.de> <m2a9knrnvl.fsf@kcl.ac.uk> <alpine.LNX.2.00.1308121749110.16959@macbroy21.informatik.tu-muenchen.de>

Thanks for your feedback. A the moment, it looks like the best solution is to keep the explicit congruence around. Simple proofs seem to take approximately this shape: theorem A ~~ B proof - have A ~~ A' by (* alpha-equivalence + ~~ reflexive *) also have ... ~~ B' using (* some algebraic rule *) by blast also have ... ~~ B by (* alpha-equivalence + ~~ reflexive *) finally show ?thesis . qed Perhaps this can be improved, but this seems to work okay for my purposes. The thing I have in mind is to write various tactics which produce many such proof steps using some meta-reasoning (in this case, a diagram representation and some rewriting techniques for the expressions A and B). On 12 August 2013 16:54, Makarius <makarius at sketis.net> wrote: > On Mon, 12 Aug 2013, Christian Urban wrote: > >> So we can talk about Isabelle/ML and be very grateful that it is so >> smoothly >> integreated with everything else. But the fact remains that almost all >> people >> who want to learn Isabelle do not want to learn anything about ML and its >> poorly documented infrastructure that is called Isabelle distribution. > > > Using Isabelle/ML is definitely not trivial, but it is much easier than it > used to be several years ago, and the official documentation is continously > getting more and more complete, although rather thick now. It is also much > better than Coq, for example, where the reader of the sources also needs to > know some French, not just OCaml. > > Getting basic terminology right is only the starting point, it is necessary > but not sufficient for what follows for those Isabelle users who want to > embark on building their own tools for the platform. > > > Makarius >

**References**:**[isabelle] Quotients of nominal types***From:*Aleks Kissinger

**Re: [isabelle] Quotients of nominal types***From:*Christian Urban

**Re: [isabelle] Quotients of nominal types***From:*Makarius

**Re: [isabelle] Quotients of nominal types***From:*Christian Urban

**Re: [isabelle] Quotients of nominal types***From:*Makarius

- Previous by Date: Re: [isabelle] match_tac, schematic and bound variables
- Next by Date: Re: [isabelle] List.span
- Previous by Thread: Re: [isabelle] Quotients of nominal types
- Next by Thread: Re: [isabelle] "show" taking very long with goals with many hypothesis
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list