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.