Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] structured induction: mutual definitions and "...

Email Gateway (Aug 18 2022 at 17:46):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
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

Email Gateway (Aug 18 2022 at 17:48):

From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, May 31, 2011 at 6:08 PM, Randy Pollack <rpollack@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

Last updated: Apr 25 2024 at 08:20 UTC