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> _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
