Re: [isabelle] Quotients of nominal types



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
>




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