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