транзитивное замыкание идентичности относительно

Question

Я не в состоянии доказать следующее lemma в Isabelle:

lemma "Id^* = Id" 

Любые идеи о том, как доказать это?

Answer 1

Чтобы получить представление о том, как это работает, вы должны в первую очередь думать о том, как вы бы это доказать на бумаге. Как вы видите на

term "Id" 

Id представляет собой набор пар (типа ('a * 'a) set). Таким образом, вам нужно показать равенство двух множеств. Канонический способ сделать это - показать, что каждый набор является подмножеством другого.

Давайте начнем с Id^* ⊆ Id. Как показать, что набор является подмножеством другого? Точно, показывают, что каждый элемент из «меньше» устанавливается также элемент «больше» один, то есть,

fix x y 
assume "(x, y) ∈ Id^*" 
then show "(x, y) ∈ Id" 

Поскольку транзитивное замыкание определяется индуктивно, мы можем сделать это по индукции следующим

by (induct) simp_all 

То есть использовать правило индукции по умолчанию для предпосылки формы (_, _) ∈ _^* (что бывает rtrancl_induct), а затем упростить базовый регистр, а также индуктивный футляр.

Еще раз, полное доказательство

lemma 
    "Id^* ⊆ Id" 
proof (rule subrelI) 
    fix x y 
    assume "(x, y) ∈ Id^*" 
    then show "(x, y) ∈ Id" 
    by (induct rule: rtrancl_induct) simp_all 
qed 

Другое направление остается в качестве упражнения.

Answer 2

Если вы просто вызовите кувалды (через панель или через try), то вы сразу же получите доказательство:

by (metis rtrancl_empty rtrancl_idemp) 

Answer 3

Я до сих пор новичок в этом. Я полагаю, что все доказательство Isar - это что-то вроде:

lemma "Id^* = Id" 
proof (rule equalityI) 
    show "Id^* ⊆ Id" 
    proof (rule subrelI) 
    fix x y 
    assume "(x, y) ∈ Id^*" 
    then show "(x, y) ∈ Id" 
    by (induct) simp_all 
    qed 
next 
    show "Id ⊆ Id^*" 
    proof (rule subrelI) 
    fix x y 
    assume "(x, y) ∈ Id" 
    then show "(x, y) ∈ Id^*" 
    by (auto) 
    qed 
qed