[isabelle] [nominal-isabelle] proving the substitution lemma
Moez A. Abdel-Gawad writes:
> However, my own personal attempt to prove the substitution
> lemma in Coq - with very minor resort to the variable con-
> vention and alpha-conversion equivalence - seemed to tell
> that the substitution lemma may not be the best example to
> use for *motivating* the need for the 'isabelle-nominal'
> package and project, as is done for example on this web-
> page http://isabelle.in.tum.de/nominal/main.html
I agree: The substitution lemma is not the most exciting
proof to formalise. On the other hand, it is very small
and everyone knows about it and about the issues. I like
it, since one can explain the nominal Isar-proof of this
lemma in 5 minutes to people who never have touched a
theorem prover in their lives. That is why I presented it
on the nominal web-page.
> While I do not discount the possibility of the package
> being useful - and even necessary - for other proofs, my
> experiment gave me the feeling that a much simpler app-
> roach may be possible (may be even as simple as adding a
> new tactic), which may work in fact for many similar pr-
> oofs as well, and - if not - is very likely to work at
> least for the purpose of proving the substitution lemma.
Would you mind sharing your proof? In the experience I obtained
with the nominal package is that the techniques (strong
induction principles) which we use to prove the substitution
lemma have proved most valuable in all formalisations we did
so far. Nowadays I would refuse to do any formalisation, if
I did not have them.
> PS: I was wondering if there is a Coq package and/or
> project similar to the 'isabelle-nominal' ones.
B. Aydemir, A. Bohannon and S. Weirich, Nominal Reasoning
Techniques in Coq. In Proc. of LFMTP 2006
and Xavier Leroy used some lightweight nominal techniques
in his solution of the PoplMark-challenge.
This archive was generated by a fusion of
Pipermail (Mailman edition) and