*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] apply x apply y vs. by x y*From*: Makarius <makarius at sketis.net>*Date*: Thu, 3 Sep 2015 10:24:49 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <55B694F5.4000104@in.tum.de>*References*: <55B694F5.4000104@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 27 Jul 2015, Lars Hupel wrote:

I have a proof state which can be solved by the subsequent application of two methods, i.e. have "P x" apply (induct x) apply auto done If I rewrite this to have "P x" by (induct x) auto the proof fails. Unfortunately I haven't been able to distill a small example exhibiting this behaviour. Now, I know that "by x y" is equivalent to "proof x qed y", but I always thought that is in turn equivalent to "apply x apply y". Funnily enough, "by (x, y)" works. The chained facts appear not to be significant here (I tried some variations).

(Back to this old thread.)

In principle the following equivalences of proof snippets hold: by method1 method2 == apply method1 apply method2 . == apply method1 apply method2 apply assumption* done

Makarius

- Previous by Date: [isabelle] Usability for light-on-dark color schemes
- Next by Date: Re: [isabelle] Problem with quickcheck in Isabelle2015
- Previous by Thread: [isabelle] Usability for light-on-dark color schemes
- Next by Thread: [isabelle] Case names qualified by locale
- Cl-isabelle-users September 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