Re: [isabelle] Substitute in the whole context



Hi,

Am Freitag, den 18.07.2014, 13:11 +0200 schrieb Tobias Nipkow:
> 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>
> 
> Here is a naive approximantion of what you want:
> 
>                      where [simp]: "d = (e,f)" <proof>

Of course :-)

But it doesn’t work well in a style with lots of "from fact have "foo"
by (rule lemma)" and "CaseName.IH[OF this]", which I prefer for being
more explicit.

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