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


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"
  "Q n ⟹ P (n+1)"
| "P n ⟹ Q (n+1)"

  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
  case (2 n)
  then show ?case sorry

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).



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