Re: [isabelle] recdef problem



I had this same kind of problem back in the spring, and it was suggested that I try the following:
 (hints intro!: rssem_h_term1)
using intro! rather than simp

That took care of my problems.

Now, if I only understood the difference between intro and simp... :)

Peace
- John


--On Friday, September 16, 2005 8:56 PM +0200 Nicole Rauch <rauch at informatik.uni-kl.de> wrote:

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










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