Email Gateway (Aug 18 2022 at 13:18): Email Gateway (Aug 18 2022 at 13:18):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
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...
bu
PS.: It does not change anything if I remove the !!X. ...
Email Gateway (Aug 18 2022 at 13:31):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 08:18 UTC