Re: [isabelle] Modify theorem with equality assumption



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.

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.