Re: [isabelle] Using the simplifier from the ML-level



I thought the exact behavior of simp only: thms was to add thms to the simpset resulting from Simplifier.clear_ss ss, where ss is the simpset of the actual context. Most of the time, however, HOL_basic_ss does the job.

Amine.

Makarius wrote:
On Tue, 1 Jul 2008, Gudmund Grov wrote:

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.

The main problem here is empty_ss, which is insufficient to perform rewrites for the object-logic. You can use HOL_basic_ss instead.
The following imitates "simp only" to some degree:

  apply (tactic {* asm_full_simp_tac (HOL_basic_ss addsimps @{thms my_rules} *})

Actually the "simp" method also wraps the tactic into the CHANGED combinator, making it fail if no rewrites apply.


	Makarius





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