[isabelle-dev] linordered_semiring_1

Yamada, Akihisa Akihisa.Yamada at uibk.ac.at
Fri Oct 20 17:37:30 CEST 2017

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

Best regards,

More information about the isabelle-dev mailing list