Как доказать, что свойство отношения выполняется для транзитивного замыкания этого отношения?

Я определил следующее свойство отношения:

definition rel_limited_under :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
  "rel_limited_under R A = 
   (∀x y z :: 'a. R x y ⟶ R y z ⟶ x ∈ A ⟶ z ∈ A ⟶ y ∈ A)"

Отношение R ограничено множеством A тогда и только тогда, когда любые два элемента x и z из этого множества могут быть связаны только через элемент y, принадлежащий этому множеству. Другими словами, элементы из множества A не могут быть связаны через элемент, не принадлежащий этому множеству.

Знаете ли вы общее название этого свойства? Я думаю, это что-то из теории графов.

Не могли бы вы предложить, как доказать, что свойство выполняется для транзитивного замыкания отношения?

lemma rel_tcl_limited_under:
  fixes R :: "'a ⇒ 'a ⇒ bool"
    and A :: "'a set"
  assumes as_R: "rel_limited_under R A"
  shows "rel_limited_under R⇧+⇧+ A"

graph-theory theorem-proving isabelle
person Denis    schedule 08.10.2018    source источник
comment
Путь ближе всего связан, но вы, конечно, уже это знаете. Узлы (ребра) каждого пути между x и z содержатся в A. Вершины и ребра путей принадлежат графу. Либо x является предком z, либо наоборот.   -  person Joop Eggen    schedule 08.10.2018
comment
Я имею в виду общее имя этого подграфа A. Если свернуть множество A в один узел, то в графе не будет путей, идущих от A к A. Я думал, что у такого подграфа есть какое-то особое имя.   -  person Denis    schedule 08.10.2018
comment
Что-то вроде компонента связности или клики. Но кажется, что этот вид подграфов слишком специфичен, чтобы иметь специальное имя.   -  person Denis    schedule 08.10.2018

Ответы (1)


arrow_upward
2
arrow_downward

Я могу сказать вам, что вы не можете доказать свойство rel_tcl_limited_under в Изабель, так как оно просто не имеет места. В качестве контрпримера рассмотрим A = {0} и R = {(0,1), (1,2), (2,0)}. Тогда rel_limited_under R A выполняется тривиально, так как нет x, y, z таких, что R x y /\ R y z /\ x ∈ A /\ z ∈ A. Но rel_limited_under (R^+) A не подходит: выбираем x = 0, y = 1, z = 0.

person René Thiemann    schedule 09.10.2018
comment
Спасибо! Я переопределил свойство как ∀x y z. R⇧+⇧+ x y ⟶ R y z ⟶ x ∈ A ⟶ z ∈ A ⟶ y ∈ A. И это свойство как раз подходит для моей теории. Мне не нужно доказывать лемму из вопроса. - person Denis; 09.10.2018
comment
С этим уточнением должно быть легко использовать индукцию по транзитивному замыканию. Начните с x in A, R^+ x y, z in A и R^+ y z. Затем по индукции по R^+ y z видно, что все элементы между y и z должны находиться в A. - person René Thiemann; 09.10.2018