Полиморфное определение равенства в Изабель / ZF, похоже, не работает - PullRequest
Новая
       16

Полиморфное определение равенства в Изабель / ZF, похоже, не работает

1 голос
/ 01 декабря 2019

Если есть определение равенства в Изабель / ZF (точнее, IFOL): 

axiomatization
  eq :: ‹['a, 'a] ⇒ o›  (infixl ‹=› 50)
where
  refl: ‹a = a› and
  subst: ‹a = b ⟹ P(a) ⟹ P(b)›

Как я могу это доказать: 

lemma qu:
  fixes C::‹i⇒o›
  shows ‹C = C›
oops

Это даже не проверено на типизацию! И "эквалайзер" имеет полиморфный тип! Как это может быть?

Конечно, мы можем определить равенство классов: 

definition
  eqc  :: "[(i⇒o),(i⇒o)]=>o" where
    "eqc(A,B) == ∀x. A(x) ⟷ B(x)"

, но вопрос в том, чтобы включить (adhoc?) Полиморфизм в Изабель.

1 Ответ

0 голосов
/ 06 декабря 2019

Знак равенства "=" обозначает равенство множеств в Изабель / ZF. Эквивалентность предикатов обозначается \<equiv>, что отображается как «≡» в Изабель / Джедит и контрольном документе. Это иллюстрирует следующее: 

theory Scratch imports ZF.equalities

begin

lemma A: shows "C = C" by simp 

lemma B: shows "C \<equiv> C" by simp

lemma C: 
  assumes "P \<equiv> Q" 
  shows "\<forall>x. P(x) \<longleftrightarrow> Q(x)" using assms by auto

lemma D: 
  assumes "P \<equiv> Q" 
  shows "\<forall>x y. P(x,y) \<longleftrightarrow> Q(x,y)" using assms by auto

end

Вот как это выглядит с точки зрения пользователя, я не знаю, как это реализовано внутри.

...