[isabelle] Problem with local proof



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. ...





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