Re: [isabelle] Modify theorem with equality assumption



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.