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



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.