如何证明相互递归类型的引理？

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

如何证明相互递归类型的引理？

How to prove lemmas for mutually recursive types?

isabelle