Re: [isabelle] Modify theorem with equality assumption



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

I think youâll have to instantiate the âsubstâ theorem with the right âPâ and âsâ (using âDrule.cterm_instantiateâ or other similar functions), then you can use resolution with your original theorems (e.g. âRSâ or âOFâ in ML). This is a bit tricky, but a good opportunity to exercise forward theorem derivations in Isabelle.

Alternative: A backward proof. You construct the statement of the theorem you want to prove and write a little tactic to solve it. Here, both forward and backward are about equally difficult, because you need to build some terms (the âPâ instance in the forward proof, the goal statement in the backward proof).

Jasmin





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