Re: [isabelle] Problem with local proof



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
qed


What are the causes, what the workarounds? I find it a quite nasty limitation of structured proofs...

Structured proofs are a bit like programming without "goto", or "peek" and "poke". By taking away certain features, the text can become sufficiently informative to approximate human readability to some extend.


Anyway, your above example is probably just based on a misunderstanding what "proof" and "?thesis" really mean in Isar. When you say "proof" without any arguments, the system applies some default refinement to your problem, and then enters a subproof. So the initial goal is already changed here.

The "?thesis" abbreviation always refers statically to your last claim, cf. "shows". After refining that, the abbreviation usually becomes useless (although there can be monotonic refinements where ?thesis remains applicable).

I reckon, you've meant "proof -" above, to open a proof block without any initial refinement. The you can "show ?thesis" and everything fits together as expected.


	Makarius






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