[isabelle-dev] lemma

[Lawrence Paulson]

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.sternagel at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev