Re: [isabelle] My unforgivable soundness issue with a locale



Le Sun, 22 Dec 2013 21:33:30 +0100, Peter Lammich <lammich at in.tum.de> a écrit:
inside the locale, you can prove everything you expect with A (and much
more ;) ). Only when interpreting the locale you will realize the
mistake.

That's what I would like to avoid, as I would like to be able to predict such issues. I'm still investigating the case, as the problem finally remains unsolved: adding the premiss directly in the proposition did not solve everything.

Some sanity theorems may help (successful in one case at least), but I don't know any kind of general theorem which could assert there is no possible contradictions. I guess this is feasible, as that must be something close people do when they check a logic is sound and claim they proved it.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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