Re: [isabelle] Modify theorem with equality assumption



Hi,

Am Donnerstag, den 02.04.2015, 17:46 +0200 schrieb Manuel Eberl:
> I have a number of theorems that contain some constant p both in their
> assumptions and in their conclusions.
> 
> I now want to derive modified theorems from them by adding an assumption
> "p = ?q" (for a schematic variable ?q) and replace all occurrences of p
> in the assumptions and the conclusion with ?q. Ideally in ML.
> 
> What is the easiest way to do that?


foo[unfolded eq_thm] or foo[folded eq_thm] do it in Isabelle/Isar; not
sure about Isabelle/ML.

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.