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.


Cheers,

Manuel



On 29/12/15 14:00, Wenda Li wrote:
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

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
----------------------------------
  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





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