Artem Khovanov (Sep 04 2023 at 22:14): Artem Khovanov (Sep 04 2023 at 22:14):Is it possible to get a list of all theorems in my context having a certain attribute? For instance [simp] or [transfer_rule].
Mathias Fleury (Sep 05 2023 at 05:29):lemmas [simp] = a b c d e
or multiple labels:
lemmas [simp, transfer_rule] = a b c d e
I think Mathias might have misread the question and explained how you can apply attributes to multiple theorems.
You cannot search for theorems that got applied to an arbitrary attribute because, in general, an attribute is just a function context * thm -> context * thm (reference to implementation manual).
You can ctrl+click on the attribute and, most of the time, you will end up in an ML module that also exposes a function returning the theorems applied to the attribute in question.
Here are the relevant functions for simp and transfer_rule:
ML‹
val simps = simpset_of @{context} |> dest_simps
val transfers = Transfer.get_transfer_raw @{context}
›
ah yeah I misread sorry
Mathias Fleury (Sep 05 2023 at 07:19):One addition: newer attributes are usually declared with named_theorems and you can view then like normal theorems thm no_atp
Mathias Fleury (Sep 05 2023 at 07:20):but this does not work for simp and transfer
Mathias Fleury (Sep 05 2023 at 07:20):at least for simp you need some transformations on the theorems, so it is not only about declaring the theorem, but also massaging it in the right form
Artem Khovanov (Sep 05 2023 at 13:21):Ah OK, yeah I see, not being able to search by attribute makes sense.
Last updated: Apr 28 2024 at 12:28 UTC