Stream: General

Topic: Retrieve all registered BNFs

Balazs Toth (Mar 12 2025 at 21:44):

I'm not so familiar with the ML-side of Isabelle, so I'm not sure if there is an easy way to achieve what I want:

I have a locale that could be interpreted by any BNF. Is it possible to get a list of all registered BNFs and interpret this locale for them?
I was looking into the implementation of the command print_bnfs but couldn't figure out how to get the list of BNFs and not just the pretty printed output

Dmitriy Traytel (Mar 13 2025 at 08:26):

I don't recall such a function being exported. The interface allows you to query whether a given type is a BNF.

We are using plugins for (co)datatypes if we want to have something done for any type introduced by these commands. For basic BNFs (sums, products, functions, etc.) it would have to be done manually though.

Can you give more hints about your application?

Balazs Toth (Mar 13 2025 at 13:17):

I have a lifting of definitions and lemmas (regarding substitutions of terms) that works for natural functors. I don't need the bounded property. I have a locale specifying natural functors and it would be cool to automatically have bnfs interpret this locale, such that I do not have to do it manually

Dmitriy Traytel (Mar 13 2025 at 13:33):

When you say: "I have a locale specifying natural functors" do you mean some monomorphic version of the naturality/functoriality properties? I.e., what is the type of Fmap in your locale?

Balazs Toth (Mar 13 2025 at 13:58):

Yes, it's a monomorphic version:

locale natural_functor =
  fixes
    map :: "('a ⇒ 'a) ⇒ 'b ⇒ 'b" and
    to_set :: "'b ⇒ 'a set"
  assumes
    map_comp [simp]: "⋀b f g. map f (map g b) = map (λx. f (g x)) b" and
    map_ident [simp]: "⋀b. map (λx. x) b = b" and
    map_cong0 [cong]: "⋀b f g. (⋀a. a ∈ to_set b ⟹ f a = g a) ⟹ map f b = map g b" and
    to_set_map [simp]: "⋀b f. to_set (map f b) = f ` to_set b" and
    exists_functor [intro]: "⋀a. ∃b. a ∈ to_set b"

Dmitriy Traytel (Mar 13 2025 at 14:58):

I see. You can use the following. It is a bit wasteful, because it looks at all types declared in a context, but as long as you are not doing this over and over again it should be fine.

ML ‹fun all_bnfs ctxt = ctxt |> Proof_Context.theory_of |> Theory.defs_of |> Defs.all_specifications_of
  |> map_filter (fn ((kind, name), _) => if kind = Defs.Type then BNF_Def.bnf_of ctxt name else NONE)›

declare [[ML_print_depth=100]]
ML ‹all_bnfs @{context} |> map BNF_Def.T_of_bnf›

Balazs Toth (Mar 13 2025 at 15:12):

I'll try that, thanks!

Last updated: Dec 28 2025 at 02:03 UTC