*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 31 May 2011 19:42:21 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTinrh8Dn_=ANrnvcANAZ4PazZ_Rj6w@mail.gmail.com>*References*: <BANLkTinrh8Dn_=ANrnvcANAZ4PazZ_Rj6w@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

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

**References**:

- Previous by Date: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?
- Next by Date: [isabelle] tactical combinators
- Previous by Thread: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?
- Next by Thread: [isabelle] tactical combinators
- Cl-isabelle-users June 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list