Re: [isabelle] Proof by analogy and proof stability in Isabelle
Tobias Nipkow schrieb:
A possibility would also be to include the concept of lemma that can be
referenced into the
unpacked proof certificate, and include the proofs of required lemmas
only once. This
would make this certificate format slightly more complex, but avoid
explosion of the certificate
This is the killer, I believe:
"Moreover, if the proofs of intermediate lemmas will also be unpacked,
this proof would remain correct even if some intermediate lemmas
disappear in the new version!"
Otherwise replaying proofs is uncritical.
by preserving the modularity of the original proof.
This archive was generated by a fusion of
Pipermail (Mailman edition) and