Re: [isabelle] some problems with the /\ quantifier
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
many thanx, noam
×××××× 13 ×××× 2015 08:22,â "Lars Hupel" <hupel at in.tum.de> ×××:
> > 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and