I am trying to understand why all four of these appear to be independent theorems even though the “greater than” relations are nothing but abbreviations. And maybe the problem is here:
> abbreviation (input) > greater_eq (infix ">=" 50) where > "x >= y ≡ y <= x" > > abbreviation (input) > greater (infix ">" 50) where > "x > y ≡ y < x” Perhaps we need “op > == %x y. y < x”? Larry On 16 Apr 2014, at 10:13, Christian Sternagel <c.sterna...@gmail.com> wrote: > 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 > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
