Re: [isabelle] Modify theorem with equality assumption



It occurred to me to simply use theorem rewriting. 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
  in
    thm
    |> Local_Defs.unfold ctxt' [Thm.assume cprop RS @{thm p_unique}]
    |> Thm.implies_intr cprop
    |> rotate_prems 1
    |> singleton (Variable.export ctxt' ctxt)
  end

  val _ =  Pretty.writeln (Syntax.pretty_term @{context} (Thm.prop_of
@{thm master1}))
  val _ =  Pretty.writeln (Syntax.pretty_term @{context} (Thm.prop_of
(generalize_master_thm @{context} @{thm master1})))
*}


Input theorem:
g â O(Îx. real x powr ?p') â
1 < (âi<k. as ! i * bs ! i powr ?p') â
eventually (Îx. 0 < f x) sequentially â
f â Î(Îx. real x powr p)

Output theorem:
g â O(Îx. real x powr ?p') â
1 < (âi<k. as ! i * bs ! i powr ?p') â
eventually (Îx. 0 < f x) sequentially â
(âi<k. as ! i * bs ! i powr ?p''1) = 1 â
f â Î(Îx. real x powr ?p''1)


Cheers,

Manuel


On 02/04/15 18:35, Jasmin Blanchette wrote:
>> I have a number of theorems that contain some constant p both in their
>> assumptions and in their conclusions.
>>
>> I now want to derive modified theorems from them by adding an assumption
>> "p = ?q" (for a schematic variable ?q) and replace all occurrences of p
>> in the assumptions and the conclusion with ?q. Ideally in ML.
>>
>> What is the easiest way to do that?
> I think youâll have to instantiate the âsubstâ theorem with the right âPâ and âsâ (using âDrule.cterm_instantiateâ or other similar functions), then you can use resolution with your original theorems (e.g. âRSâ or âOFâ in ML). This is a bit tricky, but a good opportunity to exercise forward theorem derivations in Isabelle.
>
> Alternative: A backward proof. You construct the statement of the theorem you want to prove and write a little tactic to solve it. Here, both forward and backward are about equally difficult, because you need to build some terms (the âPâ instance in the forward proof, the goal statement in the backward proof).
>
> Jasmin
>
>




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