Re: [isabelle] some problems with the /\ quantifier



does this problem happen whenever the /\ quantifier is involved,
or just when automatic names are generated?
for example if I use
  apply(induct n)
will I be able to use 'n' with all the methods?


On Sun, Sep 13, 2015 at 12:02 PM, Lars Hupel <hupel at in.tum.de> wrote:

> > 2. this is a nice solution, but why do methods differ with this respect?
> > this is very confusing.
>
> No, it is not a nice solution. These methods are "improper", which means
> they are still supported but you should refrain from using them. They
> are really nice for exploring proofs, but as I said, it is much better
> to rewrite such proofs afterwards. See also Â9.2.3 from the Isar
> Reference Manual.
>
> > 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.
>
> 'rename_tac' might make your proof more robust, but it does not improve
> readability at all.
>
> The precise methods to use were not the main point of my recommendation;
> rather that instantiations and eliminations often are much more elegant
> in Isar style. If you don't want to use 'auto', 'rule' would also work
> in that situation:
>
>   from assms obtain z where "w = real_of_int z"
>     by (rule Ints_cases)
>
> By the way, because of the LCF nature of Isabelle, there is no harm in
> using 'auto' even if you don't understand what it's doing. In fact,
> automated tactics are very often more robust than low-level proofs
> because they are not as sensitive to details.
>
> Cheers
> Lars
>



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