[isabelle] Substitute in the whole context



Hi,

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

Thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~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.