*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] recdef problem*From*: Nicole Rauch <rauch at informatik.uni-kl.de>*Date*: Fri, 16 Sep 2005 20:56:32 +0200

Dear all,

*** Bad final proof state: *** \<forall>s1 s2 stmt.

*** heightStatement (termStatement (Rep_StatementPos (seqFstP stmt))) *** < heightStatement (termStatement (Rep_StatementPos stmt)) *** 1. \<forall>s1 s2 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]:

< heightStatement (termStatement (Rep_StatementPos stmt))" .... qed

(hints recdef_simp add: rssem_h_term1)

Thanks for any hints Nicole -- "Never in the field of software development was so much owed by so

**Attachment:
PGP.sig**

**Follow-Ups**:**Re: [isabelle] recdef problem***From:*John Ridgway

**Re: [isabelle] recdef problem***From:*Elsa L Gunter

**Re: [isabelle] recdef problem***From:*Norbert Schirmer

- Previous by Date: [isabelle] who knows theorem-proving about cache protocols
- Next by Date: Re: [isabelle] recdef problem
- Previous by Thread: Re: [isabelle] who knows theorem-proving about cache protocols
- 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