*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:47:39 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <551DB1BE.9050308@in.tum.de>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr> <551DB1BE.9050308@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 2 Apr 2015, Manuel Eberl wrote:

The following piece of code seems to do what I want to do. Am I doinganything in there that I should not do or do differently?ML {* fun generalize_master_thm ctxt thm = let val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt val p' = Free (p', HOLogic.realT) val a = @{term "nth as"} $ Bound 0 val b = @{term "Transcendental.powr"} $ (@{term "nth bs"} $ Bound 0) $ p' val f = Abs ("i", HOLogic.natT, @{term "op * :: real => real => real"} $ a $ b) val setsum = @{term "setsum :: (nat => real) => nat set => real"} $ f $ @{term "{..<k}"} val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (setsum, @{term "1::real"})) val cprop = Thm.cterm_of ctxt' prop

Just the usual hints on context-conformance of Isabelle/ML snippets: * The @{term} antiquotations mention free variables "as", "bs", "k". To which context do they belong? If they are undeclared, the code will crash in a context that declares them locally. * @{term "nth as"} is polymorphic, i.e. in invents a locally fixed type 'a (depending on the compilation context). This is likely to break down when used in a different context. * As a general rule of thumb, @{term} antiquotations are only useful for well-defined closed terms, such as @{term "1::real"}. Variables need to be constructed explicitly at run-time, like p' above. * The global context above is not immediately clear, making it hard to test. Morover, it seems to use an undefined repository version, instead of the latest release. 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

- Previous by Date: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- 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