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



On Tue, May 31, 2011 at 6:08 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote:
> 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

Hi Randy,

Here is a proof that works:

inductive_cases fe2_elim [elim!]: "F2 b1 ~f f2"
inductive_cases be2_elim [elim!]: "B2 f1 ~b b2"

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"
by (induct arbitrary: f3 and b3 rule: fooEq_barEq.inducts, auto intro:
fooEq_barEq.intros)

OR:

by (induct arbitrary: f3 and b3 set: fooEq barEq, auto intro:
fooEq_barEq.intros)

The important thing is the "and" in "arbitrary: f3 and b3". This tells
induct to generalize over "f3" in the first goal, and over "b3" in the
second.

Simply saying "arbitrary: f3 b3" generalizes over both variables in
the first goal, but does not generalize the second one at all. Or
actually, the "b3" seems to be totally ignored, since there is no
variable with that name in the first goal. It seems like there ought
to be a warning message in that case, if you tell "induct" to
generalize over a non-existent variable.

Hope this helps,
- Brian

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