*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 07 Apr 2015 11:52:56 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1504071140010.51301@lxbroy10.informatik.tu-muenchen.de>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr> <551DB1BE.9050308@in.tum.de> <alpine.LNX.2.00.1504071140010.51301@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

This code runs in the context of a locale in which as and bs are fixed and have type "real list". I should have mentioned that. I have to use the repository version because I require some measure-theoretic theories that are not present in the latest release. Cheers, Manuel On 07/04/15 11:47, Makarius wrote: > On Thu, 2 Apr 2015, Manuel Eberl wrote: > >> The following piece of code seems to do what I want to do. Am I doing >> anything 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:*Makarius

**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:*Makarius

- 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