Email Gateway (Aug 22 2022 at 12:06): Email Gateway (Aug 22 2022 at 12:06):From: 李勇坚 <lyj238@ios.ac.cn>
Dear experts:
I meet a problem on a proof of a typical case analysis, whose structure is as follows:
have "case1 \or case2 \or ....\or casen" by auto
moreover
{assume "case1"
proof_1
have "?P"
}
......
moreover
{assume "case162"
proof_n
have "?P"
}
ultimately show “？P"
all 162 moreovers are finished, but the last ultimately command cann't be finished?
why? is there is a limit on the number of subcases (moreovers)?
The proof is in the on_inis.thy, which is attached
regards!
yongjian Li
duanCubData.zip
Email Gateway (Aug 22 2022 at 12:06):From: Wenda Li <wl302@cam.ac.uk>
Hi Yongjian,
You can try "try0" in the end. In my computer, Isabelle2015 gives "by
satx" and "by fastforce". I guess the problem with auto in your case is
that it tries to simplify the large number of assumptions.
Cheers,
Wenda
Email Gateway (Aug 22 2022 at 12:06):From: Manuel Eberl <eberlm@in.tum.de>
I would like to add that this looks like a classic use case of
Isabelle2016's ‘consider’ syntax. This approach avoids the ‘big bang
integration’ at the end.
Then you can write ‘consider … | … | … by …’ to prove the validity of
your case splitting and then write ‘hence … proof cases’ to get all the
different cases as separate proof obligations.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:06):From: Makarius <makarius@sketis.net>
Indeed.
A special test version for Christmas is available here:
http://www4.in.tum.de/~wenzelm/test/Isabelle_23-Dec-2015/
Official release candidates for Isabelle2016 will be published next year;
stay tuned.
Makarius
Email Gateway (Aug 22 2022 at 12:18):From: Makarius <makarius@sketis.net>
See http://isabelle.in.tum.de/website-Isabelle2016-RC0
Makarius
Last updated: Apr 18 2024 at 12:27 UTC