Re: [isabelle] Verify the legitimacy of a proof?

On 08/07/2017 13:30, Makarius wrote:
On 08/07/17 13:01, Manuel Eberl wrote:
Unfortunately, it is very easy to circumvent this. I don't recall who
found this originally, but you can hide the âtaintâ of a theorem by
going through a type class instantiation:

"Found this originally" sounds very funny to me.

Of course, the problem of oracles vs. type classes instantiations is as
old as oracles and type class instantiations in Isabelle. It is rather
well-known for insiders.

I am sure Manuel meant no disrespect. No doubt you were aware of this behaviour from the start.

So we are back to the new meta-problem from recent years: even power
users don't know anymore what Isabelle is and what it does, and
especially what it does not.
It is usually due to a fanciful interpretation of the documentation. The latter says that "The system always records oracle invocations within derivations of theorems by a unique tag." but does not claim that these tags are also always inherited in the way one is all too likely to assume. There you are, Manuel.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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