# [isabelle] Problem with arbitrary specification in double inductive rule induction

Hello,
I have a problem with bindings in a double inductive rule inductive proof.
The following is a contrived example:
inductive P :: "nat ⇒ bool"
and Q :: "nat ⇒ bool"
where
"Q n ⟹ P (n+1)"
| "P n ⟹ Q (n+1)"
lemma
fixes x::nat
shows "P n ⟹ Q m ⟹ P (n+m) "
and "Q n ⟹ Q m1 ⟹ P (n+m1)"
proof(induction arbitrary: m m1 rule: P_Q.inducts)
case (1 n)
then show ?case sorry
next
case (2 n)
then show ?case sorry
qed
If I put the cursor at the proof line I see:
1. ⋀n m. Q n ⟹ (Q m1 ⟹ P (n + m1)) ⟹ Q m ⟹ P (n + 1 + m)
2. ⋀n. P n ⟹ (⋀m. Q m ⟹ P (n + m)) ⟹ Q m1 ⟹ P (n + 1 + m1)
m1 is a free variable; m is bound.
Why is m1 still free even though I have specified that it should be
arbitrary? Including m1 in the arbitrary specification makes no difference
however removing m from the specification does make m free (as expected).
Cheers
Mark

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*