# [isabelle] recdef problem

```Dear all,

```
I'm trying to define a recursive function. But Isabelle (2005, of Sept. 14th) complains about
```
*** \<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:

```
"\<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):
```

```
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.