[isabelle] A sorry qed



Hi,

Right now I was in the middle for a multi-case induction proof,
something like

        have "foo"
        proof(induct ...)
        case (A ...)
          ...
          show ?case by ...
        next
        case (B ...)
          ...
          show ?case by ...
        next

with many cases remaining. At this point, I wanted to stop working on
this proof and do something else. With apply-scripts I’d just write
"sorry" instead of "done" and be done with it. But what can I do here,
besides writing down each missing case and solving it with "sorry"? I
tried

        show "foo" sorry
        qed
        
but of course "foo" is not the current goal any more. Things like

        qed sorry
        
or

        apply_end(sorry)
        qed

or
     qed(cheating)
        
(the “cheating” coming from A.1.3 of isar-ref, but seemingly not meant
literarly) of course don’t make sense either. Is there a clean way to
stop the proof here?

Thanks,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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