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