[isabelle-dev] Advice for replacing @{simpset} with @{context}.

[David Greenaway]

Hi all,

I am in the process of updating some of our local tools to the
repository version of Isabelle, in preparation for the next Isabelle
release (possibly named Isabelle 2013-1?) One of the changes that has
occurred since Isabelle 2013 is that simpsets have been deprecated in
favour of storing simplifier rules directly in the context.

In this new world order, what is the best way to manage "long-term"
simpsets when they are not in active use?

For example, imagine that I have a theorem attribute "foo", which adds
a rule to a set of theorems:

    lemma a [foo]: ...
    lemma b [foo]: ...
    lemma c [foo]: ...

I also have a tactic "bar" which internally passes this set of theorems
to the simplifier. The implementation in Isabelle 2013 is simple: have
a simpset floating around in your theory data, add new theorems to it on
demand, and finally use it when needed.

I am not sure what the best way to port this forward is. I could store
the theorems as a list in my theory data, but that would mean it would
need to be converted into a discrimination net each time the tactic
"bar" was used, which could have performance implications when the
number of theorems is large.

I could convert back and forth from a context each time a new rule is
added as such:

    val new_ss = simpset_of ((put_simpset convenient ctxt old_ss) addsimps [new_thm])

but I suspect that this was not the intended solution.

Any suggestions as to the best way to manage sets of rules that will
eventually be fed into the simplifier?

Thanks so much,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.