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



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.