*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Having trouble on Producing an inductive lemma for the following inductive definition.*From*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Date*: Fri, 30 Jan 2009 12:17:22 -0800 (PST)

inductive finite_stp :: "('a => bool) => 'a set => bool" where stp_emptyI [simp, intro!]: "finite_stp Pa {}" | stp_insertI[simp, intro!]: "finite_stp Pa A /\ Pa a ==> finite_stp Pa (insert a A)" I want to prove: lemma stp_finite_induct [case_names empty insert, induct set: finite_stp]: "finite_stp Pa F /\ Pa x ==> P {} ==> (!!x Pa F . finite_stp Pa F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" Is this a true? Thanks, Tim

**Follow-Ups**:

- Previous by Date: Re: [isabelle] Partial Linear Arithmetic
- Next by Date: Re: [isabelle] Partial Linear Arithmetic
- Previous by Thread: [isabelle] Journal of Automated Reasoning: Special Issue on the POPLmark Challenge
- Next by Thread: Re: [isabelle] Having trouble on Producing an inductive lemma for the following inductive definition.
- Cl-isabelle-users January 2009 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