*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] structured induction again?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 22 Jun 2011 08:12:30 +0200*In-reply-to*: <BANLkTim9cycsBTggo06eDiXtBpZk7Xav4w@mail.gmail.com>*References*: <BANLkTim9cycsBTggo06eDiXtBpZk7Xav4w@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; de; rv:1.9.2.17) Gecko/20110414 Thunderbird/3.1.10

Hi Randy,

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)

**References**:**[isabelle] structured induction again?***From:*Randy Pollack

- Previous by Date: [isabelle] structured induction again?
- Next by Date: Re: [isabelle] power2_sum outside of rings
- Previous by Thread: [isabelle] structured induction again?
- Next by Thread: [isabelle] VSTTE 2012 : Second Call for Papers
- 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