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



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