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

I doubt that your lemma is true. The "Pa x" should be underneath the !!x.
Unless finite_stp is just a boiled down version of some larger def, I
would not define finite_stp at all but would write "finite F & (ALL x:F.
Pa x)" explicitly.
Tobias
TIMOTHY KREMANN schrieb:
> 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

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