Доказательство классовой теоремы в Изабель - PullRequest
Новая
       71

Доказательство классовой теоремы в Изабель

1 голос
/ 14 июля 2020

Я должен доказать тривиальность, используя классы типов: 

class order =
  fixes lesseq :: " 'a ⇒ 'a ⇒ bool" (infix "≼" 50)
  assumes refl:    "x ≼ x"
      and trans:   "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
      and antisym: "x ≼ y ⟹ y ≼ x ⟹ x = y"
begin

  theorem "(myle:: ('b::order) ⇒ 'b ⇒ bool) x x"
  proof -
    show ?thesis by (rule refl)
  qed

end

Здесь Isabelle / jEdit выделяет by (rule refl) розовым цветом и говорит: 

Failed to apply initial proof method⌂:
goal (1 subgoal):
 1. myle x x

В чем проблема? В противном случае доказательство кажется go до

1 Ответ

3 голосов
/ 14 июля 2020

myle и ≼ - это не одна и та же функция.

В аннотации типа (myle:: ('b::order) ⇒ 'b ⇒ bool) просто указано, что myle - это функция, которая принимает два элемента типа 'b и возвращает логическое значение и что 'b является типом, принадлежащим классу типов order.

Если вы хотите что-то доказать насчет ≼, просто используйте тот же символ или имя lesseq.

...