Re: [isabelle] Modify theorem with equality assumption



> * What is the context where "p" in @{term "p"} comes from and belongs to?
p is an abbreviation of type real defined in terms of as and bs in the
locale context.

> * 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. 
Ah, I see.

> "The" repository version is undefined, until "hg id" is used. 
e83ecf0a0ee1. I usually make a point of pulling the latest version
regularly to keep my developments up-to-date.

> Another variation: fix q locally, then work with non-schematic
> material inside the extended context (which is usually easier and more
> robust), then export the result into the original context to make q
> schematic. 
Is that not what I did in the end? (q being p')


Cheers,

Manuel


On 07/04/15 11:54, Makarius wrote:
> 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
>
>
>
> The main point of Thm.cterm_of acting on Proof.context in coming
> Isabelle2015 is to make Isabelle/ML tool implementations more
> conformant to normal context discplines, and not drop out into some
> global thy value from the background.
>
>
>     Makarius






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