Re: [isabelle] Simplification




Wolff Burkhart wrote:
> I.e., I'd like to have a function of type thm => thm that
> converts:

I have forgotten this part of the question:

This solves the problem:

lemma annoyTrue: "(P ==> True) == Trueprop True"
  apply (atomize (full)) by auto

lemma annoyTrue': "(True ==> PROP P) == PROP P" by auto

ML{* Simplifier.rewrite_rule [ at {thm annoyTrue}, @{thm annoyTrue'}]
  (assume @{cterm "[| A ==> True ; B |] ==> C"})*}

The function is then just

Simplifier.rewrite_rule [ at {thm annoyTrue}, @{thm annoyTrue'}]

Cheers,
Amine.






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