Как поднять леммы - PullRequest
Новая
       10

Как поднять леммы

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

Вот типовой тип данных с детерминированным отношением. 

datatype ty1 = A | B | C ty1 | D ty1

inductive rel1 where
  "rel1 A (C B)"
| "rel1 (C B) (D A)"

lemma rel1_det:
  "rel1 x y ⟹ rel1 x z ⟹ y = z"
  by (elim rel1.cases; auto)

Я пытаюсь поднять лемму для следующего типа: 

datatype 'a ty2 = E 'a | F 'a

abbreviation "rel2 ≡ rel_ty2 rel1"

lemma rel2_det:
  "rel2 x y ⟹ rel2 x z ⟹ y = z"
  apply (cases x; cases y; auto)
  apply (metis rel1_det right_uniqueD right_uniqueI ty2.rel_intros(1) ty2.right_unique_rel)
  by (metis rel1_det right_uniqueD right_uniqueI ty2.rel_intros(2) ty2.right_unique_rel)

Но доказательство очень уродливо,Я думаю, это можно упростить, используя метод transfer, подъемный пакет или что-то еще.Не могли бы вы предложить, как его использовать?

1 Ответ

2 голосов
/ 28 марта 2019

Я не знаю, как использовать трансферный пакет, чтобы доказать это;однако легко доказать, что вы используете предикат right_unique из библиотеки и правила для него, которые пакет datatype предоставляет вам бесплатно: 

lemma right_unique_rel1: "right_unique rel1"
  by (auto simp: right_unique_def elim: rel1.cases)

lemma right_unique_rel2: "right_unique rel2"
  by (intro ty2.right_unique_rel right_unique_rel1)
...