Расчет переходных укупорочные

Question

У меня есть следующее определение:

definition someRel :: "nat rel" 
where 
    "someRel = {(1, 2), (2, 3), (3, 4), (4, 5)}" 

Я хочу, чтобы доказать следующую лемму:

lemma "someRel^*``{1}={1, 2, 3, 4, 5}" 

я придумал следующее доказательство:

proof 
    show "someRel^*``{1} ⊆ {1, 2, 3, 4, 5}" 
    proof 
    fix x 
    assume "x ∈ someRel⇧* `` {1}" 
    then show "x ∈ {1, 2, 3, 4, 5}" 
     using assms someRel_def by (auto elim: rtranclE) 
    qed 
next 
    show "{1, 2, 3, 4, 5} ⊆ someRel^*``{1}" 
    proof 
    fix x 
    assume "x ∈ {1::nat, 2, 3, 4, 5}" 
    then show "x ∈ someRel⇧* `` {1}" 
     using assms someRel_def Image_singleton by (induction) blast+ 
    qed 
qed 

Это доказательство имеет следующие проблемы:

• Первая часть (show "someRel^*``{1} ⊆ {1, 2, 3, 4, 5}") подтверждена с использованием правила rtranclE. Это не сработает, если я добавлю еще одну пару в отношение someRel (скажем, пара (6, 7))
• Доказательство второй части (show "{1, 2, 3, 4, 5} ⊆ someRel^*``{1}") не заканчивается.

Может ли кто-нибудь предложить лучшее доказательство? То, что (а) допускает большее количество пар в отношении someRel и (б), которое завершается.

Answer 1

Оказывается, что для вашего конкретного экземпляра (и некоторые немного более крупного, которые я пробовал), достаточно использовать следующий (найденный первое применение auto и затем запустить sledgehammer на остальных целях, чтобы определить полезные факты, как converse_rtrancl_into_rtrancl здесь):

by (auto simp: someRel_def converse_rtrancl_into_rtrancl elim: rtranclE) 

Однако, в общем случае это может быть, лучше, чтобы сделать одно из следующих действий:

1. устройства тактик, чтобы доказать такие цели (на самом деле вычислений вовлеченного транзитивного замыкания)
2. вычислить транзитное замыкание внутри Isabelle/HOL (либо через simp - что может быть медленным - или через eval - что, насколько я знаю, является своего рода оракулом).

Для последнего может представлять интерес запись AFP Executable Transitive Closures.

Обновление: Я добавил пример simproc, который вычисляет изображения конечных транзитивных замыканий по конечным множествам путем оценки в версию разработки AFP. Вместо Executable Transitive Closures, однако, я основывался на примере на Executable Transitive Closures of Finite Relations. Ваш пример можно найти в конце теории Finite_Transitive_Closure_Simprocs (как только веб-сайт AFP синхронизируется с основным хранилищем ртути).

Обновления: Обратите внимание, что указанный выше simproc специально направлен на шаблонах вида r^* `` x где множество r и x являются конечным в том смысле, что они приведены в конечном множестве обозначений {x1, x2, ..., xN}. Таким образом, для запуска конкретной цели вам может потребоваться добавить дополнительные факты/simp rules/simprocs/..., чтобы нормализовать выражение в этой форме.

Пример: Если у вас была цель

"(converse someRel)^* `` {1} = {1}" 

вы должны добавить правила, которые на самом деле «применить» в converse операцию на заданном конечном множестве. Ниже будет делать:

lemma [simp]: 
    "converse (insert (x, y) A) = insert (y, x) (converse A)" 
    by auto 

Теперь цель может быть решена с помощью

by (auto simp: someRel_def) 

Answer 2

Добавление к ответу Криса, вот полная версия, которая использует AFP-запись для переходных замыканий, и которая делает используйте code-simp вместо eval. code-simp немного медленнее, чем eval, но не полагается на оракулы.

theory Test 
imports "$AFP/Transitive-Closure/Transitive_Closure_List_Impl" 
begin 

lemma to_memo_list: "(set xs)^* `` {a} = set (memo_list_rtrancl xs a)" 
    unfolding memo_list_rtrancl Image_def by auto 

definition someRel :: "nat rel" 
where 
    "someRel = {(1, 2), (2, 3), (3, 4), (4, 5), (5,3)}" 

definition someRel_list :: "(nat × nat)list" 
where 
    "someRel_list = [(1, 2), (2, 3), (3, 4), (4, 5), (5,3)]" 

lemma someRel_list: "someRel = set someRel_list" by code_simp 

lemma "someRel^*``{4}={3, 4, 5}" 
    unfolding someRel_list to_memo_list by code_simp 

end