*To*: Nicole Rauch <rauch at informatik.uni-kl.de>*Subject*: Re: [isabelle] recdef problem*From*: John Ridgway <ridgwayj at acm.org>*Date*: Sun, 18 Sep 2005 09:14:31 -0400*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <D2D4DDC6-A3B6-4783-A132-B0C413F2C2BB@informatik.uni-kl.de>*References*: <D2D4DDC6-A3B6-4783-A132-B0C413F2C2BB@informatik.uni-kl.de>*Reply-to*: John Ridgway <ridgwayj at acm.org>

(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

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

**Follow-Ups**:**Re: [isabelle] recdef problem***From:*Nicole Rauch

**References**:**[isabelle] recdef problem***From:*Nicole Rauch

- Previous by Date: [isabelle] recdef problem
- Next by Date: Re: [isabelle] who knows theorem-proving about cache protocols
- Previous by Thread: [isabelle] recdef problem
- Next by Thread: Re: [isabelle] recdef problem
- Cl-isabelle-users September 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list