Явные аксиомы о секвентах - PullRequest
Новая
       8

Явные аксиомы о секвентах

0 голосов
/ 12 июня 2018

Примечание: Это повторный вопрос второго вопроса здесь , который оказался менее связанным с первым вопросом (ответили там), чем я думал, что это будет.

Рассмотрим следующую минимальную разработку на основе библиотеки Isabelle Sequents: 

theory Test
  imports Pure Sequents.Sequents
begin

syntax "_Trueprop"    :: "two_seqe" ("((_)/ ⊢ (_))" [6,6] 5)
consts Trueprop :: two_seqi
parse_translation ‹[  (@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))  ]›
print_translation ‹[  (@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))  ]›

axiomatization where
  xch : "⋀A B C D. $A, $B, $C ⊢ $D  ⟹  $C, $B, $A ⊢ $D"

lemma xch0 : "$A, $C ⊢ $D  ⟹  $C, $A ⊢ $D"
  apply (rule xch[of A _ C D] ; assumption)  done

lemma xch1 : "$A, P, $C ⊢ $D  ⟹  $C, P, $A ⊢ $D"
  apply (rule xch[of A _ C D] ; assumption)  done

lemma xch2 : "$A, P, Q, $C ⊢ $D  ⟹  $C, P, Q, $A ⊢ $D"
  apply (rule xch[of A _ C D] ; assumption)  done

Эти доказательства работают (фактически, они работают даже без аннотаций of).Однако я хочу знать, что я мог бы написать вместо _ s, чтобы быть максимально явным.То есть, как мне написать «пустую последовательность» или «последовательность, содержащую только P» или «последовательность, содержащую только P, Q»?Не работает запись "" для xch0, P или "P" для xch1, "P, Q" для xch2, и я не могу понять из источника Sequents для какого явного синтаксиса эти обозначения являются аббревиатурами.

1 Ответ

0 голосов
/ 14 июня 2018

Последовательности в левой части ⊢ внутренне представлены как приложения функций.Это гарантирует, что объединение высшего порядка может создавать схематические переменные в теоремах с произвольным числом последовательных элементов.Таким образом, $A, $B, $C ⊢ $D представляются как Trueprop (%s. A (B (C s))) (%s. D s).

Итак, в вашей первой лемме экземпляр B создается с помощью функции тождества %x. x.

Отдельные элементы типа объекта o преобразуются в этот аппликативный формат с использованием констант SeqO' и Seq1', объявленных в начале теории Sequents.Маркер $ указывает, что синтаксический анализатор не должен вставлять такую ​​константу.

Таким образом, в вашей второй лемме B создается с SeqO'(P).В третьей лемме должен быть создан экземпляр B с последовательностью P и Q, которая выражается в виде %s. SeqO'(P, SeqO'(Q, s)).Обозначения <<P>> и <<P, Q>> обозначают одно и то же и являются предпочтительными.

Вы можете посмотреть на внутреннее представление секвента с помощью Изабель / ML через 

ML {* @term{"$A, P, $C ⊢ $D"} *}

Вот как я понялиз того, что происходило.

...