Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 12:07):

From: Makarius <makarius@sketis.net>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 12:07):

From: Amine Chaieb <chaieb@in.tum.de>
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:

view this post on Zulip Email Gateway (Aug 18 2022 at 12:14):

From: Gudmund Grov <gg10@macs.hw.ac.uk>
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

Last updated: May 03 2024 at 12:27 UTC