我试图捕捉这样一个事实,即在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
定义联系起来?
如果你这样定义了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›