Alex Weisberger (Sep 04 2022 at 16:21): Alex Weisberger (Sep 04 2022 at 16:21):The first question would be, is a theorem considered proven when a theorem definition is listed in the output?
I ran into this in a more complicated example, but here's a simplified one:
theorem contradiction: "n = Suc n"
proof(induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case by auto
qed
Obviously this is not true, and the 0 case fails to get marked as proven. However, when my cursor is over the qed, I see the following output:
theorem ?n = Suc ?n
And the theorem is output when I use the thm command as well. I thought this output is only produced when the proof is actually proven? There's also no error shown on the final qed, just in the bad case. Is this expected?
Mathias Fleury (Sep 05 2022 at 04:27):Isabelle is optimistic (which is necessary in order to be able to do stuff in parallel): it assumes that the proof steps above finished (so no purple running forever tactics) and were error-free
Alex Weisberger (Sep 05 2022 at 15:18):Thanks. The error is obvious in this case, though it is a little scary for larger proofs since it’s easier for those errors to get lost.
I wonder if there’s a setting to control that, for example to prevent publishing a theory with an error that someone else consumes.
Lukas Stevens (Sep 05 2022 at 15:22):If you build your session with isabelle build, the build will fail.
Last updated: Apr 24 2024 at 20:16 UTC