Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] structured induction again?


view this post on Zulip Email Gateway (Aug 18 2022 at 17:48):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
I have mutually defined inductive relations on a datatype:

datatype preClam =
pcVar nat "nat list"
| pcLam preClam

inductive weak :: "nat \<Rightarrow> preClam \<Rightarrow> preClam
\<Rightarrow> bool"
and split :: "preClam \<Rightarrow> (nat * preClam) \<Rightarrow> bool"
where
wkVar[intro!]: "weak n (pcVar m gam) (pcVar m (Cons n gam))"
| wkLam[intro]: "\<lbrakk>split wmM (m,M); weak n M wnM; weak m wnM
wmnM\<rbrakk>\<Longrightarrow>
weak n (pcLam wmM) (pcLam wmnM)"
| split[intro!]: "weak n N wnN \<Longrightarrow> split wnN (n,N)"

I want to prove a theorem by simultaneous induction:

lemma
shows weak_pcPN:"weak m M wmM \<Longrightarrow> P"
and split_pcPN:"\<lbrakk>split wnN nN; nN = (n,N)\<rbrakk>
\<Longrightarrow> Q"

I want to generalize n and N which appear in the second part of the
lemma. (This is standard, as n and N were only introduced to make the
statement of the lemma suitable for induction.) So I expect to write
something like

proof (induct arbitrary: n N rule: weak_split.inducts)

This attempt applies the induction rule but doesn't generalize n and
N. The relevant fact introduced by this induction is

(m, M) = (n, N) \<Longrightarrow> Q

which is of no use at all since n and N are not generalized.

How can this proof be done?

Thanks for any help.
Randy

view this post on Zulip Email Gateway (Aug 18 2022 at 17:48):

From: Tobias Nipkow <nipkow@in.tum.de>
Hi Randy,

I think you need to give arbitrary a list of lists, one for each
inductive predicate, separated by "and". In this case the first list
should probably be empty:

proof (induct arbitrary: and n N rule: weak_split.inducts)

Tobias


Last updated: Mar 29 2024 at 08:18 UTC