Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
The relevant text from NEWS is this: * Simplifier tactics and tools use proper Proof.context instead of historic type simpset. Old-style declarations like addsimps, addsimprocs etc. operate directly on Proof.context. Raw type simpset retains its use as snapshot of the main Simplifier context, using simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port old tools by making them depend on (ctxt : Proof.context) instead of (ss : simpset), then turn (simpset_of ctxt) into ctxt. So the only way to replace a HOL_basic_ss addsimps ... somewhere deep inside my code (in my actual case, inside a conversion) is to thread through the proof context everywhere? ... a quite tedious change. -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
On Fri, 13 Sep 2013, Peter Lammich wrote: The relevant text from NEWS is this: * Simplifier tactics and tools use proper Proof.context instead of historic type simpset. Old-style declarations like addsimps, addsimprocs etc. operate directly on Proof.context. Raw type simpset retains its use as snapshot of the main Simplifier context, using simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port old tools by making them depend on (ctxt : Proof.context) instead of (ss : simpset), then turn (simpset_of ctxt) into ctxt. So the only way to replace a HOL_basic_ss addsimps ... somewhere deep inside my code (in my actual case, inside a conversion) is to thread through the proof context everywhere? ... a quite tedious change. Is this hypothetical, or do you still have tools without a proper context? It should be trivial to pass through some ctxt: Proof.context nonetheless, i.e. do the localization in that elementary sense. Unless there is something really strange here ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Advice for replacing @{simpset} with @{context}.
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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
On Thu, 12 Sep 2013, David Greenaway wrote: 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. Deprecated is is not really the wording we would use in the Isabelle context. Sun/Oracle use that term for Java operations that are never changed, but Isabelle lives on continuous renovation for 25 years already. The NEWS file explains what will happen in the coming release with simpset vs. Proof.context -- the Simplifier was one of the last hold-outs of non-localized tools, so after long delays we are mostly through with it. Isabelle/jEdit has now this Documentation dockable to access documentation. Its tree view also includes NEWS to access the all-important NEWS file with the history user-relevant changes. It also has its own jEdit editor mode with Sidekick tree etc. (The NEWS file still needs some polishing before we start the actual release candidate cycle in a few weeks.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
On 13/09/13 04:17, Makarius wrote: The NEWS file explains what will happen in the coming release with simpset vs. Proof.context -- the Simplifier was one of the last hold-outs of non-localized tools, so after long delays we are mostly through with it. Sorry, I should have mentioned that I read the NEWS file; I understood that the simplifier now accepted a context instead of a simpset, and that addsimps operated on contexts instead of simpsets. My question was instead related to the best way to perform operations on long-lived simpsets which need to be mutated over time, now that there are no exposed APIs for manipulating them. Florian's reply was helpful in pointing out some code (the code generator) which also had this problem, and its solution to this which amounts to: (i) taking your old simpset; (ii) putting it into a dummy context; (iii) performing your addsimp/addcong/etc operation; (iv) extract the simpset out again. Cheers, 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
