Re: [isabelle] A proof on moreover and ultimately

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.


On 2015-12-29 06:00, æåå wrote:
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
  {assume "case1"
  have "?P"

  {assume "case162"
  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

yongjian Li

Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.