[isabelle] proving the substitution lemma
I'm new to Isabelle and Coq.
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-
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.
PS: I was wondering if there is a Coq package and/or
project similar to the 'isabelle-nominal' ones.
moez at rice.edu | www.cs.rice.edu/~moez | (713) 392-2844
"And you have been given of knowledge but little"
"Our knowledge can only be finite, while our ignorance
must necessarily be infinite." -Karl Popper
This archive was generated by a fusion of
Pipermail (Mailman edition) and