Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Tjark Weber <tjark.weber@gmx.de>
Nicole,
when Isabelle can't prove your goal, it may be able to disprove it: both
"quickcheck" and "refute" find simple counterexamples to your conjectures.
(As Larry already explained, the reason why these are not theorems is that the
quantifier !! extends over the whole statement, not just over the premises of
the implication).
Best regards,
Tjark
Email Gateway (Aug 17 2022 at 13:27):From: Lawrence Paulson <lp15@cam.ac.uk>
I think you are interpreting the formulas incorrectly. The first
subgoal requires showing that if P(N) holds for some positive integer
N, then P(1) holds. The second requires showing that if P(N) holds
for some positive integer N, and M is also a positive integer, then P
(M).
Larry Paulson
Last updated: May 03 2024 at 01:09 UTC