[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
qed
Best regards,
Akihisa
More information about the isabelle-dev
mailing list