Re: [isabelle-dev] linordered_semiring_1
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
Re: [isabelle-dev] linordered_semiring_1
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
[isabelle-dev] linordered_semiring_1
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
