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