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