Search code examples
isabelle

How to prove lemmas for mutually recursive types?

Here is a sample theory:

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)

I'm trying to prove, that rel1 is deterministic. But it seems that I can't use a simple induction. Could you suggest what tactics to use to prove such lemmas?

Solution

  • For mutually dependent types, proofs use mutually dependent induction. So, the lemma is going to have two claims as well:

    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