Re: [isabelle] Transitivity reasoning in Isar with \ge
On Fri, 9 Sep 2011, Peter Lammich wrote:
I just wondered if it is possible to use the Isar-style transitivity
reasoning with \ge, i.e.
note `a\ge b` also note `... \ge c` finally have "a\ge c"
There is still no proper way to do it. When I've introduced the concept
of calculational reasoning in Isar the >= abbreviations did not exist, and
it was already known that it would not work. (The potential for confusion
when swapping order of concrete vs. abstract syntax was known long before
Isar, which was the reason for avoiding it in early Isabelle/HOL.)
Later >= was introduced nonetheless, when I was not looking / not quick
enough to explain the situation. Since that time I have an item on my
TODO list to extend the "..." treatment of Isar to accomodate that
extension of the HOL library. The >= abbreviation is an example where
bug / feature are one and the same thing.
This archive was generated by a fusion of
Pipermail (Mailman edition) and