[isabelle] A proof on moreover and ultimately



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

Attachment: duanCubData.zip
Description: duanCubData.zip



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