*To*: noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] some problems with the /\ quantifier*From*: Lars Hupel <hupel at in.tum.de>*Date*: Sun, 13 Sep 2015 11:02:43 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAGOKs0_YyEvN39x-UXL6jnofDj-A2pfo35qsGxn6KSNCBKwUjA@mail.gmail.com>*References*: <CAGOKs09PRLE1E97Sw9ri493tdjA8G3vRMAMYyWm+TBf0nfxVuA@mail.gmail.com> <55F50825.9020104@in.tum.de> <CAGOKs0_YyEvN39x-UXL6jnofDj-A2pfo35qsGxn6KSNCBKwUjA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

> 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:*noam neer

**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

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