习惯性地捕捉“所有幂等半环诱导偏序”

Question

我试图捕捉这样一个事实，即在Isabelle / HOL的任何幂等半环中存在诱导的部分排序，但是我在制定最佳/正确的方法时遇到了麻烦。

我定义：

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

现在，可以直接证明less_eq和less满足order类型的所有定律。但是，有没有一种方法可以说服Isabelle / HOL，idem_semiring_1的任何实例也必然是使用这些定义的order实例，以便以下查询类型检查？

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

没有子类，sublocale等组合，咒语似乎达到了我想要的。特别是，以下内容：

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

似乎有效，因为以下的引理通过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

但以下不进行类型检查：

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

我不是要说服伊莎贝尔将≤语法与less_eq定义联系起来？

Answer 1

如果你这样定义了idem_semiring_1怎么办：

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›