*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] some problems with the /\ quantifier*From*: noam neer <noamneer at gmail.com>*Date*: Sun, 13 Sep 2015 09:59:36 +0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <55F50825.9020104@in.tum.de>*References*: <CAGOKs09PRLE1E97Sw9ri493tdjA8G3vRMAMYyWm+TBf0nfxVuA@mail.gmail.com> <55F50825.9020104@in.tum.de>

1. here it is possible to not instantiate, because it is a simplified example. in the original proof I had to instantiate. 2. this is a nice solution, but why do methods differ with this respect? this is very confusing. 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. many thanx, noam ×××××× 13 ×××× 2015 08:22,â "Lars Hupel" <hupel at in.tum.de> ×××: > 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:*Lars Hupel

**Re: [isabelle] some problems with the /\ quantifier***From:*Larry Paulson

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

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

- 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