[isabelle-dev] linordered_semiring_1

[Florian Haftmann]

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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171030/523cb04c/attachment.sig>