Email Gateway (Aug 22 2022 at 13:02): Email Gateway (Aug 22 2022 at 13:02):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
what is the equivalent to e.g.
lemma "..."
...
using [[simproc del: s]]
...
in Eisbach methods (or if that doesn't work with Isabelle/ML).
cheers
chris
Email Gateway (Aug 22 2022 at 13:02):From: Daniel Matichuk <Daniel.Matichuk@nicta.com.au>
Hi Christian,
The match method can be slightly abused to get the desired effect:
method my_simproc_env methods m =
(match termI in H[simproc del: bad_simproc]:_ ⇒ ‹m›)
Here the match against the “termI” fact only produces one result, which we name and then use as a handle for making our “simproc del:” declaration.
We can then use this as a usual higher-order method:
apply (my_simproc_env ‹simp›)
However, it is relatively straightforward to write a method in ML that will accomplish this a bit more generically.
method_setup noting =
‹Scan.lift (Parse.and_list1 Parse.xthms1 --| Args.$$$ "in") -- Method_Closure.method_text >> (fn (args, m) => fn ctxt =>
let
fun no_binding args = map (pair (Binding.empty, [])) args;
val ctxt' = ctxt
|> Proof_Context.note_thmss ""
(Attrib.map_facts_refs (map (Attrib.attribute_cmd ctxt)) (Proof_Context.get_fact ctxt) (no_binding args))
|> snd
in Method_Closure.method_evaluate m ctxt' end)
›
Which then looks a bit like the “note” command:
apply (noting [[simproc del: bad_simproc]]
in ‹simp›)
Regards,
Dan
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.
Last updated: Nov 21 2024 at 12:39 UTC