*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] some problems with the /\ quantifier*From*: noam neer <noamneer at gmail.com>*Date*: Fri, 18 Sep 2015 13:00:43 +0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <55FBA1BC.9060001@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> <CAGOKs0-RRpTOfF3QAvY3f0BZu-gwKDc3k6iW2k083Yi864J0gQ@mail.gmail.com> <55FBA1BC.9060001@in.tum.de>

OK, I just tried the Isar form of induction that starts with proof (induction n) and when I reached case (Suc n) it seems there are still problems. the 'n' has different color and the simplifier doesn't work properly. so, what should I do if I want to use the induction variable? what is the parallel of 'obtain'? On Fri, Sep 18, 2015 at 8:31 AM, Lars Noschinski <noschinl at in.tum.de> wrote: > On 18.09.2015 07:16, noam neer wrote: > > does this problem happen whenever the /\ quantifier is involved, > > or just when automatic names are generated? > > Proof methods (and attributes like of, where) can usually only address > free variables -- the reason being that bound variables have no meaning > outside the subterm they were bound in. > > They are a few older methods (the "_tac" family), which have special > code to match names with bound variables. > > -- 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

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

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

- Previous by Date: Re: [isabelle] a new power operator
- 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