Dear BNF experts,
a while ago  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
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.
isabelle-dev mailing list