Как доказать леммы для взаимно рекурсивных типов?

Question

Вот пример теории:

datatype t1 = A | B t2
     and t2 = C | D t1

inductive rel1 and rel2 where
  "rel1 A 0"
| "rel2 x n ⟹
   rel1 (B x) n"
| "rel2 C 1"
| "rel1 x n ⟹
   rel2 (D x) n"

lemma rel1_det:
  "rel1 x n ⟹ rel1 x m ⟹ n = m"
  apply (induct x, auto)
  apply (simp add: rel1.simps)
  apply (simp add: rel1.simps)

Я пытаюсь доказать, что rel1 является детерминированным.Но, похоже, я не могу использовать простую индукцию.Не могли бы вы предложить, какую тактику использовать для доказательства таких лемм?

Answer 1

Для взаимозависимых типов доказательства используют взаимозависимую индукцию.Итак, у леммы также будет два утверждения:

lemma
    rel1_det: "rel1 x n ⟹ rel1 x m ⟹ n = (m::nat)" and
    rel2_det: "rel2 y p ⟹ rel2 y q ⟹ p = (q::nat)"
        apply (induction x and y arbitrary: n m and p q)
        apply (simp add: rel1.simps)+
        apply (simp add: rel2.simps)+
    done