Re: [isabelle] Atomisation of free variables



Dear Manuel,

I don't know whether this is exactly what you want, but perhaps the following snippet is of help:

consts P :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
consts Q :: "'a ⇒ 'b ⇒ 'c ⇒ bool"

axiomatization where foo: "P a b c ⟹ Q a b c"

ML {*
fun transform ctxt thm =  
  let 
    val thm' = forall_intr_vars thm
    val meta_eq = Object_Logic.atomize ctxt (cprop_of thm')
  in
    Raw_Simplifier.rewrite_rule ctxt [meta_eq] thm'
  end

val new_thm = transform @{context} @{thm foo}

*}

Best,
René



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