*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] A bug in chained proof mode*From*: Eddy Westbrook <westbrook at kestrel.edu>*Date*: Wed, 11 Jun 2014 10:15:42 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <53984646.1010603@gmail.com>*References*: <AEAA6C7E-C502-46EA-821C-1872106C56CB@kestrel.edu> <53984646.1010603@gmail.com>

All, Thanks for the replies! I understand more about the chained mode now, and will use your suggestions. Thanks again, -Eddy On Jun 11, 2014, at 5:06 AM, Christian Sternagel <c.sternagel at gmail.com> wrote: > Dear Eddy, > > this actually is the intended behavior, the reason of which is explained in: > > G. Bauer and M. Wenzel. Calculational reasoning revisited - an > Isabelle/Isar experience. In R. J. Boulton and P. B. Jackson, editors, > Theorem Proving in Higher Order Logics: TPHOLs 2001, volume 2152 of > Lecture Notes in Computer Science. Springer-Verlag, 2001. > > According to the isar-ref manual (see Section 2.2.4 "Calculational reasoning") your example would translate into > > assume "e1 = e2" > have "f e1 = f e2" ... > note calculation = this (* "f e1 = fe2" *) > have "f e2 = f e2" ... > note calculation = <TRANS> [OF calculation this] (* "f e1 = f e2" *) > from calculation > have "f e1 = f e2" > > where the crucial spot is <TRANS>. That is, the actual content of "calculation" depends on the chosen rule. And as explained in the above paper this is done by trying all declared (via [trans] and [sym]; those can be consulted via "print_trans_rules") lemmas while discarding results that are mere projections. > > cheers > > chris > > Btw: *wispered* you should be careful when throwing around words like "bug" ;) > > On 06/11/2014 07:03 AM, Eddy Westbrook wrote: >> Hi, >> >> I think I have found a bug in the chained proof mode, that occurs for equality proofs if one of the proof used in the chain is a reflexive proof. As an example, the following proof fails, even though (as far as I understand the chain mode) it should succeed: >> >> lemma chain_bug: "e1 = e2 ⟹ f e1 = f e2" >> proof - >> assume eq1: "e1 = e2" >> have "f e1 = f e2" by (rule arg_cong[OF eq1]) >> also >> have "f e2 = f e2" by (simp) >> finally >> have "f e1 = f e2". >> qed >> >> Although it may seem silly to write a proof that “f e2 = f e2”, the reason it comes up is that the proof is machine-generated, and sometimes it is easier to generate a proof that something equals itself rather than checking explicitly for that fact. >> >> Anyway, just thought I would report this. >> >> Thanks, >> -Eddy >> >

**References**:**[isabelle] A bug in chained proof mode***From:*Eddy Westbrook

**Re: [isabelle] A bug in chained proof mode***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] isabelle build -vb runs out of store
- Next by Date: Re: [isabelle] Cygwin Isabelle2014 sledgehammer libwww-perl missing
- Previous by Thread: Re: [isabelle] A bug in chained proof mode
- Next by Thread: [isabelle] Cygwin Isabelle2014 sledgehammer libwww-perl missing
- Cl-isabelle-users June 2014 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