Re: [isabelle] structured induction again?



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

Am 22/06/2011 04:12, schrieb Randy Pollack:
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 archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.