[isabelle-dev] map/rel/set for lift_bnf

[Lars Hupel]

Dear BNF experts,

a while ago [0] I posted some comments on the "lift_bnf" command. I'm
currently in the process of cleaning up the "Finite_Map" theory and
found out that now, "lift_bnf" exports the definitional theorems for
map/rel/set.

In this case, the theorem looks like this:

fmmap ≡ λf. Abs_fmap ∘ Finite_Map.fmap.fun.map_fun f ∘ fmlookup

But if I look at "BNF_Def.map_def_of_bnf", the theorem looks like this:

fmmap ≡ λf. Abs_fmap ∘ op ∘ (map_option f) ∘ fmlookup

I couldn't find any way to unfold "Finite_Map.fmap.fun.map_fun" (which
is presumably some internal constant), which means I still have to use
the workaround of manually registering the lemmas I want.

This is not urgent, but it would be cool if I could get rid of the
workaround for Isabelle2017.

Cheers
Lars


[0]
<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-August/msg00001.html>