See now http://isabelle.in.tum.de/repos/isabelle/rev/a1a4a5e2933a
Cheers Florian Am 28.10.2017 um 16:14 schrieb Florian Haftmann: > 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 >> > > > > _______________________________________________ > 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