Re: [isabelle] Transitivity reasoning in Isar with \ge
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"
have "a >= b" (is "_ >= ?rhs")
also have "?rhs >= c" (is "_ >= ?rhs")
also (xtrans) have "?rhs = d" (is "_ = ?rhs")
also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
also (xtrans) have "?rhs > f" (is "_ > ?rhs")
also (xtrans) have "?rhs > z"
finally (xtrans) show ?thesis .
Alternatively, one can use "declare xtrans [trans]" and then
leave out the "(xtrans)" above.
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"
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