*To*: Makarius <makarius at sketis.net>, Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Understanding backtracking in by vs qed*From*: Joshua Chen <joshua.chen at uibk.ac.at>*Date*: Sat, 23 Mar 2019 11:43:25 +0100*In-reply-to*: <acedd452-8dfd-59c4-ba08-1e70902d10d6@sketis.net>*References*: <9900e999-47f3-56c6-8f06-3f19d409ff58@uibk.ac.at> <acedd452-8dfd-59c4-ba08-1e70902d10d6@sketis.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.5.3

The 'by' step can enumerate all possibilities for the initial proofmethod (move, infer_ty) and then try the auto step and then finish(which is implicit). The proof-qed sequence only uses the firstpossibility of 'proof' and 'qed' needs to finish that without furtherbacktracking.

Other things might go wrong here, as this sounds somewhat non-standard.

Best, Josh On 3/23/19 11:38 AM, Makarius wrote:

On 22/03/2019 17:53, Joshua Chen wrote:I have a proof that works: have <statement> using <facts> proof (move, infer_ty) qed (auto simp: ty) and one that doesn't: have <statement> using <facts> by (move, infer_ty) (auto simp: ty) The manual says that "by" abbreviates "proof ... qed" but with additional backtracking, what is it about this that could cause "by" to fail and "qed" to succeed?The 'by' step can enumerate all possibilities for the initial proof method (move, infer_ty) and then try the auto step and then finish (which is implicit). The proof-qed sequence only uses the first possibility of 'proof' and 'qed' needs to finish that without further backtracking. You can try to put a few 'back' commands between 'proof' and 'qed' above, to see if relevant alternative states emerge in between.I'm unsure if it would be relevant, but infer_ty is a method that only changes the proof context (by adding some theorems to context data) without changing the goal.Other things might go wrong here, as this sounds somewhat non-standard. Makarius

**Follow-Ups**:**Re: [isabelle] Understanding backtracking in by vs qed***From:*Makarius

**References**:**[isabelle] Understanding backtracking in by vs qed***From:*Joshua Chen

**Re: [isabelle] Understanding backtracking in by vs qed***From:*Makarius

- Previous by Date: Re: [isabelle] Understanding backtracking in by vs qed
- Next by Date: Re: [isabelle] Understanding backtracking in by vs qed
- Previous by Thread: Re: [isabelle] Understanding backtracking in by vs qed
- Next by Thread: Re: [isabelle] Understanding backtracking in by vs qed
- Cl-isabelle-users March 2019 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