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.