[isabelle] recdef problem



Dear all,

I'm trying to define a recursive function. But Isabelle (2005, of Sept. 14th) complains about

*** Bad final proof state:
*** \<forall>s1 s2 stmt.
*** termStatement (Rep_StatementPos stmt) = seqS s1 s2 \<longrightarrow>
***    heightStatement (termStatement (Rep_StatementPos (seqFstP stmt)))
***    < heightStatement (termStatement (Rep_StatementPos stmt))
***  1. \<forall>s1 s2 stmt.
*** termStatement (Rep_StatementPos stmt) = seqS s1 s2 \<longrightarrow> *** heightStatement (termStatement (Rep_StatementPos (seqFstP stmt)))
***        < heightStatement (termStatement (Rep_StatementPos stmt))
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef".

I then took exactly this remaining goal as lemma and proved it:

lemma rssem_h_term1 [simp]:
"\<forall> s1 s2 stmt. termStatement (Rep_StatementPos stmt) = seqS s1 s2 \<longrightarrow> heightStatement (termStatement (Rep_StatementPos (seqFstP stmt)))
        < heightStatement (termStatement (Rep_StatementPos stmt))"
.... qed

and added this lemma to my recdef definition as hint (and even added it to the simplifier set for testing purposes, as you can see above):

(hints recdef_simp add: rssem_h_term1)

But still Isabelle gives me the same "Bad final proof state". How can I convince Isabelle to accept the lemma as proof for the remaining goal?

Thanks for any hints

Nicole

--
"Never in the field of software development was so much owed by so
many to so few lines of code" -- Martin Fowler about JUnit

Attachment: PGP.sig
Description: Signierter Teil der Nachricht



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