Discussion:
[isabelle] Cantor's Theorem
(too old to reply)
Makarius
2016-01-01 21:36:02 UTC
Permalink
Raw Message
To test the slightly updated HTML presentation in Isabelle2016-RC0 here is
an updated proof of Cantor's Theorem in HOL:

http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Cantor.html

It is a return to plain reasoning, ignoring special tricks from the early
1990s to make it work "automagically".


As a proof of the elementary nature of the theorem in Higher-Order Logic,
here is also a version based on Pure + basic HOL:
http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Higher_Order_Logic.html
(subsection ‹Cantor's Theorem›). No automated reasoning tools are
available at that point. Not even the classical rule.


Technical remark: in these HTML pages the IsabelleText font is provided by
the server. So it should (in theory) work out everywhere without Unicode
dropouts. It should look exactly like in jEdit (not Isabelle/jEdit,
because the semantic markup is missing).


Makarius
Jan Burse
2017-04-25 11:29:59 UTC
Permalink
Raw Message
Are there any plans for a proof extraction component for
any of the automatic proof strategies? Like "why" directive

that would execute the proof slower, because of extracting
proof, but in the end show the proof?

In some CAS system step-by-step explanations seem to be
very common, here is an example:

https://www.symbolab.com/solver/derivative-calculator//frac%7Bd%7D%7Bdx%7D/left%28sin/left%28x/right%29%5E%7B2%7D/right%29
Post by Makarius
To test the slightly updated HTML presentation in Isabelle2016-RC0 here is
http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Cantor.html
It is a return to plain reasoning, ignoring special tricks from the early
1990s to make it work "automagically".
As a proof of the elementary nature of the theorem in Higher-Order Logic,
http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/library/HOL/HOL-Isar_Examples/Higher_Order_Logic.html
(subsection ‹Cantor's Theorem›). No automated reasoning tools are
available at that point. Not even the classical rule.
Technical remark: in these HTML pages the IsabelleText font is provided by
the server. So it should (in theory) work out everywhere without Unicode
dropouts. It should look exactly like in jEdit (not Isabelle/jEdit,
because the semantic markup is missing).
Makarius
Loading...