Идиоматически захватывая «все идемпотентные полукольца вызывают частичный порядок» - PullRequest
Новая
       15

Идиоматически захватывая «все идемпотентные полукольца вызывают частичный порядок»

0 голосов
/ 26 марта 2019

Я пытаюсь уловить тот факт, что в любом идемпотентном полукольце в Изабель / ХОЛ есть индуцированное частичное упорядочение, но у меня возникают проблемы при разработке наилучшего / правильного способа сделать это.

Я определяю: 

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.Однако существует ли способ убедить Изабель / HOL, что любой экземпляр idem_semiring_1 также обязательно является экземпляром order с использованием этих определений, так что следующие проверки типов запроса? 

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

НетСочетание подкласса, сублокала и т. д., заклинания, кажется, добиваются того, чего я хочу.В частности, следующее: 

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?

1 Ответ

1 голос
/ 26 марта 2019

Что если вы определили 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›
...