[isabelle] Substitute in the whole context


I often see this pattern:

I am in some isar context:
        case (CaseName a b c d)

and one of the first few facts is finding out something about d:

        from CaseName(..)
        obtain e f where "d = (e,f)" <proof>

and from now on, I would like to forget d, but I still have to unfold it
in local facts and goals:

        from CaseName(3)[unfolded `d = _`] 
        have "..." <proof>
        show ?case unfolding d <proof>

Is there some better way of handling this, where after I have shown "d =
(e,f)" I don’t have to worry about d any more?

I can imagine a command

        subst_in_context `d = (e,f)`

which unfolds d in all local facts and all goals, while retaining their
names (CaseName(2)) etc. until the next "next" or "qed".
Would that be desirable?
Would it be technical possible?


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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