[isabelle-dev] linordered_semiring_1

[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