Hi Akihisa, thanks for pointing that out.
I will take care of this.
All the best,
Florian
Am 20.10.2017 um 17:37 schrieb Yamada, Akihisa:
> Dear Isabelle/HOL developers,
>
> I propose to make linordered_semiring_1 a subclass of zero_less_one.
>
> class linordered_semiring_1 =
> linordered_semiring + semiring_1 + zero_less_one
>
> (Of course, zero_less_one should be defined earlier.)
>
> Currently, it does not assume 0 < 1, but this generality allows only
> nonsense (and confusing) instances as the assumptions of
> ordered_semiring is applicable only if there is some positive element,
> which cannot exist if 0 < 1.
>
> lemma (in linordered_semiring_1)
> assumes a0: "0 < a" shows "0 < 1"
> proof (rule ccontr)
> assume "¬ 0 < 1" then have "1 ≤ 0" by auto
> from mult_nonpos_nonneg[OF this] a0 have "a ≤ 0" by auto
> with a0 show False by auto
> qed
>
> Best regards,
> Akihisa
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
