*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] some problems with the /\ quantifier*From*: noam neer <noamneer at gmail.com>*Date*: Fri, 18 Sep 2015 08:16:29 +0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <55F53BB3.9030101@in.tum.de>*References*: <CAGOKs09PRLE1E97Sw9ri493tdjA8G3vRMAMYyWm+TBf0nfxVuA@mail.gmail.com> <55F50825.9020104@in.tum.de> <CAGOKs0_YyEvN39x-UXL6jnofDj-A2pfo35qsGxn6KSNCBKwUjA@mail.gmail.com> <55F53BB3.9030101@in.tum.de>

does this problem happen whenever the /\ quantifier is involved, or just when automatic names are generated? for example if I use apply(induct n) will I be able to use 'n' with all the methods? On Sun, Sep 13, 2015 at 12:02 PM, Lars Hupel <hupel at in.tum.de> wrote: > > 2. this is a nice solution, but why do methods differ with this respect? > > this is very confusing. > > No, it is not a nice solution. These methods are "improper", which means > they are still supported but you should refrain from using them. They > are really nice for exploring proofs, but as I said, it is much better > to rewrite such proofs afterwards. See also Â9.2.3 from the Isar > Reference Manual. > > > 3. I admit this proof isn't robust with respect to variable names, but > this > > can be solved with 'rename_tac', as explained in the documentation. your > > recommended solution uses 'auto' which I try not to use too much because > > I'm not sure what exactly it is doing, and I prefer simple commands like > > [of ...] or 'rule_tac' for this reason. I guess this is also a kind of > > robustness consideration. > > 'rename_tac' might make your proof more robust, but it does not improve > readability at all. > > The precise methods to use were not the main point of my recommendation; > rather that instantiations and eliminations often are much more elegant > in Isar style. If you don't want to use 'auto', 'rule' would also work > in that situation: > > from assms obtain z where "w = real_of_int z" > by (rule Ints_cases) > > By the way, because of the LCF nature of Isabelle, there is no harm in > using 'auto' even if you don't understand what it's doing. In fact, > automated tactics are very often more robust than low-level proofs > because they are not as sensitive to details. > > Cheers > Lars >

**Follow-Ups**:**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Noschinski

**References**:**[isabelle] some problems with the /\ quantifier***From:*noam neer

**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Hupel

**Re: [isabelle] some problems with the /\ quantifier***From:*noam neer

**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Hupel

- Previous by Date: [isabelle] Isabelle error
- Next by Date: Re: [isabelle] some problems with the /\ quantifier
- Previous by Thread: Re: [isabelle] some problems with the /\ quantifier
- Next by Thread: Re: [isabelle] some problems with the /\ quantifier
- 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