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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.