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

Hello, > after which the goal is > > goal (1 subgoal): > 1. â z. w = real_of_int z ==> P w > > so, the only thing left is to substitute w and z in tl1 : > > apply (rule tl1 [of w z]) > > but this doesn't work as I expected, and I get a new goal with a new > variable za. the clue lies in the highlighting of the variable 'z': it has a yellow-ish background. In a proof, this denotes a free variable which doesn't occur in the statement and hasn't been fixed in any other way. In your example, it decidedly does not refer to the 'z' bound by the quantifier. This isn't a problem with the quantifier, but an effect of how bound variables are treated in Isabelle. There are two ways to solve your problem: 1. Don't instantiate. apply (rule tl1) apply assumption This will solve your goal just fine. There are no ambiguities at all in how the variables should be instantiated here. 2. Use 'rule_tac'. apply (rule_tac y=z in tl1) apply assumption Here, the 'z' refers to the bound variable, which is why it is coloured red. The ability to refer to bound variable is a specialty of 'rule_tac' and not available to all methods or attributes. In general, I strongly recommend against the use of 'rule_tac' together with explicit instantiations talking about bound variables (unless it is temporary and pending refactoring). (Imagine a huge red warning sign popping up when you use it.) The reason is quite simple: Bound variable names are usually system-generated and thus sometimes unpredictable. Your proof will break when you have another variable called 'z', someone renames the 'z' in 'Int_cases', ... Here is how I would write the proof: from assms obtain z where "w = real_of_int z" by (auto elim: Ints_cases) thus "P(w)" by (rule tl1) The 'z' above is written down explicitly and much more robust and you will find that explicit instantiation using 'of' works as expected. Cheers Lars

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

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

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