Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Transitivity reasoning in Isar with \ge

Email Gateway (Aug 18 2022 at 18:22):

From: Peter Lammich <lammich@in.tum.de>
Hi all,

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"

Currently, this does not work for two reasons:
First, \ge is syntactically translated to \le, before " ... " is
matched, and, second, there is no "swapped"
transitivity rule set up as [trans]. The second can be fixed by
adding such a rule:
lemma [trans]: "a\<ge>b \<Longrightarrow> b\<ge>c
\<Longrightarrow> a\<ge>(c::'a::order)" by (rule order_trans_rules)
Should this be included into the standard setup of the transitivity
reasoner?

any ideas wether it is possible to extend the behaviour of "..." to
also work with \ge?

Best,
Peter

Email Gateway (Aug 18 2022 at 18:22):

From: Johannes Hoelzl <hoelzl@in.tum.de>
Hi Peter,

for such reasoning the xtrans rules are used.
You find the following comment in ~~/src/HOL/Orderings.thy.
Here they use the (is _) keyword to introduce ?rhs as
abbreviation instead of "...", How would you extend ...
to work here?

(*

Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
for the wrong thing in an Isar proof.

The extra transitivity rules can be used as follows:

lemma "(a::'a::order) > z"
proof -
have "a >= b" (is "_ >= ?rhs")
sorry
also have "?rhs >= c" (is "_ >= ?rhs")
sorry
also (xtrans) have "?rhs = d" (is "_ = ?rhs")
sorry
also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
sorry
also (xtrans) have "?rhs > f" (is "_ > ?rhs")
sorry
also (xtrans) have "?rhs > z"
sorry
finally (xtrans) show ?thesis .
qed

Alternatively, one can use "declare xtrans [trans]" and then
leave out the "(xtrans)" above.
*)

Greetings,
Johannes

Email Gateway (Aug 18 2022 at 18:22):

From: Makarius <makarius@sketis.net>
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.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC