Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "using [[...]]" with Isabelle/Eisbach or Isabe...


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC