Theory Transitive_Closure_More

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
section ‹Auxiliary Results›

subsection ‹Reflexive Transitive Closures of Orders›

theory Transitive_Closure_More
  imports Main
begin

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

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

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

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

end