Re: [isabelle] Modify theorem with equality assumption



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





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