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