[isabelle] Transitivity reasoning in Isar with \ge



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





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