*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Makarius <makarius at sketis.net>*Date*: Tue, 7 Apr 2015 11:54:51 +0200 (CEST)*Cc*: Jasmin Blanchette <jasmin.blanchette at inria.fr>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <551E6982.6090606@in.tum.de>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr> <551DB1BE.9050308@in.tum.de> <A9D5660E-91C3-413E-925D-9AECE3D68775@inria.fr> <551E6982.6090606@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 3 Apr 2015, Manuel Eberl wrote:

Yes, I do another step. I do not assume the equation directly, but something that implies it. A function that does what I actually asked is this: fun generalize_master_thm ctxt thm = let val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt val p' = Free (p', HOLogic.realT) val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (@{term "p"}, p')) val cprop = Thm.cterm_of ctxt prop in thm |> Local_Defs.unfold ctxt' [Thm.assume cprop] |> Thm.implies_intr cprop |> rotate_prems 1 |> singleton (Variable.export ctxt' ctxt) end

* What is the context where "p" in @{term "p"} comes from and belongs to? * The prop belongs to ctxt' by construction, so further contextual operations need to use that, or a monotonic extension of it. So Thm.cterm_of ctxt should be Thm.cterm_of ctxt'. Otherwise, one needs a semantic proof, why ctxt is sufficient, but it merely obscures the code.

Makarius

**Follow-Ups**:**Re: [isabelle] Modify theorem with equality assumption***From:*Manuel Eberl

**References**:**[isabelle] Modify theorem with equality assumption***From:*Manuel Eberl

**Re: [isabelle] Modify theorem with equality assumption***From:*Jasmin Blanchette

**Re: [isabelle] Modify theorem with equality assumption***From:*Manuel Eberl

**Re: [isabelle] Modify theorem with equality assumption***From:*Jasmin Blanchette

**Re: [isabelle] Modify theorem with equality assumption***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Modify theorem with equality assumption
- Next by Date: Re: [isabelle] Modify theorem with equality assumption
- Previous by Thread: Re: [isabelle] Modify theorem with equality assumption
- Next by Thread: Re: [isabelle] Modify theorem with equality assumption
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list