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
