# [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?

Consider the following example (in Main of isabelle 2011).
datatype foo = F1 | F2 bar and bar = B1 | B2 foo
inductive fooEq::"foo \<Rightarrow> foo \<Rightarrow> bool" (infix "~f" 100)
and barEq::"bar \<Rightarrow> bar \<Rightarrow> bool" (infix "~b" 100)
where
fe1:"F1 ~f F1"
| fe2:"b1 ~b b2 \<Longrightarrow> F2 b1 ~f F2 b2"
| be1:"B1 ~b B1"
| be2:"f1 ~f f2 \<Longrightarrow> B2 f1 ~b B2 f2"
I want to prove that fooEq and barEq are transitive
lemma
shows feTrn: "\<lbrakk>f1 ~f f2; f2 ~f f3\<rbrakk>\<Longrightarrow> f1 ~f f3"
and beTrn: "\<lbrakk>b1 ~b b2; b2 ~b b3\<rbrakk>\<Longrightarrow> b1 ~b b3"
The proof is by simultaneous induction on the first premise and
inversion on the second premise. The first case (fe1) is solved by
"force"
proof (induct rule: fooEq_barEq.inducts, force)
consider the second case:
case (fe2 b1a b2a)
have j0:"F2 b2a ~f f3"
and j1:"b1a ~b b2a"
and j2:"b2a ~b b3 \<Longrightarrow> b1a ~b b3" by fact+
This is clearly wrong; we need to generalize over f3 and b3 so that j2
is parametric in b3. Try using "arbitrary":
proof (induct arbitrary: f3 b3 rule: fooEq_barEq.inducts, force)
case (fe2 b1a b2a f3a)
have j0:"F2 b2a ~f f3a"
and j1:"b1a ~b b2a"
and j2:"b2a ~b b3 \<Longrightarrow> b1a ~b b3" by fact+
What happened? The occurrence of b3 in j2 was not generalized
although a new variable "f3a" has appeared in j0.
How can this proof be done?
Thanks,
Randy

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