Re: [isabelle] Substitute in the whole context


Am Freitag, den 18.07.2014, 15:02 +0200 schrieb Lars Noschinski:
> On 18.07.2014 13:02, Joachim Breitner wrote:
> > 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:
> What about
>    note CaseName = CaseName[unfolded `d = _`]
> (although I'd probably use a different name)

thanks. That’s another nice trick, and an approximation to what I want.

It still doesn’t help me with updating the goal goal (which is probably
harder, as the “goal” as such doesn’t exist. I expect something that
implicitly opens a new context, exports a new ?case and/or thesis, and
then modifies whatever comes out of it at the end).
It also does not change other unnamed local facts containing d.


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.