Re: [isabelle] A proof on moreover and ultimately
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.
On 29/12/15 14:00, Wenda Li wrote:
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.
On 2015-12-29 06:00, æåå wrote:
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
ultimately show âïP"
all 162 moreovers are finished, but the last ultimately command cann't
why? is there is a limit on the number of subcases (moreovers)?
The proof is in the on_inis.thy, which is attached
This archive was generated by a fusion of
Pipermail (Mailman edition) and