# Re: [isabelle] Having trouble on Producing an inductive lemma for the following inductive definition.

*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>
*Subject*: Re: [isabelle] Having trouble on Producing an inductive lemma for the following inductive definition.
*From*: Tjark Weber <webertj at in.tum.de>
*Date*: Sun, 01 Feb 2009 16:55:20 +0000
*Cc*: TIMOTHY KREMANN <twksoa262 at verizon.net>
*In-reply-to*: <49842EC9.6000102@in.tum.de>
*References*: <839487.99087.qm@web84005.mail.mud.yahoo.com> <49842EC9.6000102@in.tum.de>

On Sat, 2009-01-31 at 11:58 +0100, Tobias Nipkow wrote:
> I doubt that your lemma is true. The "Pa x" should be underneath the !!x.
"Pa x" is actually not needed at all. Here's an (unpolished) Isabelle
proof of the lemma (assuming "/\" meant "&"):
lemma stp_finite_induct:
"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"
apply (erule conjE)
apply (thin_tac "Pa x")
apply (erule finite_stp.induct)
apply assumption
apply (case_tac "a : A")
apply (subgoal_tac "insert a A = A")
apply auto
done
Regards,
Tjark

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*