Re: [isabelle] recdef problem



I have encountered the same probleam and have usually been able to work around it in the following manner: Begin by adding the (permissive) qualifier to recdef (ie recdef (permissive) <name> ...). This will still complain but it will give you back theorems <name>.induct and <name>.simps, but with the "bad final proof state" as hypotheses. You can now create the version of the induction theorem you want, omitting the "bad final proof state" hypotheses, by using the version of this theorem you were given together with the lemma(s) proving the "bad final proof state" as follows:

lemmas <name>_induct = <name>.induct [OF hyp_lemma1 hyp_lemma2 ...]

You can create the version of the definition (without the bad final proof state) by stating a theorem that doesn't have the unwanted hypotheses and then using <name>.simps as a rule (assuming it is just one theorem) and reducing your problem to one of solving the "bad final proof state" hypotheses. Then you want to remove the <name>.simps from the simplifier and add in your own version. This is pretty crufty, but seems to work in most cases. As far as I can guess, the problem seems to be that when you add the hypothesis to the simplifier it first gets "simplified" and then the simplifier doesn't seem to be able to prove the hypothesis from the simplified version. It would be nice if someone (more knowledgable of the inner workings of Isabelle than I currently am) would modify the redef procedure so that instead of failing with "bad final proof state" it would behave like the instance procedure and throw you into proving the "bad final proof state".
---Elsa

Nicole Rauch 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






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