[isabelle-dev] lemma

[Christian Sternagel]

Dear all,

how about adding the following lemmas to the order class?

lemma (in order) rtranclp_less_eq [simp]:
   "(op ≤)⇧*⇧* = op ≤"
   by (intro ext) (auto elim: rtranclp_induct)

lemma (in order) tranclp_less [simp]:
   "(op <)⇧+⇧+ = op <"
   by (intro ext) (auto elim: tranclp_induct)

lemma (in order) rtranclp_greater_eq [simp]:
   "(op ≥)⇧*⇧* = op ≥"
   by (intro ext) (auto elim: rtranclp_induct)

lemma (in order) tranclp_greater [simp]:
   "(op >)⇧+⇧+ = op >"
   by (intro ext) (auto elim: tranclp_induct)

cheers

chris