Re: [isabelle] Modify theorem with equality assumption



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

with 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)

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

What I would like to know is whether any of the things I do are
considered bad style.


Cheers,

Manuel


On 03/04/15 07:02, Jasmin Blanchette wrote:
>> On 02.04.2015, at 23:16, Manuel Eberl <eberlm at in.tum.de> wrote:
>>
>> 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?
> I donât know, but this
>
>> 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)
> looks different from what you described abstractly in your previous email.
>
> Jasmin
>




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