[isabelle] Transitivity reasoning in Isar with \ge
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Transitivity reasoning in Isar with \ge
- From: Peter Lammich <lammich at in.tum.de>
- Date: Fri, 09 Sep 2011 14:46:01 +0200
- User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:184.108.40.206) Gecko/20101125 SUSE/3.0.11 Thunderbird/3.0.11
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
any ideas wether it is possible to extend the behaviour of "..." to
also work with \ge?
This archive was generated by a fusion of
Pipermail (Mailman edition) and