[isabelle] Using the simplifier from the ML-level



Hi,

As part of a larger tactic being developed I need
to be able to use the simplifier (from the ML-level) using different
simpsets. Basically, I want the same behavior as calling (simp only: ..)
will give. For example, assuming the theorem list my_rules

  lemmas my_rules = ...

I need a tactic "my_simp" such that

apply (simp only: my_rules) = apply (tactic "my_simp @{thms my_rules}")

I have tried the following

ML {*
fun my_simp defs = simp_tac (MetaSimplifier.addsimps (MetaSimplifier.empty_ss,defs)) 1;
*}

but in some cases, it fails to rewrite, while (simp only: ...) succeeds.

I will be very grateful for any help on this manner, and note
that  I am currently using Isabelle 2007.

Best,

Gudmund





--
Heriot-Watt University is a Scottish charity
registered under charity number SC000278.






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