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