*To*: Burkhart Wolff <Burkhart.Wolff at lri.fr>*Subject*: Re: [isabelle] Problem with local proof*From*: Makarius <makarius at sketis.net>*Date*: Wed, 20 May 2009 15:39:42 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <37700668-BFD3-4162-B0E7-70A9DC6C986A@lri.fr>*References*: <37700668-BFD3-4162-B0E7-70A9DC6C986A@lri.fr>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Thu, 30 Apr 2009, Burkhart Wolff wrote:

I run quite a few times in this particular problem pattern: I proved a local lemma, I succesfully completed the main proof, (done is finished), but got a "Failed to finish proof" at the end. Here is my example: lemma is_processT6_S1: assumes A :"tick ~ X" and B :"(s @ [tick], {}) ~ F P" shows "(s::'a event list, X) ~ F P" proof have C : "!!X::'a event set. tick ~ : X ==> X - {tick} = X" by auto show ?thesis apply(insert A B) apply(subst C[symmetric], simp) apply(erule is_processT6_S) done qedWhat are the causes, what the workarounds? I find it a quite nastylimitation of structured proofs...

Makarius

- Previous by Date: [isabelle] Problems with datatype definition
- Next by Date: Re: [isabelle] strange behaviour with type instantiation
- Previous by Thread: Re: [isabelle] Problems with datatype definition
- Next by Thread: [isabelle] problem with opening proof
- Cl-isabelle-users May 2009 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