[isabelle-dev] linordered_semiring_1

[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
> 

-- 

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/20171028/110a483c/attachment.sig>