Idiomatically capturing "all idempotent semirings induce a partial order"

Question

I am trying to capture the fact that there's an induced partial ordering in any idempotent semiring in Isabelle/HOL but am having trouble working out the best/correct way to do it.

I define:

class idem_semiring_1 = semiring_1 +
  assumes idem [algebra_simps]: ‹a + a = a›
begin

definition less_eq :: ‹'a ⇒ 'a ⇒ bool›
  where ‹less_eq a b ⟷ a + b = b›

definition less :: ‹'a ⇒ 'a ⇒ bool›
  where ‹less a b ⟷ less_eq a b ∧ ¬ less_eq b a›

end

Now, it's straightforward to demonstrate that less_eq and less satisfy all of the laws of the order type class. However, is there a way of convincing Isabelle/HOL that any instance of idem_semiring_1 is also necessarily an instance of order using these definitions, so that the following query type-checks?

term ‹(y::'a::{idem_semiring_1}) ≤ x›

No combination of subclass, sublocale, etc., incantations seems to achieve what I want. In particular, the following:

sublocale idem_semiring_1 ⊆ order less_eq less
  by (standard; clarsimp simp add: algebra_simps less_eq_def less_def) (metis add.assoc)

seems to work, as in the following lemmas become trivially provable via simp:

lemma
  fixes x::‹'a::{idem_semiring_1}›
  shows ‹less_eq x x›
    by simp

lemma
  assumes ‹less_eq x y›
      and ‹less_eq y z›
    shows ‹less_eq x z›
  using assms by simp

but the following does not type-check:

lemma
  fixes x :: ‹'a::{idem_semiring_1}›
  shows ‹x ≤ x›

What am I not doing to convince Isabelle to connect the ≤ syntax with the less_eq definition?

ammbauer ammbauer · Accepted Answer · 2019-03-26T16:00:03

What if you defined idem_semiring_1 like this:

class idem_semiring_1 = semiring_1 + order +
  assumes idem [algebra_simps]: ‹a + a = a› and
      less_eq_idem_semiring_1: ‹a ≤ b ⟷ a + b = b›

Idiomatically capturing "all idempotent semirings induce a partial order"

1 Answers