# Re: [isabelle] Transitivity reasoning in Isar with \ge

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

On Fri, 9 Sep 2011, Peter Lammich wrote:

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

```
```

```

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