*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] A proof on moreover and ultimately*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 29 Dec 2015 14:16:38 +0100*In-reply-to*: <7cde3e5964ac8e6b5f04742243631a8e@cam.ac.uk>*References*: <6524ebdc76fa4e23a8cb4fabdd95b600@EX01.ios.ac.cn> <7cde3e5964ac8e6b5f04742243631a8e@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.4.0

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

**Follow-Ups**:**Re: [isabelle] A proof on moreover and ultimately***From:*Makarius

**References**:**[isabelle] A proof on moreover and ultimately***From:*李勇坚

**Re: [isabelle] A proof on moreover and ultimately***From:*Wenda Li

- Previous by Date: Re: [isabelle] A proof on moreover and ultimately
- Next by Date: Re: [isabelle] A proof on moreover and ultimately
- Previous by Thread: Re: [isabelle] A proof on moreover and ultimately
- Next by Thread: Re: [isabelle] A proof on moreover and ultimately
- Cl-isabelle-users December 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list