Quelle  induc.thy   Sprache: Isabelle

      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)"
 

 
 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 ∉ F ==> 
               P F ==> P (insert x F))
     ==> P F"